Advice for implementing GADTs?

[Benjamin Redelings]

Thanks a bunch for this!

On 8/4/22 3:45 PM, Simon Peyton Jones wrote:
>
> QUESTION 1: Are there any obviously important resources that I've 
> overlooked?
>
> That's a good list.  Ningning's thesis https://xnning.github.io/ is 
> also good stuff.

Thanks!


> QUESTION 2: if my quick scan is correct, none of the papers mention 
> the GHC technique of determining untouchability by assigning "levels" 
> to type variables.  Is there any written paper (outside the GHC 
> sources) that discusses type levels?
> It is disgracefully undocumented, I'm afraid.  Sorry.  Didier Remy 
> used similar ideas, in some INRIA papers I think.

OK, that was my impression, just checking.  I think I get the basic idea...


> QUESTION 3: My impression is that:
>
> (a) type variable levels were introduced in order to clarify which 
> MetaTyVars are "untouchable", but
>
> (b) levels now also check that type variables do not escape their 
> quantification scope.
>
> (c) levels can also be used to figure out which variables are free in 
> the type environment, and therefore should not be generalized over.
>
> Does this sound right?  I suspect that I might be wrong about the last 
> one...
>
>
> Correct about all three.
>
Good to know!

> Except that a unification variable is only untouchable if it comes 
> from an outer level *and* there are some intervening Given 
> equalities.   If there are no equalities it's not untouchable.  E.b.
>
>    f = \x -> case x of
> Just y -> 3::Int
>
> Here the (3::Int) can affect the result type of the function because 
> the Just pattern match does not bind any Given equalities (in a GADT 
> like way).
>
3.1: OK, so if the case branch introduces type-class constraints, but 
not equality constraints, then the unification variables from an outer 
level are still touchable?  Presumably because the type-class 
constraints don't interact with the equality constraints?

3.2: The OutsideIn paper talks about creating implication constraints, 
which then bubble UP to the level where the solver is applied.  Maybe 
only at the outermost level?

However, it sounds like GHC pushes given constraints from a GADT pattern 
match DOWN into the case branch.  Implication constraints would only be 
created if the wanted constraints bubble up to a GADT pattern match, and 
are not entailed by the givens.  So

* implication constraints like (a ~ Int ==> a ~ Int) are never created.

* however, implication constraints like (a ~ Int ==> b ~ Int) could be 
created.

I may be assuming that GHC runs the solver for each GADT pattern match 
before creating implication constraints.

Does that sound right?

3.3: Also, is there a standard way to pretty-print implication 
constraints?  The OutsideIn paper uses LaTeX \supset I think, but there 
isn't an obvious ASCII character to use to for \supset...


> I keep meaning to write an updated version of Practical type inference 
> for arbitrary rank types 
> <https://www.microsoft.com/en-us/research/publication/practical-type-inference-for-arbitrary-rank-types/>, 
> but failing to get around to it!
>
That would be great, if you find the time!  Are you thinking of adding 
practical steps for handling equality constraints to it? Or, removing 
the deep-subsumption language?  Or something else? It has already been 
quite helpful.

-BenRI

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20220815/8f13619b/attachment.html>