I see PureScript has recently gotten kind polymorphism, along with a host of other goodies that I spent a lot of time thinking about. (I’m the author of -XTypeInType in GHC and have published a bunch of papers on fancy type systems. I’m eager to get dependent types in GHC.) It looks like https://github.com/purescript/purescript/pull/3779# was based largely off my work.
So I’d love to know more about your experience of these features in PureScript. You’ve had an opportunity to re-imagine these features in a new(er) language, with less historical baggage than GHC has. What aspects of this all were strange to you? What worked well? Have you had innovations you think GHC should take on?
One question, in particular: that GitHub ticket claims to use “Kind Inference for Datatypes” as inspiration. You’re ahead of GHC in that regard – we have not yet implemented that paper. Do you have any feedback that will be helpful when we do so?
Thanks. So glad to see these ideas implemented beyond Haskell!
Richard
I found the implementation based on “Kind Inference for Datatypes” to be straightforward. The paper was very clear and I enjoyed working through it. Thank you for the resource! PureScript’s type system in general is very conservative, so most changes were about reducing the “fanciness” of it . This is also based on my experience of implementing the draft from last July (I think?), so there may have been changes. For reference, here is the actual implementation.
In the paper there is a concept of local contexts. I believe this only exists to support quantification of free variables. PureScript does not quantify over free variables, so I did not implement anything like this, which made things like promotion much simpler.
I found this ticket to be essential reading for a number of issues.
I implemented “the quantification check” as part of generalization using dependency analysis to get better errors. It’s not clear to me that this check is necessary if you interleave inferred quantifiers with explicit quantifiers, however, which I thought I remember reading GHC does now.
A similar quantification check that I added was the “no unambiguous generalization check” for things like type SomeProxy = forall a. Proxy a where GHC uses Any. PureScript has nothing like Any and throws an error that asks the user to explicitly quantify something like this. This shows up (perhaps unintuitively) with anonymous record synonyms that might contain kind-polymorphic fields since we cannot just generalize these field signatures in an arbitrary synonym. We also disallow this in data types where GHC uses an existential. Partly because PureScript doesn’t support existentials, but I also think it’s just as dubious.
Basically anywhere GHC tries to use Any in the type-system, we throw some sort of generalization error.
I implemented a subsumption check to support higher-rank kinds, which required some minor changes to the instantiation judgement.
I had to do some unification in the elaboration judgment to support type wildcards. Wildcards are unknown types with unknown kinds, which can leak through to elaboration.
Most of the time and work probably went into integrating it with the constraint solver. I honestly have no idea how GHC’s solver works with PolyKinds, so it was largely about making it work intuitively with what we have (fundeps and instance chains).
You’ve had an opportunity to re-imagine these features in a new(er) language, with less historical baggage than GHC has. What aspects of this all were strange to you? What worked well? Have you had innovations you think GHC should take on?
Since this is all “hot off the presses”, I have not done much experimentation. We’ll have to see what the community rolls with once it’s released. What GHC baggage do you think has been the most constraining to you? PureScript has it’s own baggage, certainly, even if it’s not as old as GHC, but it has the advantage of being a much lighter compiler.
Yes. Local contexts are all about having some subset of variables that can be reordered, in order to generalize them in the correct order. If all type variables are explicitly introduced with a given order, then local contexts are unnecessary.
this ticket
Yes, that ticket (as you might guess) formed much of the background thought behind the paper. If memory serves, the paper started as an attempt to figure out what to do about that ticket.
This is a dark art, indeed. Some collaborators and I are hoping to write a paper about this, but I think the paper will focus on issues other than PolyKinds. You might find recent patch !2492 (Discourse won’t let me, a new user, turn this into a link) an interesting read. See specifically https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/typecheck/TcCanonical.hs#L2117, which explains it all. Happy to answer questions about the solver.
What GHC baggage do you think has been the most constraining to you?
The biggest, for me, is our terrible syntax for GADTs. When we say data T a where ..., the a should scope over the where bit! Dealing with implicit quantification is also a bit of a pain. For example, when we say f :: forall a. Proxy a -> (), we infer a new kind k for the type of a. The problem is that there really isn’t a way to disable that kind-generalization, and it sometimes gets in the way. To be honest, there aren’t specific pain points I was thinking of when writing that comment, but everything in GHC just always feels so big, and I wonder how much that tempers our enthusiasm.
We just don’t have GADTs . For generalization, we treat it uniformly as other generalization (ala “Let should not be generalized”), so this only occurs in a top-level context. Are you saying that GHC will generalize kinds in any context?
I greatly appreciate the leanness of PureScript’s compiler. The PureScript compiler isn’t really a research vessel, but it is a production-grade Haskell-like at a fraction of the size and complexity, so maybe there are educational opportunities there.
. This is also based on my experience of implementing the draft from last July (I think?), so there may have been changes. For reference,