[Prev][Next][Index][Thread]
question about typing power of F_omega
Is a theorem of the following kind known to hold for the type system
F_omega?
For any integer n, there is an untyped term M_n such that M_n
is not typable in F_n, but it is typable in F_n+1.
F_n is the fragment of F_omega that allows type constructors of
order up to n.
I know that F_3 can type more than F_2 (or sometimes denoted by F),
but I couldn't find any results about higher order fragments.
I would appreciate any reference to such results.
Thanks,
--Jakov Kucan