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

[Jason Dagit]

On Mon, Oct 6, 2008 at 1:56 PM, Ryan Ingram <ryani.spam at gmail.com> wrote:

> 2008/10/6 Jason Dagit <dagit at codersbase.com>:
> > \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 /\?


>
> @t = type application, with the rule:
>
> (a :: forall x. b) @t :: (replace occurrences of x in b with t)


How do you know how to apply this rule in general?

For example, (a :: forall x y. x -> y) @t, would mean what?


> -- the quantified type "x" gets packed into the data
> -- and comes out when you pattern match on it
> data Sealed s where
>    Sealed :: /\t. s t -> Sealed s


By 'x' you mean 't' right?

goodOrder = \sx :: Sealed (p x) -> \sy :: (/\b. Sealed (q b)) ->
>    case sx of (Sealed @y pxy) ->
>        case (sy @y) of (Sealed @z qyz) ->
>            Sealed @z (f pxy qyz)


You have the expression (Sealed @y pxy), but I don't understand what that
signifies.  Are you just saying that by doing a pattern match on 'sx' that
you're going to bind the existentially quantified variable to 'y'?  This
notation confuses me, but I can happily accept that we are binding the
existential type 'y' somewhere.

Assuming, I understand that, correctly, the expression (Sealed @z qyz) is
binding 'z' to an existential.  Why do you say, (sy @y).  What does that
mean?  That makes 'b' unify with 'y' that was bound in the first case?
goodOrder works as I expect, so I'm happy with this.

badOrder = \sx :: Sealed (p x) -> \sy :: (/\b. Sealed (q b)) ->
>    -- in order to pattern-match on sy, we need to give it a type
>    -- so we just pick an arbitrary type "unknown" or "u" distinct
> from any other type we know about
>    case (sy @u) of (Sealed @z quz) ->
>        case sx of (Sealed @y pxy) ->
>            Sealed @z (f pxy quz) -- doesn't typecheck!
>
> In the good order, you have already unpacked the existential for sx,
> so you know what type to instantiate sy at.  In the bad order, you
> don't know what type to instantiate sy at.


We instantiate 'u' to be the existential in sy.  OK.  But, my understanding
is that 'u' is unconstrained at this point, we said, forall b. Sealed (q b),
afterall.  So, when we bind 'y' in the second case, what prevents 'u' from
unifying with 'y'?

For what it's worth, in my real program where this came up, sy was created
by a recursive call like this:
foo :: Sealed (p x) -> Sealed (q b)
foo = do
  p <- blah
  q <- foo
  return (Sealed (f p q))

Because the b doesn't appear on the LHS of the function arrow, I understand
it to have the same polymorphic properties as the 'forall b.' in the type
signature of goodOrder and badOrder.  Indeed, this example seems to
re-enforce that.  We had to reorder the binding of p and q to get this to
type check.

Thanks for the quick response,
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20081006/8d356329/attachment.htm