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

[Benjamin Redelings]

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 
>> <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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20211014/6f50e37d/attachment.html>