You might also find this talk helpful.
https://www.microsoft.com/en-us/research/publication/type-inference-as-const...
And this paper: https://www.microsoft.com/en-us/research/publication/outsideinx-modular-type...
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.
You might also enjoy Ningning Xie's thesis,
https://xnning.github.io/papers/Thesis.pdf
and her paper "Kind inference for data types"
https://xnning.github.io/papers/kind-inference.pdf
which are all about kind inference.
Simon
PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.)
| -----Original Message-----
| From: Haskell-Cafe On Behalf Of
| Benjamin Redelings
| Sent: 14 October 2021 15:14
| To: Haskell Cafe
| Subject: Re: [Haskell-cafe] Resources on how to implement (Haskell 98)
| kind-checking?
|
| 4. So, apparently GHC takes neither of these options, instead it does:
|
| iii) Represent kinds with modifiable variables. Substitution can be
| implemented by modifying kind variables in-place. This is called
| "zonking" in the GHC sources.
|
| This solves a small mystery for me, since I previously think that
| zonking was replacing remaining kind variables with '*'. And indeed
| this seems to be an example of zonking, but not what zonking is.
|
| 5. It turns out that the Technical Supplement to the PolyKinds paper
| (Kind Inference for Datatypes) does have more detail.
|
| -BenRI
|
|
|
| On 10/12/21 3:35 PM, Benjamin Redelings wrote:
| > Hi,
| >
| > 1. I'm looking for resources that describe how to implement kind
| > Haskell 98 checking. Does anyone have any suggestions?
| >
| > * I've looked at the PolyKinds paper, but it doesn't cover type
| classes.
| >
| > * I've looked at the source code to GHC, but it is hard to follow
| for
| > a variety of reasons. It isn't laid out like an algorithm
| > description, and the complexity to handle options like PolyKinds and
| > DataKinds makes the code harder to follow.
| >
| >
| > 2. One question that came up is how to 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.
| >
| > 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. Is this the recommended approach?
| >
| >
| > 3. Also, is Haskell 98 kind checking the same as Haskell 2010 kind
| > checking?
| >
| > -BenRI
| >
| >
| _______________________________________________
| Haskell-Cafe mailing list
| To (un)subscribe, modify options or view archives go to:
| https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.
| haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fhaskell-
| cafe&data=04%7C01%7Csimonpj%40microsoft.com%7Ca5f05a143187488dc9e9
| 08d98f1cf5fc%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637698177117
| 544440%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJ
| BTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=nbrfIYORY0IfrnCIv4OAY89Bn
| wdd6QjWNhWuGYm3Ngk%3D&reserved=0
| Only members subscribed via the mailman list are allowed to post.
