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
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 all we can
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
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 type
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)?
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 we
