question about typing power of F_omega

• To: types@uk.ac.glasgow.dcs (types forum submission)
• Subject: question about typing power of F_omega
• From: kucan@edu.mit.lcs.theory
• Date: Fri, 05 Feb 93 11:34:37 -0500
• Approved: types@dcs.gla.ac.uk

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

• Prev: Re: F-bounded polymorphism
• Next: Re: F-bounded polymorphism and the Cardelli-Curien-Ghelli algorithm
• Index(es):
  • Main
  • Thread