[Haskell-cafe] [External] Resources on how to implement (Haskell 98) kind-checking?

[Ingle, Apoorv N]

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 <benjamin.redelings at gmail.com<mailto:benjamin.redelings at 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 at 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.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20211014/4fd2a9f5/attachment.html>