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

[apfelmus]

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.