Oh, I forgot to add, would it make sense to put some of the information
I discovered about implementing kind checking into the wiki somewhere?
I am mostly thinking of a sequence of steps like:
1. Divide class, data/newtype, type synonym, and instance declarations
into recursive groups.
1a) Record for each group which LOCAL typecons are mentioned in the
declaration
1b) ... etc
2. Infer kinds within a recursive group
2a) Treat type classes as having kind k1 -> k2 -> ... -> kn -> Constraint
2b) Begin by recording a kind k1 -> k2 -> ... -> kn -> Constraint/* for
each typecon
2c) etc...
2d) Substitute kind variables (zonking)
2e) Substitute * for remaining kind variables (zapping)
3. ...
I am not actually sure what to write yet, the above is just an illustration.
It might also help to reference the relevant papers (mostly the
PolyKinds paper), and maybe also to mention papers like the THIH paper
that don't actually implement kind checking.
-BenRI
On 10/15/21 1:37 PM, Richard Eisenberg wrote:
On Oct 14, 2021, at 11:59 AM, Benjamin Redelings
<benjamin.redeli...@gmail.com> wrote:
I asked about this on Haskell-Cafe, and was recommended to ask here
instead. Any help is much appreciated!
I saw your post over there, but haven't had time to respond.... but
this retelling of the story makes it easier to respond, so I'll do so
here.
* 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 -> *.
What is unique about type classes? It seems like you're worried about
locally quantified type variables in method types, but (as far as kind
inference is concerned) those are very much like existential variables
in data constructors. So perhaps take the bit about existential
variables from the PolyKinds part of that paper and combine it with
the Haskell98 part.
It's true that many implementors may find the notation in that paper
to be a barrier, but you just have to read the rules clockwise,
starting from the bottom left and ending on the bottom right. :)
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.
This won't work.
class C a where
meth :: a b -> b Int
You have to know the kind of local b to learn the kind of
class-variable a. So you have to do it all at once.
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.
I don't really see the difference between (ii) and (iii). Maybe (ii)
records the kinds in a table somewhere, while (iii) records them "in"
the kind variables themselves, but that's not so different, I think.
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).
We can imagine that, instead of mutation, we build a substitution
mapping unification variables to types (or kinds). This would be
stored just as a simple mapping or dictionary structure. No mutation.
As we learn about a unification variable, we just add to the mapping.
If we did this, zonking would be the act of applying the substitution,
replacing known unification variables with their values. It just so
happens that GHC builds a mapping by using mutable cells in memory,
but that's just an implementation detail: zonking is still just
applying the substitution.
Zonking does /not/ replace anything with *. Well, functions that have
"zonk" in their name may do this. But it is not really logically part
of the zonking operation. If you like, you can pretend that, after
zonking a program, we take a separate pass replacing any yet-unfilled
kind-level unification variables with *. Sometimes, this is called
"zapping" in GHC, I believe.
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...
Zonking is a bit laborious to implement, but not painful. Laborious,
because it requires a full pass over the AST. Not painful, because all
it's trying to do is replace type/kind variables with substitutions:
each individual piece of the puzzle is quite simple.
I hope this is helpful!
Richard
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
