[Haskell-cafe] Type system madness

[Martin Percossi]

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