[Haskell-cafe] Are arbitrary rank types and existentials equivalent?

Henning Thielemann schlepptop at henning-thielemann.de
Mon Nov 10 17:09:46 EST 2008


Ryan Ingram schrieb:

> There's a natural relation between higher rank types and existentials;
> one way to think about it is this: if you have some existential type t
> (subject to some constraints), you cannot operate on it except with
> some function that accepts any type t subject to those constraints.
> 
> There is a simple encoding of existential types using higher rank types:
> 
> Given
>> data E a1..an = forall e1...en. (constraints) => E t1..tn
> where t1..tn are types in terms of a1..an, we replace with
>> data E' a1..an = E' (forall b. (forall e1..en. t1 -> t2 -> ... -> tn -> b) -> b)

Can you please put this on the Wiki?


More information about the Haskell-Cafe mailing list