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 |
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 |
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 |
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 |
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 |
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 |
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 |
Free forum by Nabble | Edit this page |