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

[apfelmus]

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