[Haskell-cafe] Existential quantification of environments.

Keean Schupke k.schupke at imperial.ac.uk
Tue Nov 22 11:19:27 EST 2005

Wolfgang Jeltsch wrote:

>>This seems to suggest:
>>    Add a == exists (add :: a -> a -> a)
>Doesn't "exists" normally quantify over types and not over values?
It is quantifying over types, it is saying there exists a type "a -> a 
-> a" that has
at least one value we will call "add"...

I think the important point is that the existential is a pair of (proof, 
which through curry-howard-isomorphism is (value in set, set). Here we 
are saying that
there is a set of "functions" with the type "a -> a -> a" ... for the 
existential to be satisfied
there must be one called "add". Consider this as an assumption placed on 
the environment
by the function.


More information about the Haskell-Cafe mailing list