Resources on how to implement (Haskell 98) kind checking?

[Benjamin Redelings]

Hi,

I asked about this on Haskell-Cafe, and was recommended to ask here 
instead.  Any help is much appreciated!

1. I'm looking for resources that describe how to implement kind Haskell 
98 checking.  Does anyone have any good suggestions?  So far, the papers 
that I've looked at all fall short in different ways:

* Mark Jones's paper "A system of constructor classes":  This paper 
contains a kind-aware type-inference algorithm, but no kind inference 
algorithm.  The closest it comes is the rule:

     C :: k' -> k   and   C' :: k'   =>   C C' :: k

* The THIH paper doesn't have an algorithm for kind checking.  It 
assumes that every type variable already has a kind.

* The 2010 Report helpfully mentions substituting any remaining kind 
variables with *.  But it refers to "A system of constructor classes" 
for an algorithm.

* The PolyKinds paper was the most helpful thing I've found, but it 
doesn't cover type classes.  I'm also not sure that all implementers can 
follow algorithm descriptions that are laid out as inference rules, but 
maybe that could be fixed with a few hints about how to run the rules in 
reverse.  Also, in practice I think an implementer would want to follow 
GHC in specifying the initial kind of a data type as k1 -> k2 -> ... kn 
-> *.

* I've looked at the source code to GHC, and some of the longer notes 
were quite helpful.  However, it is hard to follow for a variety of 
reasons.  It isn't laid out like an algorithm description, and the 
complexity to handle options like PolyKinds and DataKinds makes the code 
harder to follow.



2. The following question (which I have maybe kind of answered now, but 
could use more advice on) is an example of what I am hoping such 
documentation would explain:

> Q: How do you handle type variables that are present in class methods, 
> but are not type class parameters? If there are multiple types/classes 
> in a single recursive group, the kind of such type variables might not 
> be fully resolved until a later type-or-class is processed.  Is there 
> a recommended approach?
>
> I can see two ways to proceed:
>
> i) First determine the kinds of all the data types, classes, and type 
> synonyms.  Then perform a second pass over each type or class to 
> determine the kinds of type variables (in class methods) that are not 
> type class parameters.
>
> ii) Alternatively, record the kind of each type variable as it is 
> encountered -- even though such kinds may contain unification kind 
> variables.  After visiting all types-or-classes in the recursive 
> group, replace any kind variables with their definition, or with a * 
> if there is no definition.
>
> I've currently implement approach i), which requires doing kind 
> inference on class methods twice.
>
Further investigation revealed that GHC takes yet another approach (I 
think):

iii) Represent kinds with modifiable variables.  Substitution can be 
implemented by modifying kind variables in-place.  This is (I think) 
called "zonking" in the GHC sources.

This solves a small mystery for me, since I previously thought that 
zonking was just replacing remaining kind variables with '*'.  And 
indeed this seems to be an example of zonking, but not what zonking is 
(I think).

Zonking looks painful to implement, but approach (i) might require 
multiple passes over types to update the kind of type variables, which 
might be worse...



3. I'm curious now how many other pieces of software besides GHC have 
implemented kind inference...


-BenRI
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20211014/94ca3864/attachment.html>