[Haskell-cafe] [Haskell] Higher types in contexts

[Ryan Ingram]

I find it easy to understand this distinction by writing out the types of
the constructors and case expressions for these objects, in a language like
system F:

(here, {x :: t} means a type argument with name x of kind t)

Exists :: {f :: *->*} -> {a :: *} -> f a -> Exists f
Forall :: {f :: *->*} -> ({a :: *} -> f a) -> Forall f

Notice the higher rank type in the constructor 'Forall'.

Similarly, the case deconstruction for these:

caseExists :: {r :: *} -> {f :: *->*} -> ({a :: *} -> f a -> r) -> Exists f
-> r
caseForall :: {r :: *} -> {f :: *->*} -> (({a :: *} -> f a) -> r) -> Forall
f -> r

The function passed to caseExists needs to be able to handle any type 'a'
we throw at it, whereas the function passed to caseForall can choose what
'a' it wants to use (and can choose multiple different 'a's by calling the
({a::*} -> f a) parameter function multiple times.  In the simple case that
the case function only instantiates 'a' at a single type, we can simplify
this:

caseForall' :: {r :: *} -> {f :: * -> *} -> {a :: *} -> (f a -> r) ->
Forall f -> r

and this function is definable in terms of caseForall:

caseForall' {r} {f} {a} k v = caseForall {r} {f} (\mk_fa -> k (mk_fa {a})) v

  -- ryan

On Mon, Mar 5, 2012 at 9:37 PM, wren ng thornton <wren at freegeek.org> wrote:

> On 3/5/12 5:13 PM, AntC wrote:
>
>> I've tried that ListFunc wrapping you suggest:
>> [...]
>>
>> But I can't 'dig out' the H-R function and apply it (not even
>> monomorphically):
>>
>
> That's because the suggestion changed it from a universal quantifier to an
> existential quantifier.
>
>    data Exists f = forall a. Exists (f a)
>
>    data Forall f = Forall (forall a. f a)
>
> With Exists, we're essentially storing a pair of the actual type 'a' and
> then the f a itself. We can't just pull out the f a and use it, because we
> don't know what 'a' is. We can bring it into scope temporarily by case
> matching on the Exists f, which allows us to use polymorphic functions, but
> we still don't actually know what it is so we can *only* use polymorphic
> functions.
>
> Conversely, with Forall we're storing some f a value which is in fact
> polymorphic in 'a'. Here, because it's polymorphic, the caller is free to
> choose what value of 'a' they would like the f a to use. Indeed, they can
> choose multiple different values of 'a' and get an f a for each of them.
>
> --
> Live well,
> ~wren
>
>
> ______________________________**_________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120306/919e0c72/attachment.htm>