Re: [Haskell-cafe] Existential types (Was: Type vs TypeClass duality)

Ryan Ingram wrote:
On 10/24/07, apfelmus
wrote: So, instead of storing a list [∃a. Show a => a], you may as well store a list of strings [String].
I've seen this before, and to some extent I agree with it, but it breaks down for bigger examples due to sharing.
In most cases, "x" has a more compact representation than the result of evaluating "show x". So if you keep a list of [show x, show y, show z] around for a long period of time, you're leaking space. Consider instead:
data StringFn where StringFn :: forall a. a -> (a -> String) -> StringFn
applyStringFn :: StringFn -> String applyStringFn (StringFn a f) = f a
[ StringFn x show, StringFn y show, StringFn z show ]
Now, you use more time every time you compute the result, but StringFn has a compact representation; you're not leaking the space used for the string throughout the execution of the program, but only allocating it while it's used.
Indeed. (Although the effect will be marginal in this particular example since the unevaluated thunk (show x) is represented as compactly as x . But the time-space trade-off would matter when strings from the list are used several times.) 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 mean, every stream can be represented by the list of its results but the observation for fusion is that there is a much more compact representation for the state (like an integer for [1..] or the source list in map f . map g $ [x,y,...]) Regards, apfelmus

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). Best, Wouter

Wouter Swierstra wrote:
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. [..]
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
(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).
Yes. I mean, I want to say that the efficiency gain of fusion is based on the fact that the state (the "seed" a ) can be represented more compactly than the resulting CoFix f . I.e. while ∃a. (a -> f a, a) =~= CoFix f the former type may be a more compact representation than the latter, demonstrating that an existential type may have performance benefits compared to an isomorphic alternative. (This is even without sharing here, Ryan remark was about sharing issues) Regards, apfelmus
participants (3)
-
apfelmus
-
apfelmus@quantentunnel.de
-
Wouter Swierstra