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

[Jason Dagit]

On Tue, Oct 7, 2008 at 8:02 AM, apfelmus <apfelmus at quantentunnel.de> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20081007/67ea02ba/attachment.htm