<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi Richard,</p>
<p>Many thanks for the hints!<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>
<blockquote type="cite" class="">
<div class="">
<div class="">
<blockquote type="cite" style="color: #007cff;" 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>
</div>
</blockquote>
<p>I was doing it all at once -- but I wasn't sure how to export the
information about 'b' from the procedure. (After you record the
kinds of the typecons like C, I believe the different typecons in
the recursive group become separable.)<br>
</p>
<p>I presume (in retrospect) that GHC modifies the declaration to
record the kind of b, and then re-walks the declaration to
substitute kind variables later?<br class="">
</p>
<blockquote type="cite"
cite="mid:010f017c8507c42b-13b49b21-3b8e-4a8d-93b6-56c60f61ed60-000000@us-east-2.amazonses.com">
<div>
<blockquote type="cite" class="">
<div class="">
<div 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>
</div>
</blockquote>
<p>Yeah, that is a good point. That clarified for me what GHC is
doing.<br>
</p>
<blockquote type="cite"
cite="mid:010f017c8507c42b-13b49b21-3b8e-4a8d-93b6-56c60f61ed60-000000@us-east-2.amazonses.com">
<div><br class="">
<blockquote type="cite" class="">
<div class="">
<div 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>
</blockquote>
<p>OK, that makes sense. I'll start with the mapping approach, and
then consider optimizing things later.</p>
<p><br>
</p>
<blockquote type="cite"
cite="mid:010f017c8507c42b-13b49b21-3b8e-4a8d-93b6-56c60f61ed60-000000@us-east-2.amazonses.com">
<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>
</div>
</blockquote>
<p>Yes, I was definitely confusing zonking and zapping. (Wow, lots
of fun names here!)</p>
<p><br>
</p>
<blockquote type="cite"
cite="mid:010f017c8507c42b-13b49b21-3b8e-4a8d-93b6-56c60f61ed60-000000@us-east-2.amazonses.com">
<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>
</blockquote>
This was quite helpful -- I think I was trying to somehow avoid a
separate pass over the AST.<br>
<p>But if that is a difficulty on the right road, I will just go for
it. <br>
</p>
<p>-BenRI<br>
</p>
</body>
</html>