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

[Ryan Ingram]

On Mon, Oct 6, 2008 at 10:27 PM, Jason Dagit <dagit at codersbase.com> wrote:
> Why is useful to replace forall with /\?

To make it look more like a capital lambda, just like \ is notation
for lambda.  It's a lambda abstraction over a type instead of a value;
that's how polymorphism works in GHC's core language.

>> @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?

As written,

(a :: forall x y. x -> y) @t :: (forall y. t -> y)

But it doesn't matter, as you can write:
   /\y. /\x. (a :: forall x y. x -> y) @y @x  :: forall y x. x -> y

which allows you to arbitrarily reorder the foralls; the compiler does
this when it wants to instantiate a variable in the middle of a group
of foralls.

This is similar to
   flip f x y = f y x
which allows you to reorder the arguments of a function.

>> -- 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?

Yes, oops.  Although it doesn't matter because you can rename bound
variables, which is what I did when writing the message; I just forgot
to update the documentation! :)

>> 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.

It's just like any other data constructor/destructor; it's just that
the constructor for Sealed takes an additional argument: the type that
the existential is bound at.  So when you pattern match on it, you get
that type back out.

> 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?

Yes, that's correct.

> 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'?

Sort of, but not exactly.  Here's an example at the value level:

f x = (5 * x, \y -> y + x)

g x = case f x of (v, g) ->
             \y -> (v, g y)

h y = case f ?? of (v, g) ->
             \x -> plug in x to the f above, then (v, g y)

Your "badorder" is similar to h; you have to instantiate the type
variable before you can evaluate the case statement.

You may think it doesn't matter, because you could instantiate it to
anything after the fact, but it's possible that the result of the case
statement depends on the choice of instantiation for sy; consider if
sy had an additional constraint:

> Sealed (fromInteger) :: forall t. Num t => Sealed ((->) Integer)

Now the result of the case statement is the concrete implementation of
fromInteger for whatever type it gets instantiated at.

> 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.

Yes, that's correct; consider the simpler example of "const"

const :: forall a b. a -> b -> a

foo = const "hello"

which becomes

foo :: forall b. b -> String
foo = /\b. const @String @b "hello"
      = /\b. \x :: b. "hello"

 -- ryan