[lmm]

You shouldn't need special cases for optional/maybe in the first case; optional/maybe are simple sum types, you would want whatever flow-typing system you have to do the right thing with user-defined "x or y or z" types, and if you do that then it'll automatically work just as well for optional/maybe.

(I don't like inclusive union types because they're noncompositional - code you write with them isn't parametric any more - which seems particularly awkward in a compiled language - how do you compile code that forms unions involving type parameters?)

[RX14]

You shouldn't be able to use a type without giving all the necessary type parameters, so you can't form a union type with unbound type parameters in so it's not a problem? I'm not 100% sure what you're asking...

I'm not 100% sure how you can integrate sum types with a flow-typing system, perhaps with pattern matching?

[lmm]

> You shouldn't be able to use a type without giving all the necessary type parameters, so you can't form a union type with unbound type parameters in

So inside the body of a generic method (or class) you can't form unions involving the method's type parameters? That works but makes them much less useful as a language feature - most language features work as normal within a generic method.

> I'm not 100% sure how you can integrate sum types with a flow-typing system, perhaps with pattern matching?

Whatever you do for union types should work, surely. Indeed it ought to be simpler since you have more information to work with - with a sum type if the thing is B then you know it's not A, whereas with a union type it's possible for the thing to be both A and B.

[RX14]

In crystal, the compiler always knows the concrete values of the type parameters of any generic before typing it. I really am interested in knowing more about what you said about union types being non compositional because I'm definitely not a type theorist. The crystal compiler wasn't written by type theorists and the typing algorithm is completely home-grown.

And regarding sum types I was just thinking syntactically instead of in terms of the type system.

[lmm]

> In crystal, the compiler always knows the concrete values of the type parameters of any generic before typing it.

Hmm. Does that mean you can't have a generic method in a separate compilation unit from where it gets used?

> I really am interested in knowing more about what you said about union types being non compositional because I'm definitely not a type theorist.

I'm not really a type theorist, I'm just thinking about e.g. if you have a method like:

    def doSomething[A](userSuppliedValue: A) = {
      val x = if(someCondition) Some(userSuppliedValue) else None
      x match {
        case Some(a) => y ...
        case None => z ...
      }
      x match {
        case None => v ...
        case Some(a) => w ...
      }
    }

then the compiler knows that if we take branch y we will also take branch w and if we take branch z we will also take branch v. Whereas if you do the same thing with an inclusive union type, that's true most of the time but not when userSuppliedValue is null.

[RX14]

We don't have compilation units, all code is compiled at once in Crystal. It's a little painful in terms of compile times with large codebases but nowhere near C++ compile times yet :) We're thinking about caching and various modifications to the crystal compiler to make compilation faster.

I'm confused by your example too. If you mean replacing matching None with testing for nil, then you'd have to replace Some(T) with an `else`, then the compiler absolutely can prove that if you take one branch you take the other - given that x is not assigned to (not sure why the compiler would want to prove that though). And after all that I'm not sure how your example relates to, or what you even mean by "noncompositional".

[lmm]

> I'm confused by your example too. If you mean replacing matching None with testing for nil, then you'd have to replace Some(T) with an `else`, then the compiler absolutely can prove that if you take one branch you take the other

If you use an inclusive union, the type of x becomes A | nil (or however you write it). The trouble is that you don't know whether A might also be a type that includes nil, and userSuppliedValue might be nil already. So if you write in match/case style your branching behaves inconsistently in that case (because x is both an A and a nil) - and if you write in "if(x == nil)" style then you can't infer that branch y will be taken when someCondition is true.

> And after all that I'm not sure how your example relates to, or what you even mean by "noncompositional".

What I mean is that viewing these types as type-level functions, they don't compose. For option/maybe-style types, composition works as expected: you can know the behaviour of X[Y[A]] by reasoning about X and Y independently. That doesn't work for inclusive unions, because whether A | nil is a different type from A depends on what type A is.