log-book

Types

November 19, 2022, tags: type system.

Types first appeared in Principia Mathematica, Whitehead and Russell [1910-1913].

In Functionality in Combinatory Logic of H. B. Curry:

For a theory concerned with an analysis of these notions I have proposed the name combinatory logic. This is a formal theory based on a primitive frame (i.e., set of primitive ideas, axioms and rules of procedure) of such great simplicity that even comparatively simple inferences, such as are ordinarily made by a substitution process can be decomposed into a large number of the elemental steps represented by the rules of procedure; it furthermore does not postulate any such notions as variable, although all the inferences ordinarily made by the use of variables can-when suitable definitions have been made, of course-be made as compound inferences within the system. The development of this theory, to the point where these statements relative to variables can be proved, is contained in a series of papers culminating in “Apparent Variables from the Standpoint of Combinatory Logic” (Ann. M1lath., 2nd ser., 34, 381-404 (1933)).

We are concerned with statements of the form (using E. H. Moore’s terminology) “f is a function on X to Y”; or (for functions of several variables) “f is a function on X1X2Xm to Y.” The following type of question suggests itself: Suppose we have given certain entities f1, f2, …, fn concerning each of which a statement of the above form has been made; suppose further that g is an entity derived from f1, …, fn by substitution or other such processes; then, what statement of the above form can we infer concerning g? We make inferences of the above form intuitively; what this paper asserts is that when certain formal constituents are added to the primitive frame of combinatory logic, then these inferences can be made abstractly within the extended system.

In Curry and Feys [1958] this type assignment mechanism was adapted to λ-terms.

In Church [1940] lambda-terms were ornamented by fixed types.

Formalism of types in programming

  • M of type A can be an argument only of a function of type A → B.
  • (real → real) → (real → real) for indefinite integrals f(x)dx;
  • (real → real) × real × real → real for definite integrals abf(x)dx;
  • ([0, 1] → real) → (([0, 1] → real) → real) → (([0, 1] → real) → real)

Hindley-Milner algorithm

decides whether an untyped term does have a type and computes the most general type types found their way to functional programming languages.

It was first implemented as part of the type system (simply typed λ-calculus) of the programming language ML. (Milner, Tofte, Harper, and McQueen [1997])

subject reduction theorem

In type theory, a type system has the property of subject reduction (also subject evaluation, type preservation or simply preservation) if evaluation of expressions does not cause their type to change.

if a term M is correctly typed by type A, then also during the computation of M the type remains the same.