Existential quantification of environments.
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.
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
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
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.
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
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
participants (3)
-
Adrian Hey -
Keean Schupke -
Wolfgang Jeltsch