[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.

[RX14]

Ah! I understand completely now! Interestingly I've only very rarely noticed that being a problem in practice. I'm not quire sure what to say about it more than that because it's definitely a real problem but I haven't noticed it being a pain point in practice. Most type parameters in crystal are only used for collection APIs which never union the type parameter with nil.

[lmm]

Interesting. I imagine that's the Ruby influence - on paper at least, Crystal's featureset is almost ML-family, but sounds like the culture must be rather different.

Being able to move all your concerns into the type system is really nice, and the difference between a type system that does what you expect 95% of the time and one that does 100% of the time is huge - but I don't know any way to get there except gradually. I've been doing Scala for 8 years and it probably took 4 before I realised how important this stuff was even in the simple case of Option - and that's coming from a background of Java before then and already being dubious of things that step outside the type system.

Language inconsistencies matter, but only in large codebases, and by the time you have those large codebases it's probably too late to change the language. I think Scala gets a lot right, I think something like Idris gets more right. I can make the case for why those things are the right things in terms of theoretical purity/consistency. But when it comes to practical differences I don't know how to convince anyone other than by saying "go maintain a 300kloc system in an ML-family language for 5 years and see how much easier it is" :/.

Best of luck. I hope Crystal finds some things that work well, and that we all add something to the language design state of the art. I do think we're getting gradual progress and consensus - if nothing else, almost every new language has at least some form of sum typing and pattern matching these days - but I guess progress on the aspects that matter for big systems is inherently going to be slow, because it's only after we've built those big systems that we can see what's wrong (and what's right) with them.

[RX14]

Interestingly crystal has neither sum types or pattern matching (and it doesn't need them) :)

And yeah, nobody has any experience maintaining 300kloc+ systems in crystal. And i'm sure we get loads of things wrong and there are lots of pain points. I hope we find some type theorists to pick through the problems when that happens too, because crystal's type system is really quite different to anything I've ever seen before. And it would be nice to see what comes out of that theory wise.