3 ms·
Yeah, we can consider `string`, `int` to both be subtypes of `string | int`, and `string & int` to be a subtype of both `string`, `int`. There are some problem
by sparkie 2y ago
Yeah, we can consider `string`, `int` to both be subtypes of `string | int`, and `string & int` to be a subtype of both `string`, `int`.
There are some problems with doing so though, such as inferring the types, but this can be mostly mitigated by giving types a polarity, as Dolan introduced in Algebraic Subtyping[1].
This can be a bit hard to wrap your head around at first because given a function `f : a -> b`, the parameter `a` has negative polarity and return type `b` has positive polarity, but in the function body, the polarities are reversed, and the argument becomes positive, with the result value being negative. Local variables are ambipolar as they can be both introduced and eliminated in the function body.
It becomes even more of a problem when you have types of kind `* -> *` or higher where the type argument can be covariant or contravariant. As far as I'm aware type inference for handling these in combination with algebraic subtyping is still an open problem.
[1]:https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/thesis.pdf https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/the...