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

Type ::= ... | QuantifiedType QuantifiedType ::= VA. T ype | Universal Quantification EA. Type | Existential Quantification VAcType. Type | EAcType. Type Bounded Quantification

As shown above, this notion uses quantifiers over an interval of subtypes of a specific type. Bounded quantification, which connects subtyping with parametric polymorphism, improves lambda-calculus. In fact, inheritance is used in a way that subtypes are created as specialized entities regarding the supertypes.

In other words, in object-oriented languages types are defined as bounded quantification, and can be seen as supertypes allowing the creation of subtypes by inheritance.

The lambda-calculus improved by these different notions (polymorphism, inheritance, etc.) and supporting well the type systems can perfectly model important programming principles such as data abstractions.

In this paper we have seen how a challenging philosophical question aimed to prove the logicism position in the philosophy of Mathematics has led Russell and Whitehead to develop the type theory. It failed to realize this objective, but succeeded in building involuntarily major foundations in computer science. Practically, type systems are used to detect errors in computer programs before appearing as runtime errors which are more critical. This kind of program-analysis has drastically improved the software quality. In addition, type theory has been fundamental in building type checking algorithms in the semantic stage of the languages compilers design [7, p.4].

Hence, as mentioned in [7, p.2], three central domains where type theory is inevitably used are the typed programming languages, the type-driven program analysis and optimization, and type-aided security mechanisms.

Furthermore, the theoretical studies of type theory have been used as mathematical basis to the Church' typed lambda-calculus and the intuitionistic type theory developed by Per Martin-Lцf [11]. Other fundamental theoretical results, such as the Curry-Howard isomorphism, have shown during decades their importance in practical use of computer science in general, and in the design of automated theorem proving and formal verification in particular.

1. Gottlob Frege 1879. Begriffsschrift, Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, English translation in Jean van Heijenoort (ed.), From Frege to Gцdel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, pp. 1-82, 1977.

2. Alfred North Whitehead and Bertrand Russell. Principia Mathematica. 1910-1913. Cambridge University Press, Cambridge, revised edition, 19251927.

3. Kurt Gцdel. 1934. On undecidable propositions of formal mathematical systems.

4. Reprinted with revisions in Davis (1965), 39-74.

5. Donald Gillies. 2002. Logicism and the development of computer science, A. C. Kakas and F. Sadri (eds,): Computational Logic, Springer-verlag Berlin Heidelberg, pp. 588-604.

6. Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, and Victor Vianu. 2001. On the Unusual Effectiveness of Logic in Computer Science, The Bulletin of Symbolic Logic, volume 7, issue 2, pp. 213-236.

7. Luca Cardelli, Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. Computing Surveys, Vol 17 n. 4, pp 471-522.

8. Cйsar Munoz. 1999. Type Theory and Its Applications to Computer Science. News Letter of the Institute for Computer Applications in Science and Engineering (ICASE), Vol. 8, No. 4.

9. Alonso Church. 1940. A Formulation of the Simple Theory of Types, Journal of Symbolic Logic, 5, pp. 56 68.

10. Robin Milner. 1977. A theory of type polymorphism in programming. J. Comp. Syst. Scs., 17:348-375.

11. Robert L. Constable. 2011. The Triumph of Types: Creating a Logic of Computational Reality. Cornell university. www.semanticscholar.org

12. Per Martin-Lцf. 1984. Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, Naples, Italy.