On Mon, Oct 6, 2008 at 1:56 PM, Ryan Ingram wrote:

2008/10/6 Jason Dagit :

...

\begin{code} badOrder :: (Sealed (p x)) -> (forall b. (Sealed (q b))) -> (Sealed (q x)) badOrder sx sy = case sy of Sealed y -> case sx of Sealed x -> Sealed (f x y) \end{code}

\begin{code} goodOrder :: (Sealed (p x)) -> (forall b. (Sealed (q b))) -> (Sealed (q x)) goodOrder sx sy = case sx of Sealed x -> case sy of Sealed y -> Sealed (f x y) \end{code}

It may help if you transform this a bit closer to System F with existentials & datatypes: /\ = forall

Why is useful to replace forall with /\?

@t = type application, with the rule:

(a :: forall x. b) @t :: (replace occurrences of x in b with t)

How do you know how to apply this rule in general? For example, (a :: forall x y. x -> y) @t, would mean what?

-- the quantified type "x" gets packed into the data -- and comes out when you pattern match on it data Sealed s where Sealed :: /\t. s t -> Sealed s

By 'x' you mean 't' right? goodOrder = \sx :: Sealed (p x) -> \sy :: (/\b. Sealed (q b)) ->

case sx of (Sealed @y pxy) -> case (sy @y) of (Sealed @z qyz) -> Sealed @z (f pxy qyz)

You have the expression (Sealed @y pxy), but I don't understand what that signifies. Are you just saying that by doing a pattern match on 'sx' that you're going to bind the existentially quantified variable to 'y'? This notation confuses me, but I can happily accept that we are binding the existential type 'y' somewhere. Assuming, I understand that, correctly, the expression (Sealed @z qyz) is binding 'z' to an existential. Why do you say, (sy @y). What does that mean? That makes 'b' unify with 'y' that was bound in the first case? goodOrder works as I expect, so I'm happy with this. badOrder = \sx :: Sealed (p x) -> \sy :: (/\b. Sealed (q b)) ->

-- in order to pattern-match on sy, we need to give it a type -- so we just pick an arbitrary type "unknown" or "u" distinct from any other type we know about case (sy @u) of (Sealed @z quz) -> case sx of (Sealed @y pxy) -> Sealed @z (f pxy quz) -- doesn't typecheck!

In the good order, you have already unpacked the existential for sx, so you know what type to instantiate sy at. In the bad order, you don't know what type to instantiate sy at.

We instantiate 'u' to be the existential in sy. OK. But, my understanding is that 'u' is unconstrained at this point, we said, forall b. Sealed (q b), afterall. So, when we bind 'y' in the second case, what prevents 'u' from unifying with 'y'? For what it's worth, in my real program where this came up, sy was created by a recursive call like this: foo :: Sealed (p x) -> Sealed (q b) foo = do p <- blah q <- foo return (Sealed (f p q)) Because the b doesn't appear on the LHS of the function arrow, I understand it to have the same polymorphic properties as the 'forall b.' in the type signature of goodOrder and badOrder. Indeed, this example seems to re-enforce that. We had to reorder the binding of p and q to get this to type check. Thanks for the quick response, Jason

On Mon, Oct 6, 2008 at 10:27 PM, Jason Dagit wrote:

Why is useful to replace forall with /\?

To make it look more like a capital lambda, just like \ is notation for lambda. It's a lambda abstraction over a type instead of a value; that's how polymorphism works in GHC's core language.

...

@t = type application, with the rule:

(a :: forall x. b) @t :: (replace occurrences of x in b with t)

How do you know how to apply this rule in general?

For example, (a :: forall x y. x -> y) @t, would mean what?

As written, (a :: forall x y. x -> y) @t :: (forall y. t -> y) But it doesn't matter, as you can write: /\y. /\x. (a :: forall x y. x -> y) @y @x :: forall y x. x -> y which allows you to arbitrarily reorder the foralls; the compiler does this when it wants to instantiate a variable in the middle of a group of foralls. This is similar to flip f x y = f y x which allows you to reorder the arguments of a function.

...

-- the quantified type "x" gets packed into the data -- and comes out when you pattern match on it data Sealed s where Sealed :: /\t. s t -> Sealed s

By 'x' you mean 't' right?

Yes, oops. Although it doesn't matter because you can rename bound variables, which is what I did when writing the message; I just forgot to update the documentation! :)

...

goodOrder = \sx :: Sealed (p x) -> \sy :: (/\b. Sealed (q b)) -> case sx of (Sealed @y pxy) -> case (sy @y) of (Sealed @z qyz) -> Sealed @z (f pxy qyz)

You have the expression (Sealed @y pxy), but I don't understand what that signifies. Are you just saying that by doing a pattern match on 'sx' that you're going to bind the existentially quantified variable to 'y'? This notation confuses me, but I can happily accept that we are binding the existential type 'y' somewhere.

It's just like any other data constructor/destructor; it's just that the constructor for Sealed takes an additional argument: the type that the existential is bound at. So when you pattern match on it, you get that type back out.

Assuming, I understand that, correctly, the expression (Sealed @z qyz) is binding 'z' to an existential. Why do you say, (sy @y). What does that mean? That makes 'b' unify with 'y' that was bound in the first case?

Yes, that's correct.

goodOrder works as I expect, so I'm happy with this.

...

badOrder = \sx :: Sealed (p x) -> \sy :: (/\b. Sealed (q b)) -> -- in order to pattern-match on sy, we need to give it a type -- so we just pick an arbitrary type "unknown" or "u" distinct from any other type we know about case (sy @u) of (Sealed @z quz) -> case sx of (Sealed @y pxy) -> Sealed @z (f pxy quz) -- doesn't typecheck!

