That's the only way I've ever seen it implemented. If you're proposing some idea for having null in the type system as a normal type (that doesn't boil down to just being equivalent to Option/Maybe), can you be more concrete?
Being able to create arbitrary union types between different types, like crystal (which I work on). The difference between that and option/maybe is that it ends up playing nicely with flow typing without any special cases for optional/maybe in the flow typing.
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?)
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?
> 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.
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.
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.
