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