On Mon, Oct 6, 2008 at 10:27 PM, Jason Dagit
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