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 <haskell-cafe-bounces@haskell.org> On Behalf Of | Benjamin Redelings | Sent: 14 October 2021 15:14 | To: Haskell Cafe <haskell-cafe@haskell.org> | 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.