Normal Forms have Partial Types

We prove that every -term in normal form has one of Thatte's partial types. Keywords: Functional programming, partial types. Partial types for the pure -calculus [1] were introduced by Thatte in 1988 [5] as a way to type certain -terms that are untypable in the simply-typed - calculus. Any -term that has a simple type also has a partial type. Moreover, any -term that has a partial type is strongly normalizing [6]. Type inference for partial types can be performed in cubic time, as demonstrated by Kozen and Schwartzbach together with the present author [3]. Our algorithm improved the exponential time algorithm of O'Keefe and Wand [4]. In this paper we prove that every -term in normal form has a partial type. This property is shared by few other type systems, one example being the simple intersection types of Coppo and Giannini [2]. The set of partial types is defined by the grammar t ::=\Omega j t ! t Partial types are ordered by as follows: 1. t \Omega for any t; 2. s ! t s..