Types for the Scott Numerals
Martı́n Abadi, Luca Cardelli, Gordon D. Plotkin · 1993
where case(n)(a)(f) returns a if n is 0 and f(x) if n is the successor of x (see, e.g., [2]). The Scott numerals are distinguished from the Church numerals by their \linearity: the bound variables of 0, succ, and case occur at most once in the bodies of these functions, and the predecessor function n:n(0)( x:x) can be computed trivially. The Scott numerals can be typed in an extension of System F with covariant recursive types. We can take the type of the Scott numerals to be the solution to the equation S = 8R: (R! (S ! R)! R):