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
Alfonso Acosta wrote:
This bit was specially helpful:
"So, how to compute a value b from an existential type ∃a.(a -> a)? ..."
Could you give a specific example of computing existential types?
Well, the word "compute" was probably not a good choice, I meant the
following question: "given a
Peter Hercek wrote:
I do not see why forall can be lifted to the top of function arrows.
I probably do not understand the notation at all. They all seem to be
different to me.
String -> ∀a.a
a function which takes strings a returns a value of all types together
for any input string (so only
Dan Weston wrote:
Thanks for the concise explanation. I do have one minor question though.
> -+- A more useful example is
>
> ∃a. Show a => a i.e. ∃a.(a -> String, a)
>
> So, given a value (f,x) :: ∃a.(a -> String, a), we can do
>
> f x :: String
>
> but that's pretty much al
On 10/24/07, Peter Hercek <[EMAIL PROTECTED]> wrote:
>
> I do not see why forall can be lifted to the top of function arrows.
> I probably do not understand the notation at all. They all seem to be
> different to me.
Consider this simple function:
\b x y -> if b then x else y
Let's say
apfelmus wrote:
-+- Since ∀ and ∃ are clearly different, why does Haskell have only one
of them and even uses ∀ to declare existential types? The answer is the
following relation:
∃a.(a -> a) = ∀b. (∀a.(a -> a) -> b) -> b
So, how to compute a value b from an existential type ∃a.(a -> a)?
