There are a number of type system features which Haskell has and PureScript currently doesn’t, and which some people might want to see in PureScript one day. For example:
- existential types
- Type families
- Data kinds
- Coercible and DerivingVia
- Constraint kinds
- Kind polymorphism
- Pi types
Note that some of these are subsumed by others, eg GADTs subsume existential types.
I am beginning to feel that it may be worth clarifying a stance on whether or not we want PureScript to get these features, that is, distinguishing “we do not want to add this because of reasons X, Y, Z” from “this would be nice to have but we just haven’t gotten around to it yet.”
Firstly, I want to draw attention to the fact that we do not have anywhere near the resources or expertise that GHC does for implementing and maintaining these kinds of features (or at least, this is my impression). For example, there is a long standing bug in kind unification which we haven’t yet gotten around to fixing.
Because of this, I would like us to be much more conservative about adding type level features than, say, GHC Haskell is. Any big type level feature is probably not only a fair bit of effort to implement in the first place, but also potentially a large maintenance burden, especially if, say, a few months after initial release, we find a serious bug in a feature which we struggle to fix but cannot remove because a chunk of the ecosystem has come to rely on it.
I also think there’s a lot to be said for having a smaller language with fewer features: the more features there are, the more you need to learn if you want to make the best use of the ecosystem, the more scope there is for those features to interact poorly with each other, and the more effort is going to be required to specify the language (if we ever get around to that).
I think a particularly convincing example of the utility of ruling out some particular type system feature is when that allows library authors to make stronger assumptions about what can safely be done. For example, all type constructors in PureScript are injective; this allows library authors to safely provide functions such as
lowerLeibniz. As I understand it, adding type families would invalidate this reasoning.
So hopefully you can now see where I’m coming from when I say I’d like to start ruling out type system features.
In particular, since we have an open PR implementing Coercible, I think now would be a good opportunity to raise the possibility of committing to not adding type families. Also, if we want to implement existential types, I think we should commit to not adding GADTs, since GADTs subsume existential types; if we had both GADTs and existential types, we’d have two different and probably incompatible ways of doing the exact same thing.
What do you all think? Does this all sound sensible or am I missing something?
Some other relevant posts (both by @paf31, as it happens) which have helped shape my thoughts here: