<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>