Thanks!  Good point. For kind inference, I think that point won't come in to play unless I add CUSK's, which are not yet on the radar.  For type-inference though that is a good point. -BenRI On 10/13/21 8:58 AM, David Feuer wrote:

Haskell 2010 defines virtually the same language as Haskell 98. The differences are too trivial to worry about. One spot you may wish to follow GHC (and I think Hugs, at least) rather than the Report: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/bugs.html#typechecking-of...

On Tue, Oct 12, 2021, 3:37 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: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Along with what Emil suggests, Sec 4. of A system of constructor classes: overloading and implicit higher-order polymorphism[1] may also be useful. — Apoorv [1]: http://web.cecs.pdx.edu/~mpj/pubs/fpca93.pdf On Oct 13, 2021, at 14:22, Emil Axelsson <78emil@gmail.commailto:78emil@gmail.com> wrote: Maybe Typing Haskell in Haskellhttp://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf is what you're looking for? / Emil Den 2021-10-12 kl. 21:35, skrev Benjamin Redelings: 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: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

At this point you might want to ask on ghc-devs. They might ask you to document what you find out, though. On Thu, Oct 14, 2021 at 10:25 AM Benjamin Redelings < benjamin.redelings@gmail.com> wrote:

Thanks! Yes, that introduces the idea that requires kind inference.

Interestingly, it contains a (kind-aware) type-inference algorithm, but no kind inference algorithm!

Perhaps kind-inference is considered too "obvious" to require an algorithm. The closest it comes is the rule:

C :: k' -> k and C' :: k' => C C' :: k

This is helpful, but it would probably be beneficial for better documentation to exist SOMEWHERE.

-BenRI On 10/13/21 3:49 PM, Ingle, Apoorv N wrote:

Along with what Emil suggests, Sec 4. of A system of constructor classes: overloading and implicit higher-order polymorphism[1] may also be useful.

— Apoorv

[1]: http://web.cecs.pdx.edu/~mpj/pubs/fpca93.pdf

On Oct 13, 2021, at 14:22, Emil Axelsson <78emil@gmail.com> wrote:

Maybe Typing Haskell in Haskell http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf is what you're looking for?

/ Emil

Den 2021-10-12 kl. 21:35, skrev Benjamin Redelings:

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: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- brandon s allbery kf8nh allbery.b@gmail.com

And I happened to bump into Sec 4. of Kind Inference for Datatypes[1] It atleast has the heading kind checking for H98 — Apoorv [1]: https://arxiv.org/abs/1911.06153 On Oct 14, 2021, at 09:24, Benjamin Redelings mailto:benjamin.redelings@gmail.com> wrote: Thanks! Yes, that introduces the idea that requires kind inference. Interestingly, it contains a (kind-aware) type-inference algorithm, but no kind inference algorithm! Perhaps kind-inference is considered too "obvious" to require an algorithm. The closest it comes is the rule: C :: k' -> k and C' :: k' => C C' :: k This is helpful, but it would probably be beneficial for better documentation to exist SOMEWHERE. -BenRI On 10/13/21 3:49 PM, Ingle, Apoorv N wrote: Along with what Emil suggests, Sec 4. of A system of constructor classes: overloading and implicit higher-order polymorphism[1] may also be useful. — Apoorv [1]: http://web.cecs.pdx.edu/~mpj/pubs/fpca93.pdf On Oct 13, 2021, at 14:22, Emil Axelsson <78emil@gmail.com> wrote: Maybe Typing Haskell in Haskell is what you're looking for? / Emil Den 2021-10-12 kl. 21:35, skrev Benjamin Redelings: 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: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

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.