Existential quantification of environments.

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

Existential quantification of environments.

Keean Schupke
If I have a function:

   f x y = add x y

and I want to type the function in isolation, then the type of 'add' is
essentially carried in the environment... Lets say I want to make this
type explicit in the type signature (where f is valid for any a where
there is an add function on a - ignoring the class that Haskell would
require for the overloading):

   add :: Int -> Int -> Int
   add :: Float -> Float -> Float

   f :: forall a . exists (add :: a -> a -> a) => a -> a -> a

or a step further:

   class Add a where
      add :: a -> a -> a
   instance Add Int where ...
   instance Add Float where ...

   f :: forall a . Add a => a -> a -> a

This seems to suggest:

    Add a == exists (add :: a -> a -> a)

Does this seem in any way right? It seems that the definition of 'f'
does require the existance of 'add'. That is the definition is valid iff
there exists a function called 'add' of the correct type. Also doesn't
the existential quantifier stop you looking inside 'add' - obviously you
cannot inspect the definition as it may not be defined (yet?), but
presumably you can still apply 'add'.

    Regards,
    Keean.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Existential quantification of environments.

Adrian Hey
On Tuesday 22 Nov 2005 10:39 am, Keean Schupke wrote:
> If I have a function:
>
>    f x y = add x y
>
> and I want to type the function in isolation, then the type of 'add' is
> essentially carried in the environment...

I am no expert in type theory so I'm probably about to get way
out of my depth, but isn't this what "principal typings" are all
about (as distinct from "principal types"). Maybe a look at type
system CT would be useful too.

 http://www2.dcc.ufmg.br/~camarao/CT/

Regards
--
Adrian Hey
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Existential quantification of environments.

Keean Schupke
Excellent link thanks! Not quite what I was thinking of - but definitely
related.
I'll give it a read and see if they want to existentially quantify
environments...

    Keean.

Adrian Hey wrote:

>On Tuesday 22 Nov 2005 10:39 am, Keean Schupke wrote:
>  
>
>>If I have a function:
>>
>>   f x y = add x y
>>
>>and I want to type the function in isolation, then the type of 'add' is
>>essentially carried in the environment...
>>    
>>
>
>I am no expert in type theory so I'm probably about to get way
>out of my depth, but isn't this what "principal typings" are all
>about (as distinct from "principal types"). Maybe a look at type
>system CT would be useful too.
>
> http://www2.dcc.ufmg.br/~camarao/CT/
>
>Regards
>--
>Adrian Hey
>  
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Existential quantification of environments.

Wolfgang Jeltsch
In reply to this post by Keean Schupke
Am Dienstag, 22. November 2005 11:39 schrieb Keean Schupke:
> [...]

> This seems to suggest:
>
>     Add a == exists (add :: a -> a -> a)

Doesn't "exists" normally quantify over types and not over values?

> [...]

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Existential quantification of environments.

Keean Schupke
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Existential quantification of environments.

Wolfgang Jeltsch
In reply to this post by Keean Schupke
Am Dienstag, 22. November 2005 17:19 schrieben Sie:
> 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"...

It says that there exists a value add.  With quantifying over types I meant
something like this:

        exists a. <some type using the type variable a>

This is how forall in GHC and Hugs looks like.

> [...]

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe