[Haskell-cafe] Type system madness
jcast at ou.edu
Wed Jul 11 16:13:55 EDT 2007
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).
More information about the Haskell-Cafe