[Haskell-cafe] Type system madness
haskell-cafe at martinpercossi.com
Wed Jul 11 13:17:51 EDT 2007
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.
Please check out my music: http://www.youtube.com/user/thetonegrove
More information about the Haskell-Cafe