On Tue, Oct 7, 2008 at 8:02 AM, apfelmus <[EMAIL PROTECTED]> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
