[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
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.
More information about the Haskell-Cafe
mailing list