
2 Feb
2006
2 Feb
'06
4:11 p.m.
On Thu, 2 Feb 2006, Taral wrote:
On 2/2/06, Philippa Cowderoy
wrote: Not in the context of a predicative type system. Also, if we treat it simply as an annotation (exists a . a), we end up throwing away the additional information inferred.
There's that word again. Can someone explain what "predicative" means, in detail?
For historical reasons that's hard work. The short version is "type variables can only be instantiated to monotypes", whereas in an impredicative system type variables can be instantiated to types including quantifiers. -- flippa@flippac.org 'In Ankh-Morpork even the shit have a street to itself... Truly this is a land of opportunity.' - Detritus, Men at Arms