
22 Nov
2005
22 Nov
'05
8:16 a.m.
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