On Wednesday 11 July 2007, Martin Percossi wrote: > 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"
Not quite. When you give a constructive proof of exists x. x -> x, you only prove it at one value of x, and a value of type exists x. x -> x is just such a proof. When you go and use that proof, you can thus only use it at one type. Thus, properly speaking, a value of type exists x. x -> x should be thought of as a pair of a type x and a (monomorphic) function of type x -> x. So when you eliminate the existential quantifier, you get a function of type x -> x for precisely one (unknown) type. That type is the same every time, in fact, although the compiler won't let you use this fact (doing so would turn the existential quantifier into a dependent sum). <snip> Jonathan Cast http://sourceforge.net/projects/fid-core http://sourceforge.net/projects/fid-emacs _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
