Just to clarify... In the example given the existential would be satisfied if a==Int, and there was a definition of: add :: Int -> Int -> Int IE add is a member of the set/type "a -> a -> a"... Keean Keean Schupke wrote:
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, proposition) 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.
Keean.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe