From philosophy to computation: how Russell’s type theory impacts programming languages

It is summed up again in the same reference as follows: “Type theory emerged as a unifying conceptual framework for the design, analysis, and implementation of programming languages” [5, p.7]. More precisely, the authors pointed out that “Type theory helps to clarify subtle concepts such as data abstraction, polymorphism, and inheritance. It provides a foundation for developing logics ofprogram behaviour that are essential for reasoning about programs. It suggests new techniques for implementing compilers that can improve the efficiency and integrity of code”. [5, p. 7]

More generally, type theory is defined as the discipline of studying type systems in programming languages in a formal way. It is seen as a tool in the design and definition of programming languages [6, p. 516]. It intervenes in the definition of abstraction, polymorphism [7, p.2], and other fundamental principles in programming.

2. Influence of Type Theory on Functional Programming Languages

Type theory and functional programming language are intimately related. In fact, type theory constitutes the core of most functional languages such as LISP, ML and others, and consequently the “programming by functions” paradigm became, as wanted by Church, a foundational part of the design of functional languages. They are, in addition, used to analyze other programming languages which often integrate some features of type systems' principles.

In 1932-1933 Church defined the lambda-calculus notation [8, p.60] focusing on functions as primitive objects instead of sets developed earlier by Russell and Whitehead. It became, then, an integral part of type theory.

Consequently, the typed lambda calculus became a semantic model for many functional languages and theorem provers.

More precisely, a term in lambda-calculus is a variable, function, or application. The only valid terms are who respect a type constraint fortified by types' rules. For example, if a function f is defined as f\ t1 ^ t2 , this typing rule means that the only valid input type is t1, and the only output valid type is t2.

Concerning the languages design, Church's lambda-calculus has been at the origin of the development of functional programming languages in general, and Lisp language in particular. It basically led to two main programming approaches: untyped (or implicitly typed) languages, and typed languages, such as Algol, in which the types of variables, functions or other programming objects are explicitly defined in the program.

The principle of type theory allows, on one hand, to define the data types, and on the other hand, to precise the functions intervals or their data range.

Functional programming languages deal with computation simply as evaluation of functions. The extension of Russell's type theory based on sets to a simple type theory based on functions is a basis of the development of functional languages in which a set becomes a type among many others. In this sense, it is computationally more practical to consider objects as types rather than sets. This allows the definition of many data structures such as lists, graphs, trees, etc. as different types on which many functions can be applied.

LISP is one the first and most popular functional programming language designed by McCarthy in 1958. In this language, the core data type are the atoms (or terms), lists, and functions. Lisp is known for its many innovative principles such as dynamic typing principle. It is particularly popular in Artificial Intelligence applications, in Automated Theorem Provers, and in the design of other programming languages. For example, Common Lisp was used as input and design language to create ACL2 (A Computational Logic for Applicative Common Lisp), which is basically used in the automated reasoning systems such as formal verification.

Another important functional programming language is ML, for Meta Language, which is derived from Lisp with strong type system. It is known for its type safety based on a polymorphic type system [9, p. 353]. It is widely used in the design of formal languages and theorem provers.

3. Curry-Howard Correspondence and Theorem Provers

One of the most striking results that connect Logic and Type theory is the Curry-Howard correspondence. It shows a deep relationship between Logic (usually constructive) and type systems. The basic correspondence (or isomorphism) states that programs and proofs are equivalent. The fact of using a constructive or intuitionistic proof of the existence of a certain object allows the use of this proof as a program that creates instances of that object. In other words, given a logical proposition P, a proof of P corresponds exactly to an example of type P.

This concept is widely used in the design of theorem provers. Thus, considering the type systems terminologies, a proof is a well-typed program; a type is isomorphic to a proposition, and an inhabited type is a truth or a theorem. Other correspondences are listed below in Table 1.

Many theorem provers, such as Coq, use an extension of lambda-calculus called Calculus of Inductive Constructions as the logical basis of these provers. In fact, this calculus uses the approach that considers a proposition as type discussed above.

Fig. 1 Table 1 CORRESPONDENCE BETWEEN TYPE THEORY AND LOGIC

Source: Propositions as Types, Curry-Howard Isomorphism; Klaus Ostermann Aarhus University; Educational slides.

As I already mentioned, Russell's type theory leading to Church's simple Type Theory, and then extended to the Calculus of Inductive Construction, occupies a fundamental part in several interactive “provers” or computer-assisted reasoning.

Perhaps, as suggested in [10, p.9], one of the most important contributions of “Principles of Mathematics” is its capacity to promote the proposition-as-type principle, and more generally to connect Logic to formal type systems. Consequently, Type systems provided a strong computational interpretation to Logic.

Type Theory has been used as the basic model (or meta-language) of many interactive automated reasoning systems. These provers include, among others, Coq, HOL, Twelf, and Agda.

They usually provide constructive proofs of mathematical statements or correctness and verification of other systems. This idea about the use of type theory in computer science was interestingly described in [10, p. 1] as follows: