Re: [Haskell-cafe] Existential quantification of environments.
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existential quantification of environments.
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existential quantification of environments.
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Existential quantification of environments.
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
Re: [Haskell-cafe] Existential quantification of environments.
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
