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

7 Oct 2008


      On Tue, Oct 7, 2008 at 8:02 AM, apfelmus  wrote:
...
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
Thanks, I'll be reading up on that.
...
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.
Ah, okay, so this rule of first supplying the type is what keeps my example
from being confusing about the order of @y.  That makes a lot of sense.
...
(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.)
Okay, thanks.
...
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)
Thanks, that's quite illustrative.

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
Oh right, but yes this changes things considerably.  I think your point with
this example is that this more closely matches my expectation, but I know
from experience and your explanation that this is not what I want.
Therefore, I should accept the behavior I'm seeing from the type checker :)

Thank you,
Jason