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