[Haskell-cafe] Existential quantification of environments.
k.schupke at imperial.ac.uk
Tue Nov 22 11:40:24 EST 2005
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 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe