[Haskell-cafe] Existential types (Was: Type vs TypeClass duality)
wss at cs.nott.ac.uk
Thu Oct 25 15:20:01 EDT 2007
> In a sense, that's also the reason why stream fusion à la Duncan +
> Roman + Don uses an existential type
> data Stream a where
> Stream :: ∀s. s -> (s -> Step a s) -> Stream a
> data Step a s = Done
> | Yield a s
> | Skip s
I thought there was a deeper reason for this, but I might be wrong.
You can represent all inductive types by their Church encoding. This
basically identifies every inductive type with its fold.
You can do the same for terminal coalgebras and coinductive types,
but things are a bit different. Suppose we define:
data CoFix f = In (f (CoFix f))
Then the unfold producing a value of type CoFix f has type:
forall a . (a -> f a) -> a -> CoFix f
Now if my logic doesn't fail me, we can also write this as
(exists a . (a -> f a, a)) -> CoFix f
Using the "co-Church encoding" of colists yields the above Stream
data type, where "f" corresponds to the "Step" data type. (The Skip
constructor is a bit of a fix to cope with filter and friends).
More information about the Haskell-Cafe