
17 Feb
2009
17 Feb
'09
7:28 a.m.
Wolfgang Jeltsch wrote:
First, I thought so too but I changed my mind. To my knowledge a type (forall a. T[a]) -> T' is equivalent to the type exists a. (T[a] -> T'). It’s the same as in predicate logic – Curry-Howard in action.
The connection is the other way round, I think. (exists a. T[a]) -> T' = forall a. (T[a] -> T') Regards, apfelmus -- http://apfelmus.nfshost.com