Resources on how to implement (Haskell 98) kind checking?

[Benjamin Redelings]

Hi Richard,

Many thanks for the hints!

On 10/15/21 1:37 PM, Richard Eisenberg wrote:
>
>>> 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.

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

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?

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

Yeah, that is a good point.  That clarified for me what GHC is doing.

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

OK, that makes sense.  I'll start with the mapping approach, and then 
consider optimizing things later.


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

Yes, I was definitely confusing zonking and zapping.  (Wow, lots of fun 
names here!)


> 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.
This was quite helpful -- I think I was trying to somehow avoid a 
separate pass over the AST.

But if that is a difficulty on the right road, I will just go for it.

-BenRI
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20211027/bab92692/attachment.html>