<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi,
<br>
<br>
I asked about this on Haskell-Cafe, and was recommended to ask
here instead. Any help is much appreciated!<br>
<br>
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:
<br>
<br>
* 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:<br>
<br>
C :: k' -> k and C' :: k' => C C' :: k <br>
</p>
<p>* The THIH paper doesn't have an algorithm for kind checking. It
assumes that every type variable already has a kind. <br>
</p>
<p>* The 2010 Report helpfully mentions substituting any remaining
kind variables with *. But it refers to "A system of constructor
classes" for an algorithm.<br>
</p>
<p>* 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 -> *.
<br>
<br>
* 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. <br>
</p>
<p><br>
<br>
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:
<br>
<br>
</p>
<blockquote type="cite" style="color: #007cff;">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?
<br>
<br>
I can see two ways to proceed:
<br>
<br>
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.
<br>
<br>
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.
<br>
<br>
I've currently implement approach i), which requires doing kind
inference on class methods twice.
<br>
<br>
</blockquote>
Further investigation revealed that GHC takes yet another approach
(I think):
<br>
<br>
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.
<br>
<br>
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).
<br>
<br>
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...<br>
<p><br>
</p>
<p><br>
</p>
3. I'm curious now how many other pieces of software besides GHC
have implemented kind inference...
<br>
<br>
<br>
-BenRI
<br>
</body>
</html>