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

[lmm]

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

Well, the use cases will be there, and any general-purpose language will need answers for them. One can of course achieve the same effect with other language features (e.g. Java's famous use of the "visitor pattern" for those cases), but there's a cost in verbosity and maintainability.

[RX14]

Crystal can essentially have a sum type by representing it as a union of different record types. It's not common to do in crystal though, at least not with 3+ union entries.

And pattern matching isn't really needed if you have flow typing + OO (at least I haven't found a usecase for pattern matching which crystal doesn't already have an answer to)

[lmm]

> Crystal can essentially have a sum type by representing it as a union of different record types. It's not common to do in crystal though, at least not with 3+ union entries.

Sum types usually only have two or three entries too.

> And pattern matching isn't really needed if you have flow typing + OO (at least I haven't found a usecase for pattern matching which crystal doesn't already have an answer to)

How does "flow typing + OO" solve the problem? You can use OO to emulate pattern matching via the visitor pattern, yes, but that's notoriously cumbersome; I don't see how flow typing makes any difference to that?