<div dir="auto">I believe you can treat kind chekcing /inference in the H98 setting as another instance of hindley Milner type inference where the types are the terms, and kinds are the types.  And where there are no user lambdas.  So it’s only “combinator” definitions as introduced by user defined type class and type and data definitions.  </div><div dir="auto"><br></div><div dir="auto">Moreover, I think you can limit yourself to considering it a sort of  simply typed calculus for the purposes of using a unification approach.  ESP since poly kinds aren’t there. </div><div dir="auto"><br></div><div dir="auto">I hope that helps, but if not please ask more!</div><div dir="auto"><br></div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Oct 12, 2021 at 3:37 PM Benjamin Redelings <<a href="mailto:benjamin.redelings@gmail.com">benjamin.redelings@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
1. I'm looking for resources that describe how to implement kind Haskell <br>
98 checking.  Does anyone have any suggestions?<br>
<br>
* I've looked at the PolyKinds paper, but it doesn't cover type classes.<br>
<br>
* I've looked at the source code to GHC, but it is hard to follow for a <br>
variety of reasons.  It isn't laid out like an algorithm description, <br>
and the complexity to handle options like PolyKinds and DataKinds makes <br>
the code harder to follow.<br>
<br>
<br>
2. One question that came up is how to handle type variables that are <br>
present in class methods, but are not type class parameters. If there <br>
are multiple types/classes in a single recursive group, the kind of such <br>
type variables might not be fully resolved until a later type-or-class <br>
is processed.  Is there a recommended approach?<br>
<br>
I can see two ways to proceed:<br>
<br>
i) First determine the kinds of all the data types, classes, and type <br>
synonyms.  Then perform a second pass over each type or class to <br>
determine the kinds of type variables (in class methods) that are not <br>
type class parameters.<br>
<br>
ii) Alternatively, record the kind of each type variable as it is <br>
encountered -- even though such kinds may contain unification kind <br>
variables.  After visiting all types-or-classes in the recursive group, <br>
replace any kind variables with their definition, or with a * if there <br>
is no definition.<br>
<br>
I've currently implement approach i), which requires doing kind <br>
inference on class methods twice.  Is this the recommended approach?<br>
<br>
<br>
3. Also, is Haskell 98 kind checking the same as Haskell 2010 kind checking?<br>
<br>
-BenRI<br>
<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div></div>