On Mon, Oct 6, 2008 at 1:56 PM, Ryan Ingram <ryani.spam@gmail.com> wrote:
2008/10/6 Jason Dagit <dagit@codersbase.com>:
> \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