<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>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:</p>
<p>1. Divide class, data/newtype, type synonym, and instance
declarations into recursive groups.</p>
<p>1a) Record for each group which LOCAL typecons are mentioned in
the declaration</p>
<p>1b) ... etc</p>
<p>2. Infer kinds within a recursive group</p>
<p>2a) Treat type classes as having kind k1 -> k2 -> ... ->
kn -> Constraint</p>
<p>2b) Begin by recording a kind k1 -> k2 -> ... -> kn
-> Constraint/* for each typecon</p>
<p>2c) etc...</p>
<p>2d) Substitute kind variables (zonking)</p>
<p>2e) Substitute * for remaining kind variables (zapping)<br>
</p>
<p>3. ...</p>
<p>I am not actually sure what to write yet, the above is just an
illustration.</p>
<p>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.<br>
</p>
<p>-BenRI<br>
</p>
<div class="moz-cite-prefix">On 10/15/21 1:37 PM, Richard Eisenberg
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:010f017c8507c42b-13b49b21-3b8e-4a8d-93b6-56c60f61ed60-000000@us-east-2.amazonses.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Oct 14, 2021, at 11:59 AM, Benjamin Redelings
<<a href="mailto:benjamin.redelings@gmail.com"
class="moz-txt-link-freetext" moz-do-not-send="true">benjamin.redelings@gmail.com</a>>
wrote:</div>
<div class="">
<div class="">
<p class=""><br class="">
I asked about this on Haskell-Cafe, and was recommended
to ask here instead. Any help is much appreciated!<br
class="">
</p>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>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.</div>
<br class="">
<blockquote type="cite" class="">
<div class="">
<div class="">
<p class="">* 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 class="">
</p>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>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.</div>
<div><br class="">
</div>
<div>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. :)</div>
<blockquote type="cite" class="">
<div class="">
<div class="">
<p class=""><br class="">
</p>
<p class=""> 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 class="">
<br class="">
</p>
<blockquote type="cite" style="color: #007cff;" class="">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
class="">
<br class="">
I can see two ways to proceed: <br class="">
<br class="">
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 class="">
</blockquote>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>This won't work.</div>
<div><br class="">
</div>
<div>class C a where</div>
<div> meth :: a b -> b Int</div>
<div><br class="">
</div>
<div>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.</div>
<br class="">
<blockquote type="cite" class="">
<div class="">
<div class="">
<blockquote type="cite" style="color: #007cff;" class="">
<br class="">
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 class="">
<br class="">
I've currently implement approach i), which requires
doing kind inference on class methods twice. <br
class="">
<br class="">
</blockquote>
Further investigation revealed that GHC takes yet another
approach (I think): <br class="">
<br class="">
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 class="">
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>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.</div>
<br class="">
<blockquote type="cite" class="">
<div class="">
<div class=""> <br class="">
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
class="">
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>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.</div>
<div><br class="">
</div>
<div>Zonking does <i class="">not</i><span style="font-style:
normal;" class=""> 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.</span></div>
<br class="">
<blockquote type="cite" class="">
<div class="">
<div class=""> <br class="">
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 class="">
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>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.</div>
</div>
<br class="">
<div class="">I hope this is helpful!</div>
<div class="">Richard</div>
</blockquote>
</body>
</html>