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. 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. 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. 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). 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-inferenc..., but failing to get around to it! Simon On Fri, 29 Jul 2022 at 17:08, Benjamin Redelings < benjamin.redelings@gmail.com> wrote:

Hi,

I've been working on implementing the Haskell type system for my specialized Haskell interpreter. I have now constructed a system that can type-check and run Haskell code that contains explicit type signatures, type constraints, and arbitrary-rank types.

I'm now thinking that I may need to implement GADTs -- i.e. constructors that introduce local constraints, including equality constraints. I'm looking at the paper "OutsideIn(X): Modular type inference with local assumptions" from 2011. I have three questions about implementing GADTs -- I'd be grateful for answers to any of them.

QUESTION 1: Are there any obviously important resources that I've overlooked?

The 2011 OutsideIn paper mentions several previous papers that seem quite helpful:

* Peyton Jones el at 2006. Simple Unification-based type inference for GADTs

* Schrijvers etal 2007. Towards open type functions for Haskell

* Peyton Jones et al 2004. Wobbly Types: etc.

* Schrijvers et al 2008. Type checking with open type functions.

* Shrijvers et al 2009. Complete and decidable type inference for GADTs

* Vytiniotis et al 2010. Let should not be generalized.

And of course the GHC source code. (I'm not looking at coercions at the present time, because my type-checker translates to the plain lambda calculus without type annotations, not system F or F_C. Hopefully I can remedy this later...)

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?

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...

Thanks again, and sorry for the long e-mail. -BenRI

On 1/18/22 8:55 PM, Benjamin Redelings wrote:

Hi,

1. I think I have clarified my problem a bit. It is actually not related to pattern bindings. Here's an example:

h = let f c i = if i > 10 then c else g c 'b' g 'a' w = f 'b' 10 g z w = z in (f 'a' (1::Int), f 'a' (1.0::Double))

If I am understanding the Haskell type system correctly,

* the definitions of f and g form a recursive group

* the monomorphism restriction is not invoked

* the inner binding (to f and g) leads to a local value environment (LVE):

{ f :: Char -> a -> Char; g :: Char -> Char -> Char }

with predicates (Num a, Ord a)

2. In this situation, Typing Haskell in Haskell suggests that we should NOT apply the predicates to the environment because the type for g does not contain 'a', and would become ambiguous (section 11.6.2). Instead, we should only apply predicates to the environment if their type variables are present in ALL types in the current declaration group.

Since the predicates (Num a, and Ord a) are not retained, then we cannot quantify over a.

It seems like this should make `f` monomorphic in a, and thus we should not be able apply (f 'a') to both (1::Int) and (1::Double).

Does that make any sense?

3. GHC, however, compiles this just fine. However, if I add "default ()", then it no longer compiles.

4. On further reflection, Typing Haskell in Haskell applies defaulting rules when evaluating each binding, and not just at the top level. So this might be part of where my code is going wrong.

-BenRI

On 1/15/22 11:09 AM, Benjamin Redelings wrote:

Hi,

1. I'm reading "A Static semantics for Haskell" and trying to code it up. I came across some odd behavior with pattern bindings, and I was wondering if someone could explain or point me in the right direction.

Suppose you have the declaration

(x,y) = ('a',2)

My current code is yielding:

x :: Num a => Char

y :: Num a => a

However, I notice that ghci gives x the type Char, with no constraint, which is what I would expect. It also gives y the type 'Num b => b', so I don't think it is defaulting a to Int here.

The weird results from my code stem from rule BIND-PRED in Figure 15 of https://homepages.inf.ed.ac.uk/wadler/papers/staticsemantics/static-semantic...

E |- bind ~~> \dicts : theta -> monobinds in bind : (LIE_{encl}, theta => LVE)

Here theta = ( Num a ) and LVE = { x :: Char, y :: a }. So, theta => LVE is

{ x :: Num a => Char, y :: Num a => a }

The obvious thing to do is avoid changing a type T to Num a => T if T does not contain a. Also I'm not totally sure if that trick gets to the bottom of the issue. However, the paper doesn't mention define theta => LVE that way. Is there something else I should read on this?

2. If we just chop out predicates which mention variables not in the type ( == ambiguous predicates?) then I'm not totally sure how to create code for this.

I would imagine that we have something like

tup dn = ('a', fromInteger dn 2)

x = case (tup dn) of (x,y) -> x

y dn case (tup dn) of (x,y) -> y

In this case its not clear where to get the `dn` argument of `tup` from, in the definition of `x`. Can we pass in `undefined`? Should we do something else?

If anyone can shed light on this, I would be grateful :-)

-BenRI

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Thanks for the references!  I will take a look. -BenRI On 8/4/22 9:22 PM, David Christiansen wrote:

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.

(I'm first answering now because I wasn't sure until this comment that it was the same concept of levels that I know of)

A couple of resources do exist for learning this idea. There's a quite accessible description of the basic idea in Peter Sestoft's book "Programming Language Concepts" from about ten years ago. A collection of fancier and more efficient versions are laid out by Oleg Kiselyov here: https://okmij.org/ftp/ML/generalization.html . A good source back to Remy is this one: https://hal.inria.fr/inria-00077006/document

/David

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?

Yes, but the check is a bit conservative. Look at `inert_given_eqs` in `InertCans`, and `updateGivenEqs`. * implication constraints like (a ~ Int ==> a ~ Int) are never created.

I may be assuming that GHC runs the solver for each GADT pattern match

before creating implication constraints.

That's not right. They can be created, but then get solved, by solving the Wanted from the Given. 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...

Well there is a `Outputable` instance. It uses `=>`. Simon On Mon, 15 Aug 2022 at 20:00, Benjamin Redelings < benjamin.redelings@gmail.com> wrote:

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-inferenc..., 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