In the good order, you have already unpacked the existential for sx, so you know what type to instantiate sy at. In the bad order, you don't know what type to instantiate sy at.

We instantiate 'u' to be the existential in sy. OK. But, my understanding is that 'u' is unconstrained at this point, we said, forall b. Sealed (q b), afterall. So, when we bind 'y' in the second case, what prevents 'u' from unifying with 'y'?

Sort of, but not exactly. Here's an example at the value level: f x = (5 * x, \y -> y + x) g x = case f x of (v, g) -> \y -> (v, g y) h y = case f ?? of (v, g) -> \x -> plug in x to the f above, then (v, g y) Your "badorder" is similar to h; you have to instantiate the type variable before you can evaluate the case statement. You may think it doesn't matter, because you could instantiate it to anything after the fact, but it's possible that the result of the case statement depends on the choice of instantiation for sy; consider if sy had an additional constraint:

Sealed (fromInteger) :: forall t. Num t => Sealed ((->) Integer)

Now the result of the case statement is the concrete implementation of fromInteger for whatever type it gets instantiated at.

For what it's worth, in my real program where this came up, sy was created by a recursive call like this: foo :: Sealed (p x) -> Sealed (q b) foo = do p <- blah q <- foo return (Sealed (f p q))

Because the b doesn't appear on the LHS of the function arrow, I understand it to have the same polymorphic properties as the 'forall b.' in the type signature of goodOrder and badOrder. Indeed, this example seems to re-enforce that. We had to reorder the binding of p and q to get this to type check.

Yes, that's correct; consider the simpler example of "const" const :: forall a b. a -> b -> a foo = const "hello" which becomes foo :: forall b. b -> String foo = /\b. const @String @b "hello" = /\b. \x :: b. "hello" -- ryan

Jason Dagit wrote:

Ryan Ingram wrote:

...

Jason Dagit wrote:

...

\begin{code} badOrder :: (Sealed (p x)) -> (forall b. (Sealed (q b))) -> (Sealed (q x)) badOrder sx sy = case sy of Sealed y -> case sx of Sealed x -> Sealed (f x y) \end{code}

\begin{code} goodOrder :: (Sealed (p x)) -> (forall b. (Sealed (q b))) -> (Sealed (q x)) goodOrder sx sy = case sx of Sealed x -> case sy of Sealed y -> Sealed (f x y) \end{code} It may help if you transform this a bit closer to System F with existentials & datatypes: /\ = forall

Why is useful to replace forall with /\?

Actually, the forall's should be left alone, the big lambda /\ lives on the value level, not the type level :) But this small typo aside, making all type applications explicit is the right thing to do to see what's going on. In the original System F - the basis for Haskell's type system - http://en.wikipedia.org/wiki/System_F all type applications are explicit. For instance id 'c' in Haskell would be written id Char 'c' in System F the type is an explicit argument to a polymorphic function. The definition of id would be id : ∀a. a -> a id = Λa.λx:a.x So, first supply the type and then compute something. In Haskell, the compiler figures out which type argument to apply where and this can get confusing like in Jason's example. (By the way, I found the "Proofs and Types" book references in the wikipedia page to be a very readable introduction to System F and the Curry-Howards isomorphism in general.) In System F, the example reads as follows (for clarity, we prefix type variables with an @ when they are applied) foo : ∀p,q,x,y,z.p x y -> q y z -> q x z foo = ... goodOrder : ∀p,q,x. Sealed (p x) -> (∀b.Sealed (q b)) -> Sealed (q x) goodOrder = Λp.Λq.Λx. λsx:Sealed (p x).λsy:(∀b.Sealed (q b)). case sx of Sealed @y (pxy:p x y) -> case sy @y of Sealed @z (qyz:q y z) -> Sealed @z (foo @p @q @x @y @z pxy qyz) badOrder : ... badOrder = Λp.Λq.Λx. λsx:Sealed (p x).λsy:(∀b.Sealed (q b)). case sy ??? of Sealed @z (qyz:q ??? z) -> case sx of Sealed @y (pxy:p x y) -> Sealed @z (foo @p @q @x @y @z pxy qyz) In the second case, there's no way to know what type to choose for b unless you evaluate sx first. However, the following would work: badOrder : ∀p,q,x. Sealed (p x) -> (Sealed (∀b. q b)) -> Sealed (q x) badOrder = Λp.Λq.Λx. λsx:Sealed (p x).λsy:(Sealed (∀b.q b)). case sy of Sealed @z (qyz:∀b.q b z) -> case sx of Sealed @y (pxy:p x y) -> Sealed @z (foo @p @q @x @y @z pxy (qyz @y)) In other words, (Sealed (∀b.q b)) and (∀b.Sealed (q b)) are quite different types. But this is not surprising. After all, this "Sealed" thing is the existential quantifier Sealed f = ∃x.f x and both types read Sealed (∀b.q b) = ∃x.∀b.q b x ∀b.Sealed (q b) = ∀b.∃x.q b x The latter is broader because it might yield different x for different b while the first one has to produce one x that works for all b at once. Here's an example for natural numbers that illustrates the difference: ∀m.∃n.n > m -- we can always find a larger number (sure, use n=m+1) ∃n.∀m.n > m -- we can find a number larger than all the others! Regards, apfelmus PS: The wikibook has a chapter http://en.wikibooks.org/wiki/Haskell/Polymorphism that is intended to explain and detail such issues and the translation from Haskell to System F, but it's currently rather empty.