<div dir="ltr"><div>Hi Benjamin,<br><br>Glad to know that you're looking at the kind inference algorithm for Haskell! Hope you enjoyed our kind inference paper and its technical supplement. <br><br>As mentioned in the email thread, for Haskell 98, the type inference algorithm is essentially a variant of type inference for simply typed lambda calculus (STLC), as kinds are only *, * -> *, etc (as analogous to int, int -> int, etc in STLC). To me, the most exciting parts of Haskell 98 kind inference are (1) pinpointing precisely what happens to mutually recursive declarations, (2) the formalism of "defaulting" (i.e., what happens to unconstrained kind unification variables when you have no polymorphism? In Haskell 98, they are by default solved by *), and (3) the subtle interaction between (1) and (2): you got different kinds for a declaration depending on whether or not it is mutually recursive with another declaration (as explained in Section 4.3 in the kind inference paper).<br><br></div><div>In the related work (Section 9) of the kind inference paper we have also compared with the paper "A system of constructor classes: overloading and implicit higher-order polymorphism" in terms of the kind inference algorithm. You might find the paragraph helpful:</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Jones [1995] proposed a homogeneous kind-preserving unification between two types. Kinds κ are defined only as * or κ1 → κ2. As the kind system is much simpler, kind-preserving unification ≈κ is simply subscripted by the kind, and working out the kinds is straightforward. Our unification subsumes Jones’s algorithm.</blockquote><div><div><br>My thesis contains further explanations and clarifications for the idea of "promotion" used in the paper. Please feel free to let me know if you have any questions and I'd be happy to help!<br></div><div><br></div></div><div>Cheers,</div><div>Ningning</div><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 14 Oct 2021 at 22:48, Simon Peyton Jones via Haskell-Cafe <<a href="mailto:haskell-cafe@haskell.org" target="_blank">haskell-cafe@haskell.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">You might also find this talk helpful.<br>
<a href="https://www.microsoft.com/en-us/research/publication/type-inference-as-constraint-solving-how-ghcs-type-inference-engine-actually-works/" rel="noreferrer" target="_blank">https://www.microsoft.com/en-us/research/publication/type-inference-as-constraint-solving-how-ghcs-type-inference-engine-actually-works/</a><br>
<br>
And this paper: <a href="https://www.microsoft.com/en-us/research/publication/outsideinx-modular-type-inference-with-local-assumptions/" rel="noreferrer" target="_blank">https://www.microsoft.com/en-us/research/publication/outsideinx-modular-type-inference-with-local-assumptions/</a><br>
<br>
The former is in tutorial form, but lacks a proper paper to back it up. The latter is a proper paper, but its focus is on *local* constraints which is more than you need right now.<br>
<br>
You might also enjoy Ningning Xie's thesis,<br>
<a href="https://xnning.github.io/papers/Thesis.pdf" rel="noreferrer" target="_blank">https://xnning.github.io/papers/Thesis.pdf</a><br>
and her paper "Kind inference for data types" <br>
<a href="https://xnning.github.io/papers/kind-inference.pdf" rel="noreferrer" target="_blank">https://xnning.github.io/papers/kind-inference.pdf</a><br>
which are all about kind inference. <br>
<br>
Simon<br>
<br>
PS: I am leaving Microsoft at the end of November 2021, at which point <a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a> will cease to work. Use <a href="mailto:simon.peytonjones@gmail.com" target="_blank">simon.peytonjones@gmail.com</a> instead. (For now, it just forwards to <a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>.)<br>
<br>
| -----Original Message-----<br>
| From: Haskell-Cafe <<a href="mailto:haskell-cafe-bounces@haskell.org" target="_blank">haskell-cafe-bounces@haskell.org</a>> On Behalf Of<br>
| Benjamin Redelings<br>
| Sent: 14 October 2021 15:14<br>
| To: Haskell Cafe <<a href="mailto:haskell-cafe@haskell.org" target="_blank">haskell-cafe@haskell.org</a>><br>
| Subject: Re: [Haskell-cafe] Resources on how to implement (Haskell 98)<br>
| kind-checking?<br>
| <br>
| 4. So, apparently GHC takes neither of these options, instead it does:<br>
| <br>
| iii) Represent kinds with modifiable variables. Substitution can be<br>
| implemented by modifying kind variables in-place. This is called<br>
| "zonking" in the GHC sources.<br>
| <br>
| This solves a small mystery for me, since I previously think that<br>
| zonking was replacing remaining kind variables with '*'. And indeed<br>
| this seems to be an example of zonking, but not what zonking is.<br>
| <br>
| 5. It turns out that the Technical Supplement to the PolyKinds paper<br>
| (Kind Inference for Datatypes) does have more detail.<br>
| <br>
| -BenRI<br>
| <br>
| <br>
| <br>
| On 10/12/21 3:35 PM, Benjamin Redelings wrote:<br>
| > Hi,<br>
| ><br>
| > 1. I'm looking for resources that describe how to implement kind<br>
| > Haskell 98 checking. Does anyone have any suggestions?<br>
| ><br>
| > * I've looked at the PolyKinds paper, but it doesn't cover type<br>
| classes.<br>
| ><br>
| > * I've looked at the source code to GHC, but it is hard to follow<br>
| for<br>
| > a variety of reasons. It isn't laid out like an algorithm<br>
| > description, and the complexity to handle options like PolyKinds and<br>
| > DataKinds makes the code harder to follow.<br>
| ><br>
| ><br>
| > 2. One question that came up is how to handle type variables that<br>
| are<br>
| > present in class methods, but are not type class parameters. If<br>
| there<br>
| > are multiple types/classes in a single recursive group, the kind of<br>
| > such type variables might not be fully resolved until a later<br>
| > 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<br>
| type<br>
| > synonyms. Then perform a second pass over each type or class to<br>
| > determine the kinds of type variables (in class methods) that are<br>
| not<br>
| > type class parameters.<br>
| ><br>
| > ii) Alternatively, record the kind of each type variable as it is<br>
| > encountered -- even though such kinds may contain unification kind<br>
| > variables. After visiting all types-or-classes in the recursive<br>
| > group, replace any kind variables with their definition, or with a *<br>
| > if there is no definition.<br>
| ><br>
| > I've currently implement approach i), which requires doing kind<br>
| > inference on class methods twice. Is this the recommended approach?<br>
| ><br>
| ><br>
| > 3. Also, is Haskell 98 kind checking the same as Haskell 2010 kind<br>
| > checking?<br>
| ><br>
| > -BenRI<br>
| ><br>
| ><br>
| _______________________________________________<br>
| Haskell-Cafe mailing list<br>
| To (un)subscribe, modify options or view archives go to:<br>
| <a href="https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail" rel="noreferrer" target="_blank">https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail</a>.<br>
| <a href="http://haskell.org" rel="noreferrer" target="_blank">haskell.org</a>%2Fcgi-bin%2Fmailman%2Flistinfo%2Fhaskell-<br>
| cafe&data=04%7C01%7Csimonpj%<a href="http://40microsoft.com" rel="noreferrer" target="_blank">40microsoft.com</a>%7Ca5f05a143187488dc9e9<br>
| 08d98f1cf5fc%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637698177117<br>
| 544440%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJ<br>
| BTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=nbrfIYORY0IfrnCIv4OAY89Bn<br>
| wdd6QjWNhWuGYm3Ngk%3D&reserved=0<br>
| Only members subscribed via the mailman list are allowed to post.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>
</div>