Positive Types in System F

Ying Jiang

We work on the class of the types with positive quantifiers of System F.

1. We develop a nature method to decide whether or not a given type of this class is inhabited; and in the positive case, to construct a base for the set of inhabitants of the type s.t. every inhabitant of the type is βη-equivalent to an element of the base. This methods combines and extends method in [1] and [2]

2. We present semantically a completeness result for the types of this class.

3. The above results lead to a semantical notion of extended data type. We prove that every closed inhabited type of the class is an extended data type. Also the set of extended data types is closed under several type constructors.

[1] J.-R. Hindley, Basic Simple Type Theory (Cambridge Tracts in Theoretical Computer Science), 42, Cambridge University Press.

[2] Y. Jiang, Universal types in System F, Preprint, (1998)

Address: Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, P.O. Box 8718, Beijing 100080, China

E-mail: jy@ox.ios.ac.cn