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.

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

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

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

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.

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.

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.

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

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)

> 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?

Pattern matching, at least in functional languages, is mainly used both as control flow to match on the type of arguments, and also to destructure data structures. In flow typing you replace the control flow part of pattern matching with `if x.is_a? Type` and since everything you can do to an object is just passing a message to it (thanks to ruby's smalltalk origins), you don't really need the destructuring since you can just then use `foo.bar`.

Crystal has method overloading (dynamic dispatch), which is a form of pattern matching (but not destructuring) but that's it. So I guess we have pattern matching but definitely not to the extent say haskell or elixir has it.

Visitor pattern in Crystal is just a class with a bunch of `def visit(node : Type)` and then just call `visit(foo)` and let dynamic dispatch handle the rest. The visited data structure has no knowledge about the visitor.

> In flow typing you replace the control flow part of pattern matching with `if x.is_a? Type`

Hmm, I guess flow typing lets you do an exhaustiveness check of an if-else style set of cases. Still seems like a syntactic shortcut would be nice, just as one misses "switch" in Python.

Yeah, crystal has one of those (and it's about to gain exhaustiveness checking), so I didn't literally always mean `if/else` :)

If you can switch on the type of a variable and have it have the relevant type within each switch arm I'd consider that to be pattern matching, though I guess that's just semantics.