Help getting PolyKinds over the line

language
#1

Hi, everyone. I’ve been working on adding PolyKinds to the compiler. You can see the state of the branch here: https://github.com/natefaubion/purescript/tree/polykinds

Overall it is in a good state. This branch implements TypeInType, and will infer and check against polymorphic data types like:

data Proxy a = Proxy
Proxy :: forall (k :: Type). k -> Type

This of course is desirable because it lets us eliminate the zoo of proxy types we have, and will also let us use Row constraints with things other than Type. This also fixes existing bugs in the kind checker, where it is not checking things when it should.

I haven’t been able to take this over the line yet due to life circumstances, and there are a few big things left to take care of.


One big issue remaining is dealing with classes and instances for polykinded data types. If you take Proxy as an example, it has Functor instances. However, due to the signatures of the class members, the instance is actually for Proxy @Type. Currently, elaborated kinds like this are not directly available to the solver, so it will fail to find this instance. It’s not clear to me if I can hydrate these elaborated type from the desugared class and instance declarations, or if we definitely need to kind elaborate the source class and instance declarations and put that in the environment. This requires some investigative work, and potentially extending the kind checker for these other forms.

Error reporting needs to be cleaned up in the kind checker. Right now there are still quite a bit of internalError placeholders, and they should be replaced with actual errors. We also need to insert more type checking hints in the log, so you can get a good stack trace in any errors.

We need to extend the type declaration syntax to support full kind signatures (like foreign import data but for regular data types as well), and adjust the checker accordingly (this is a topo-sort issue).

We need to potentially extend externs with this information. I have not fully investigated what the effects would be.

We need to benchmark the compiler to see if there’s anything we need to tune. I would like for this to not regress considerably in performance.


If anyone is interested in seeing this feature land and would like to help out, I can offer guidance. If not, then it might just take a little while :laughing:. Thanks!

17 Likes