On Sat, Nov 14, 2009 at 17:55, Mark Lentczner wrote:

Would I be correct in thinking: The difference between these two is that the type b can be "fixed" upon application of amy to the first two arguments (given context), whereas bob applied to two arguments MUST return a function that is applicable to every type.

amy :: Int -> a -> b -> [Either a b]
bob :: Int -> a -> (forall b. b) -> [Either a b]

Here are the same functions using fresh variables where necessary plus an additional function:

amy :: forall a b. Int -> a -> b -> [Either a b]
bob :: forall a b. Int -> a -> (forall c. c) -> [Either a b]
cat :: forall a . Int -> a -> (forall b. b -> [Either a b])

First, note that the types of amy and cat are equivalent. Since function arrows are right-associative and since there are no conflicting variables b outside the scope of forall b, the quantification can easily be pushed to the outside as in amy. (I don't know if cat is what you meant to have for bob, so I thought I'd add it just in case.)

As for bob, the only third argument it can take is bottom (undefined or error). And that argument has no effect on the types instantiated for a or b. (Using a fresh variable c helps make that more evident at a glance.)

Sean