Jonathan Cast wrote:
toUpper :: exists x. x -> x works for only one choice of x.
Are you sure that's not:
"toUpper :: exists x. x -> x works for *at least one* choice of x"
?
I'm not sure about the "haskell" meaning, but the "logic" meaning is
definitely this. For example:
forall x:Integer. 4*x is even <=> all multiples of four are even -- duh!
exists x:Integer. 4*x is even <=> it's possible to find a multiple of
four that is even -- MEGA DUH!: we know that ALL multiples of four are
even, so obviously it's possible to find AT LEAST ONE that's even: *any*
one, in fact!
It obviously doesn't change any consequences that Stefan draws: namely
that that the user of a value of that type is not entitled to assume
anything (i.e. any interface) about the value -- he only knows that such
a type exists.
Regards,
Martin
Please check out my music: http://www.youtube.com/user/thetonegrove
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
