Home » forums » LtU Forum

Resources for implementing higher-kinded types?

I’m working on a language and I would like to implement polymorphism over type constructors (for functor, applicative, monad, etc.) but I’m uncertain how to proceed.

Can anyone recommend tutorial-style resources or sample implementations of this? I’ve read that higher-order unification is involved, and that inference is undecidable without certain restrictions. Is that accurate? Would it be difficult to retrofit a (more or less) standard implementation of Hindley–Milner?

By Jon Purdy at 2016-11-09 05:04 | LtU Forum | previous forum topic | next forum topic | other blogs | 4376 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

See Mark Jones FPCA 1993 paper

A system of constructor classes: overloading and implicit higher-order polymorphism.

In the general case, like in Agda or Coq, you need higher order unification, but Jones's insight was that for ML/Haskell style type systems, you barely need to change anything at all.

His idea was to simply forbid type-level lambdas. Then the grammar of monotypes looks like:

    A ::= a | app(A,B) | A -> B | A * B | List A

Schemes look like:

   s ::= forall a:k. s | A

Note that none of these terms (a) have any binders in them, (b) have any reducible expressions.

This means that ordinary first-order unification works just fine -- you just have to keep track of the kinds of each type variable, so that you can check in the app constructor that the function and argument types match.

By neelk at Wed, 2016-11-09 10:45 | login or register to post comments

Thanks!

This is just what I was looking for. I had guessed that it would be so simple, but it’s reassuring to have some justification for that intuition.

We avoid the need to deal with polymorphic kinds by replacing any unknown part of an inferred kind with \(\ast\).

I think I can trivially deduce kinds for all type variables, because in my system most of them are already explicitly kinded. But in case I have to infer them, is defaulting really as simple as replacing all unsolved kind variables with \(\ast\) after inferring a kind? That is, if I infer \(k_1 \to k_2 \to \ast\), then can I just generalise to \(\forall k_1 k_2. k_1 \to k_2 \to \ast\) and instantiate to \(\ast \to \ast \to \ast\)?

By Jon Purdy at Wed, 2016-11-09 20:40 | login or register to post comments

Yep

In fact, you don't even need to generalize k1 -> k2 -> *, because once you've type checked your program, you can assign any concrete kind you like to k1 and k2. Haskell chooses * because (as of Haskell 98) the only base kind was *, but any choice will do.

By neelk at Fri, 2016-11-11 10:40 | login or register to post comments