[Haskell-cafe] Existential quantification of environments.

[Keean Schupke]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe