# [Haskell-cafe] Re: Inferred type is less polymorphic than expected, depends on order

apfelmus apfelmus at quantentunnel.de
Tue Oct 7 11:02:00 EDT 2008

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

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
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  = Λ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:

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

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