Unions and Intersections

@shelby3

@shelby3 I want to discuss whether to include union types here. I would like to design a language that meets the requirements you have for extensibility, but I don't necessarily want to achieve it with unions. I am not fundamentally opposed to unions, and if they are the best way to achieve what we want then we have them, but in the interests of keeping the language as small as possible, I want to make sure we are adding something of value, that cannot be achieved in other ways. Can you provide some example use cases for union types so we can explore the possibilities?

@shelby3

More comments to follow...

@shelby3 wrote:

And this is why we need anonymous structural union types, e.g.:
if (x) true
else 3
The inferred type is Boolean | Number.

I realise you can write "if x true else 3", but why would you do that? To me this is not a motivating example, it needs to be something a bit bigger, and algorithm or design pattern that benefits in readability or simplicity from having the feature. What do we lose by insisting both sides of the 'if' are the same type?

@keean

@keean wrote:

I realise you can write "if x true else 3", but why would you do that?

Resolving to an instance of a heterogeneous type.

mycollection.append(if (something) new Type1() else new Type2())

What about inferring the type "x where x is in all common traits"? If you allow traits as "return" types then this is not a problem.

@keean

@keean wrote:

What about inferring the type "x where x is in all common traits"?

I presume you mean subsuming to the greatest lower bound (GLB) when the heterogeneous types involved are traits (which btw may not exist since we can't subsume to any top type without instigating unsafe code, so it would often be compiler error). That won't apply when the heterogeneous types are data types since we can compute the anonymous structural type of the disjoint union, because otherwise data types could not be subsumed without subclassing. So without subclassing, we must have tagged disjoint unions, else we would lose the solution to Wadler's Expression Problem.

If you allow traits as "return" types then this is not a problem.

I am thinking it is a non-unified language with many corner case for us to attempt to only allow trait types (bounds) on function arguments. We must support trait objects every where a type can be used, except they (trait bounds and trait objects) make no sense in unions because traits by definition aren't tagged (reified), but unions are okay for data types will (must) be tagged in the run-time.

Thinking about this more, traits are not types of instances. They are either monomorphic bounds on a type parameter of a function/method, or they are the polymorphic interface of trait objects with the dictionary joined to the instance just like subclasses (but with a hasA instead of isA subclassing semantics). Trait objects are polymorphic, and thus stall the CPU pipeline.

There are two ways for us to support polymorphism. One is to allow tagged unions of data types, which retains extension in both axes of Wadler's Expression Problem, because we can add new variants (data types) and new operations (trait implementations). The other is to allow trait objects, which only allow adding new data types, but not new operations, i.e. if we have an instance of a trait object, we can't implement it on other traits because we erased the underlying data type which is inside the trait object.

I remember we discussed all of this before in May, but I may not have been as clarifying and succinct as I am attempting to communicate now.

Edit: Trait objects enable polymorphism within a homogeneous type parametrized collection, so that an invariant collection does not need to be used and the type parameter can remain invariant.

So it appears we need both. The two ways to achieve polymorphism offer different trade-offs.

@shelby3

@shelby3 wrote:

I presume you mean subsuming to the greatest lower bound (GLB) when the heterogeneous types involved are traits (which btw may not exist since we can't subsume to any top type without instigating unsafe code, so it would often be compiler error). That won't apply when the heterogeneous types are data types since we can compute the anonymous structural type of the disjoint union, because otherwise data types could not be subsumed without subclassing. So without subclassing, we must have tagged disjoint unions, else we would lose the solution to Wadler's Expression Problem.

No, you simply keep the intersection of the traits implemented by both sides, the type remains polymorphic (unknown).

@keean

@keean wrote:

No, you simply keep the intersection of the traits implemented by both sides, the type remains polymorphic (unknown).

Which is the same as what I wrote. So why did you write "no"? You described the GLB.

Yes we can do that when the GLB is not the top type. But it is not entirely sufficient to only offer that capability and not also unions of data types.

You seem to be not quite grasping (or articulating that you've grasped) two of my points:

The GLB might the top type. In a safe language, the top type must be the empty set.
If there is a GLB, it remains polymorphic, but we've lost (erased) one of the axes of extension of Wadler's Expression Problem, as compared to retaining a union of data types.

@shelby3

@shelby3 wrote:

There are two ways for us to support polymorphism. One is to allow tagged unions of data types, which retains extension in both axes of Wadler's Expression Problem, because we can add new variants (data types) and new operations (trait implementations). The other is to allow trait objects, which only allow adding new data types, but not new operations, i.e. if we have an instance of a trait object, we can't implement it on other traits because we erased the underlying data type which is inside the trait object.

In a way they both suffer from a form of the expression problem. With tagged-unions, we have type-case statements scattered throughout the code, and If we add a new type to the tagged-union all the type cases need to have an extra option added.

With the "trait-object", if we want to add a new method to the collection you have to add a new trait to the collection type.

You seem to be not quite grasping two of my points:

The GLB might the top type. In a safe language, the top type must be the empty set.
If there is a GLB, it remains polymorphic, but we've lost (erased) one of the axes of extension of Wadler's Expression Problem, as compared to retaining a union of data types.

If there are no traits in common between two types, then there are no functions you can call on the object. Consider two objects A and B that have no methods in common. If we have a function that returns "A|B" what methods can we call on the value with type "A|B"... none at all.

If you want to do a type-case (runtime matching) you should be using a tagged union. The point of type-classes is to derive the statically safe set of functions/methods that can be called on some object.

@keean

@keean wrote:

In a way they both suffer from a form of the expression problem. With tagged-unions, we have type-case statements scattered throughout the code, and If we add a new type to the tagged-union all the type cases need to have an extra option added.

Disagree. This is the crux of my proposed complete solution to the Expression Problem which I explained to you before in May. Let me try again to explain it.

When calling a function with a trait bound and passing a union of data types as the input, the compiler can automatically create the type-case boilerplate and wrap it as if it is a single implementation of that trait bound and pass that to function simulating monomorphism. Within said implementation, it will be doing the type-case logic, so it does stall the CPU more than monomorphim, but it is seamless at the source code and emitted function implementation level; and it is more optimizeable than trait objects which erase their knowledge of the data types and thus must use agnostic (blinded) jump tables.

It is the outcome of using only a trait bound to operate on the tagged union, which makes it fully automated boilerplate. That was my insight.

Of course that doesn't prevent the programmer from doing type-class guards to get at the precise data types for some other reason, but that wouldn't be an extensible design pattern.

@keean

@keean wrote:

You seem to be not quite grasping (or articulating that you've grasped) two of my points:

1‌‌. The GLB might the top type. In a safe language, the top type must be the empty set.

If there are no traits in common between two types, then there are no functions you can call on the object. Consider two objects A and B that have no methods in common. If we have a function that returns A|B what methods can we call on the value with type A|B... none at all.

So we are in agreement.

Except that typically inferred subsumption to the top type is a compiler error (because it probably represents something the programming didn't intend, since it is more or less useless). The programmer must declare the top type, if that is what they want.

Btw, if you use backticks ` in markdown instead of quotes then your programming terms will be rendered correctly in a monospace font as shown above.

2. If there is a GLB, it remains polymorphic, but we've lost (erased) one of the axes of extension of Wadler's Expression Problem, as compared to retaining a union of data types.

If you want to do a type-case (runtime matching) you should be using a tagged union. The point of type-classes if to derive the statically safe set of functions/methods that can be called on some object.

Seems you didn't quite understand what I was trying to explain to you this past May (granted my elucidation was probably not coherent enough then). See my prior comment for another attempt to explain how to avoid type-case boilerplate.

Tangentially, I am doubting (not understanding) the claim that was made for Rust that monomorphic trait bounds do not stall the CPU pipeline. The function can't know which implementation it will be using until run-time, unless we generate a new version of the function for each implementation of a data type. Thus the function will be calling the methods using an array of pointers to the methods. So this is a jump table. We can't inline the methods into the function unless we generate a new version of the function for each implementation of a data type. So for a tagged union type, the same array of method pointers can be used, but of course within those wrapper methods will be run-time type-case branching which further stall the CPU pipeline, but branches are more optimizeable by the CPU than arbitrary jumps that would be the case for trait objects.

@shelby3

@shelby3 I think you are not fully understanding the difference between dynamic (runtime) and static (compile time) polymorphism, and this is leading to confusion between us when we discuss this. Lets start with static polymorpism:

id<A>(x: A) : A {return x;}
id(4)

In this program id has a polymorphic type, that means its implementation is the same no matter what type it is passed. In this case only a single implementation of 'id' is required for all types.

class Show B {
    show(x : B)
}

instance Show for Int {
    show(x) = print_int(x)
}

instance Show for String {
    show(x) = print_string(x)
}

show(4)
show("ABC")

Here we see specialisation, there are different overloaded implementations for 'show' that are chosen by type. Each implementation deals with exactly one type.

show_twice<A : Show>(x : A):
    show(x)
    show(x)

Using type-classes we can write generic functions like 'show_twice' that work for any type by looking the specialised version of the function calls it uses up in the dictionaries for the types passed, but is a single generic implementation (the type class dictionary for 'Show A' is an implicit parameter').

However it is important to note that the type parameter is invariant, that means we must know the concrete type at compile time (this is the difference between parametric types and universally-quantified types, with universally-quantified types there are some situations like polymorphic-recursion where we might not know the type until runtime, which is why Haskell does this by dictionary passing). So with parametric types 'A' must be a ground type in order to compile the function, which means we can monomorphise and output a specific version of 'show_twice' for the type of the argument passed. So this is what happens:

show_twice("ABC")

compiles to:

show_twice___string(x : String):
    print_string(x)
    print_string(x)

show_twice___string("ABC")

combined with inlining this will produce:

print_string("ABC")
print_string("ABC")

So you can see there is no use for 'unions' as we must provide a concrete/ground type as the type parameter for a parametric function, and we can do this if the data is static.

When calling a function with a trait bound and passing a union of data types as the input, the compiler can automatically create the type-case boilerplate and wrap it as if it is a single implementation of that trait bound and pass that to function simulating monomorphism.

This is where I think you have a misunderstanding, if we can statically determine the type, then we can statically determine the exact type, no unions necessary. For example:

x : bool = true
y = if x then "hello" else 32
show_twice(y)

Here we know the type of 'y' is a string because 'x' is true, as such what is passed to show_twice is always 'string', it is never a 'string or int' because such a thing cannot exist y is always precisely a string or an int, never both at the same time. So for static polymorphism we never need union types.

Note: this kind of thing is not normally allowed because the type of 'y' depends on the value of ''x' being true or false. Such things are called dependent types, and languages like Rust don't allow this, instead they only allow types to depend on other types.

A follow on from above, although we cannot support monomorphisation easily in the final case above, we can use path dependent types to do something similar. If we require the return type from 'if' to be the same on both sides, or perhaps more easily have 'if' as a statement not an expression so there is no 'return' type we can simply do:

if x then:
    show_twice("hello")
else:
    show_twice(32)

Here the type of 'show_twice' depends on the path taken at runtime, but we know the exact type passed to each instantiation of the polymorphic functions 'show_twice'. This is a compelling reason to not allow 'if' in expressions.

I would argue the above code is simpler and easier to read the the 'if' expression version, with the small cost of having to repeat 'show_twice'...

So I think where I need the unions is in something like a parser:

y = if x:
        new Add(new Num(1), new Num(2))
    else:
        new Mul(new Num(1), new Num(2))
y.print()

So y would have the type Add<Num, Num> | Mul<Num, Num> and y.print() would have to be passed both dictionaries.

But with a parser its all going to go horribly wrong because we will need recursive types, and at every parse decision we will double the number of terms in type.

Consider the type signatures of the parser functions

parse_num(in : Stream) : Num
parse_add(in : Stream) : Add<Num, Num>
parse_mul(in : Stream) : Mul<Num, Num>
parse_expr(in : Stream) : Num | Add<Num, Num> | Add<Add<Num, Num>, Num> | Add<Add<Add<Num, Num>, Num>, Num> ... etc forever.

So we will also need recursive types, and be able to do something like:

type Expr = Num | Add<Expr, Expr> | Mul<Expr, Expr>
parse_expr(in : Stream) : Expr

Is that going to work? Can we infer the recursive types? What does it mean for dictionary passing?

@keean

@keean wrote:

I can do the following without unions:
(new Mul(new Add(new Num(1), new Num(2)), new Num(3))).print()
But that is all statically determined...

Exactly. Once you introduce polymorphism then without unions you will need to discard statically (in the source code) the struct types and assign to a Rust trait object. If you choose Eval for the bound of said trait object, then you won't be able to Print on it. Even if you have the foresight to put Eval+Print bound on said trait object, it still won't be open to extension to other trait bounds that were not created yet.

My solution isn't only applicable to type parametrized containers (such as List) but also in general for polymorphism as you have explained above. Thus the disadvantage of my solution compared to trait objects being that for its interoption with type parametrized containers, we are forced to use an invariant container such as List (which maintains invariance on the type parameter despite the subtyping relationship expressed by union types), is inapplicable (irrelevant) when using my solution not with a type parametrized container.

@shelby3

@shelby3 What do you think about the recursive typing issue in 'parse_expr', I think we may be able to infer it, and then it is a case of working out what dictionaries will be required in the trait-method. I think I get what is going on, and I think a parser and expressions are a good example to work with, as it is the core part of writing a compiler, which is something we are doing to implement the language.

I think its time to switch to the inferencing discussion: #5

@keean

@keean wrote:

I think its time to switch to the inferencing discussion: #5

Agreed.

@shelby3

I don't know anything about zenscript, but union types of sufficient power can enable overlapping ADTs and functions that are polymorphic across the exact shape of those ADTs.

You probably won't be able to support infinite types (surely not type inference for them), but if you used fixed point data, you don't need to (though that requires higher-kinded types to be really useful).

As an example in present day Scala:

case class Mul[A](left: A, right: A)
case class Sub[A](left: A, right: A)

type Coproduct[F[_], G[_], A] = Either[F[A], G[A]]

type Expr[A] = Coproduct[Mul, Sub, A]

case class Fix[F[_]](unwrap: F[Fix[F]])

You can regain a recursive definition for Expr[A], for example, by using Fix[Expr], and with a little effort, you can see how this representation is basically a "poor person's union type", albeit a higher order one. You can also see how ADTs can overlap and thus reuse parts of other ADTs, and how operation can be defined such that they require only the minimum components necessary.

As for how all this would translate into zenscript (or not), I'm not sure since I only learned of this project and this issue today thanks to an IM from @shelby3. Good luck Shelby! 😄

@jdegoes

@jdegoes its early days, so there's plenty of scope to influence the direction of the project :-) I have started building the compiler in JavaScript, with JavaScript as the first target. Big items to sort out are the syntax and the type system. I have been playing with type systems for a while, especially type inference, so I have a pretty good idea of how to implement it.

I think the core feature set at the moment are type-classes and union types. I think we will go with that and try and rapidly get to a first prototype, so that we can start writing programs, probably self-hosting the compiler would be the obvious thing to do.

Type inference for recursive types is not a problem in my experience, the type system internally works in the universe of regular-trees, and then we convert to 'Mu' types for display. For example:

((\x . ((x x) x)) (\x . ((x x) x))) : {} |- ((a -> b as a) -> b as b)

@jdegoes

@jdegoes wrote:

I don't know anything about zenscript, but union types of sufficient power can enable overlapping ADTs and functions that are polymorphic across the exact shape of those ADTs.

If I understand your point correctly, then we also realized that and is one of the reasons we need union types. That when combined with a novel way of resolving typeclasses for unions also enables us to truly solve the Expression Problem where apparently others haven't even they apparently erroneously claimed to.

You can regain a recursive definition for Expr[A], for example, by using Fix[Expr], and with a little effort, you can see how this representation is basically a "poor person's union type", albeit a higher order one.

We want to support a first-class unnamed structural union, to eliminate boilerplate and also so the inference engine can infer structural union types.

We are trying to provide what we see is a missing variant in programming language offerings, especially one designed to be compiled to JavaScript (although other targets might be a possibility as well). That is a strict evaluation, no subclassing(!), typeclasses, and first-class structural unions, for greater extension capabilities in a soundly typed language that is also uncluttered with paradigms and thus reasonably simple to grasp. Also a syntax reasonably close to JavaScript. We're distilling from the best features of each language.

We are building this because @keean and I decided we wanted to code (or at least experiment) in a language like this. And we see a gap in the market that is not filled. Kudos thus far to @keean on doing the most on implementation thus far. So far, we also have some interest expressed from @SimonMeskens and @svieira (both of whom I recently met via discussions at the TypeScript Github).

Thanks John for visiting our nascent project.

@shelby3

@shelby3 I am closing this issue because I think we are decided that anonymous structural unions should be in the language in some form (at least rank1).

@keean

@keean can you please edit the close to add a Label that indicates a favorable resolution?

I think I want flow typing and cleanest solution to null employing anonymous unions.

I think "flow typing" is what I call path-dependent typing, and if so, then yes it is something I want too.

Regarding null I think that makes sense. Null is effectively the unit type (void), and can be inferred into any union type.

There is a small problem with our type class approach, because normally we would want all types in the union to implement the type classes required by a function, when null will not implement all (if any) of them.

The solution is to force the programmer to explicitly provide a type-case for Null if null does not implement the type-class required for a function.

This is really a very simple axiom, and in the future we might allow more complex axioms, like inequality constraints on argument types.

This will feel almost exactly like dependent typing except we never depend on types at runtime, instead we force the user to statically insert a check value. This is really the combination of "path dependent types" and "refinement types".

I notice Ceylon always requires the type parameters, as in:

Box<Out> fmap<Box,In,Out>(Out(In) fun, Box<In> box) 
        given Box<Element> { ... }

I am sure we are okay to infer them, but it might cause problems with other Ceylon-like types, we just have to be careful as we expand the type system, and ideally keep it as simple as possible.

As long as not all types can be Null, I'm fine. As far as I'm concerned, no languages should have Null at all, a union type or an empty monad is all you need. Implicit nullable types are evil.

Navigation Menu

Repository navigation

Unions and Intersections #2

53 remaining items

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Unions and Intersections #2

Description

Activity

shelby3 commented on Sep 18, 2016

keean commented on Sep 18, 2016

shelby3 commented on Sep 19, 2016

keean commented on Sep 19, 2016

shelby3 commented on Sep 19, 2016

shelby3 commented on Sep 19, 2016

keean commented on Sep 19, 2016

shelby3 commented on Sep 19, 2016

keean commented on Sep 19, 2016

keean commented on Sep 19, 2016

shelby3 commented on Sep 19, 2016

shelby3 commented on Sep 19, 2016

shelby3 commented on Sep 19, 2016

keean commented on Sep 19, 2016

keean commented on Sep 19, 2016

53 remaining items

keean commented on Sep 20, 2016

shelby3 commented on Sep 20, 2016

keean commented on Sep 20, 2016

shelby3 commented on Sep 20, 2016

jdegoes commented on Sep 20, 2016

keean commented on Sep 20, 2016

shelby3 commented on Sep 21, 2016

keean commented on Sep 21, 2016

shelby3 commented on Sep 21, 2016

shelby3 commented on Oct 7, 2016

keean commented on Oct 7, 2016

keean commented on Oct 7, 2016

SimonMeskens commented on Oct 7, 2016

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions