[Haskell-cafe] Type system madness

[Jonathan Cast]

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