Top

Published in:

2016 | OriginalPaper | Chapter

Several Types of Types in Programming Languages

Author : Simone Martini

Published in: History and Philosophy of Computing

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Types are an important part of any modern programming language, but we often forget that the concept of type we understand nowadays is not the same it was perceived in the sixties. Moreover, we conflate the concept of “type” in programming languages with the concept of the same name in mathematical logic, an identification that is only the result of the convergence of two different paths, which started apart with different aims. The paper will present several remarks (some historical, some of more conceptual character) on the subject, as a basis for a further investigation. We will argue that there are three different characters at play in programming languages, all of them now called types: the technical concept used in language design to guide implementation; the general abstraction mechanism used as a modelling tool; the classifying tool inherited from mathematical logic. We will suggest three possible dates ad quem for their presence in the programming language literature, suggesting that the emergence of the concept of type in computer science is relatively independent from the logical tradition, until the Curry-Howard isomorphism will make an explicit bridge between them.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter From Information to Perception

next chapter Playfulness and the Advent of Computerization in Spain: The National Club of ZX81 Users

Even in “untyped” languages (Python, say) types are present and relevant.

Which is not to say when it was first used in that context. To our knowledge, the very first technical use of the term “type” in programming is H.B. Curry’s [9], to distinguish between memory words containing instructions (“orders”) and those containing data (“quantities”). These reports by Curry, as reconstructed by [12], contain a surprising and non-trivial mathematical theory of programs, up to a theorem of the style “well-typed expressions do not go wrong”! Despite G.W. Patterson’s review on JSL 22(01), 1957, 102–103, we do not know of any influence of this theory on subsequent developments of programming languages.

Of course the distinction between integers and floating points—that is, a type-based distinction, in today’s terminology—was present and used, to decide the memory layout of the different kinds of variables, and to compile into the correct arithmetic operations.

Recall that type is not a reserved word in Algol 58—it is used in the report for the “symbolic representative of some type declarator such as” INTEGER, BOOLEAN, etc.

Alan Perlis summarises in 1978, referring to Algol 58: “The use of ‘type,’ as in ‘x is of type real,’ was analogous to that employed in logic. Both programming language design and logic dipped into the English language and came up with the same word for roughly the same purpose” [32].

E.g., “ALGOL \((\ldots )\) lacks the ability to describe different kind of data” [27] (note that once again the generic “kind” is used, and not “type”). Cfr also [33], page 244.

Category theory and Bourbaki are clearly at an arm’s length, but there is no explicit reference to them in the paper.

It is a “structure,” in C’s terminology.

More precisely: dynamically allocated structure which do not follow a stack-based life policy.

Hoare’s paper will have significant impact also on Algol 68—the legitimate child of the Algol committee—which contains references and structured types. Tracing the genealogy of Algol 68’s modes (Algol 68’s terminology for types) is however a task that should be left for the future.

In John Reynolds’s words from 1983, “Type structure is a syntactic discipline for enforcing levels of abstraction” [35]. Or in those of Luca Cardelli and Peter Wegner from their seminal 1985 paper, “The objective of a language for talking about types is to allow the programmer to name those types that correspond to interesting kinds of behavior” [5].

From the terminological point of view, the paper uses “classes” when referring to records, and “types” for simple types (integer, real, boolean and references, which are typed: the type of a reference includes the name of the record class to which it refers). On page 48, however, discussing the relations with McCarthy’s proposal, we find cristal-clear awareness: “The current proposal represents part of the cartesian suggestion made by Prof. J. McCarthy as a means of introducing new types of quantity into a language.” From Hoare’s expression “record class”, Dahl and Nygaard derive the term “object class” in Simula 67 [10], then simply “class” in the object oriented jargon.

Morris talks about “protection,” “authentication”, “secrecy”.

The story of abstract data types, their relation to polymorphism, and how their parabola gives way to object oriented programming, is something to be told in a different paper, see [25].

This is not the place where to discuss the emergence and the evolution of the concept of type in logic—we will limit ourselves to a single glimpse on the view of Russell and Whitehead, which will be the dominant one in the twentieth century. Stratification, or classification, in types, orders, or similar ways was already present in the nineteenth century, see, for instance, Frege’s Stufe (in the Grundgesetze; before he also used Ordnung), usually translated with “level”, or “degree”.

“Well-typed expressions do not go wrong.” [28].

For a lucid account of the interplay between types, constructive mathematics, and lambda-calculus in the seventies, see [6], Sect. 8.1.

See, for instance, the Introduction to [28] which calls for polymorphism to ensure flexibility. Damas-Milner [15] type inference provides a powerful mechanism for enforcing type restrictions while allowing more liberal (but principled) reasoning.

This emphasis on the moral need for a programming language to assist (or even guide) the programmer in avoiding bugs or, worse, unintended behaviour in a program, is the core of what Mark Priestly [33] identifies as the “Algol research program”, a way of thinking to the design of programming languages which still today informs most work in programming language research.

Backus, J.W., Bauer, F.L., Green, J., Katz, C., McCarthy, J., Perlis, A.J., Rutishauser, H., Samelson, K., Vauquois, B., Wegstein, J.H., van Wijngaarden, A., Woodger, M.: Report on the algorithmic language ALGOL 60. Commun. ACM 3(5), 299–314 (1960)MathSciNetCrossRefMATH

Backus, J.W., Diselets, P.H., Evans, D.C., Goodman, R., Huskey, H., Katz, C., McCarthy, J., Orden, A., Perlis, A.J., Rich, R., Rosen, S., Turanski, W., Wegstein, J.: Proposal for a programming language. Technical report, ACM Ad Hoc Committee on Languages (1958)

Backus, J.W., et al.: The FORTRAN automatic coding system for the IBM 704 EDPM. IBM (1956)

Bauer, F.L., Bottenbruch, H., Rutishauser, H., Samelson, K.: Proposal for a universal language for the description of computing processes. In: Computer Programming and Artificial Intelligence, pp. 355–373. University of Michigan Summer School (1958)

Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17(4), 471–523 (1985)CrossRef

Cardone, F., Hindley, J.R.: Lambda-calculus and combinators in the 20th century. In: Gabbay, D.M., Woods, J. (eds.) Logic from Russell to Church, vol. 5 of Handbook of the History of Logic, pp. 723–817. North-Holland (2009)

Church, A.: A formulation of the simple theory of types. JSL 5, 56–68 (1940)MathSciNetMATH

Curry, H.B., Feys, R.: Combinatory Logic. North Holland, Amsterdam (1958)MATH

Curry, H.B.: On the composition of programs for automatic computing. Technical Report Memorandum 10337, Naval Ordnance Laboratory (1949)

10.

Dahl, O.-J.: The birth of object orientation: the Simula languages. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol. 2635, pp. 15–25. Springer, Heidelberg (2004). doi:10.1007/978-3-540-39993-3_3 CrossRef

11.

Dahl, O.-J., Nygaard, K.: Simula: an ALGOL-based simulation language. Commun. ACM 9(9), 671–678 (1966)CrossRefMATH

12.

De Mol, L., Carlé, M., Bullyinck, M.: Haskell before Haskell: an alternative lesson in practical logics of the ENIAC. J. Logic Comput. 25(4), 1011–1046 (2015)MathSciNetCrossRefMATH

13.

Girard, J.Y.: Une extension de l’interprétation de Gödel à l’analyse et son application à l’élimination des coupures dans l’analyse et la théorie des types. In: Proceedings of the Second Scandinavian Logic Symposium, vol. 63 of Studies in Logic and the Foundations of Mathematics, pp. 63–92. North-Holland, Amsterdam (1971)

14.

Goldberg, A., Kay, A.: Smalltalk-72 instruction manual. Technical Report SSL 76–6. Learning Research Group, Xerox Palo Alto Research Center (1976)

15.

Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: a mechanised logic of computation. LNCS, vol. 78. Springer, Berlin Heidelberg (1979)

16.

Hindley, R.: The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, 29–60 (1969)MathSciNetMATH

17.

Hoare, C.A.R.: Record handling. ALGOL Bull. 21, 39–69 (1965)MATH

18.

Hoare, C.A.R.: Further thoughts on record handling. ALGOL Bull. 23, 5–11 (1966)

19.

Hoare, C.A.R.: Notes on data structuring. In: Dahl, O.-J., Dijkstra, E.W., Hoare, C.A.R. (eds.) Structured programming, pp. 83–174. Academic Press (1972)

20.

Hoare, C.A.R.: Personal communication (2014)

21.

Hopper, G.M.: Automatic programming: present status and future trends. In: Mechanisation of Thought Processes: Proceedings of a Symposium held at the National Physical Laboratory, vol. I, pp. 155–194. HMSO, London (1959)

22.

Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479–490. Academic Press (1980)

23.

Kay, A.C.: The early history of smalltalk. SIGPLAN Not. 28(3), 69–95 (1993)CrossRef

24.

Martin-Löf, P.: Constructive mathematics and computer programming. In: Cohen, L.J., et al. (eds.) Logic, Methodology and Philosophy of Science VI, 1979, pp. 153–175. North-Holland, Amsterdam (1982)

25.

Martini, S.: Types in programming languages, between modelling, abstraction, and correctness. In: Beckmann, A., Bienvenu, L., Jonoska, N. (eds.) CiE 2016. LNCS, vol. 9709, pp. 164–169. Springer, Heidelberg (2016). doi:10.1007/978-3-319-40189-8_17 CrossRef

26.

McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, part I. Commun. ACM 3(4), 184–195 (1960)CrossRefMATH

27.

McCarthy, J.: A basis for a mathematical theory of computation, preliminary report. In: Papers Presented at the May 9–11, 1961, Western Joint IRE-AIEE-ACM Computer Conference, IRE-AIEE-ACM 1961 (Western), pp. 225–238, New York, NY, USA. ACM (1961)

28.

Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348–375 (1978)MathSciNetCrossRefMATH

29.

Morris, J.H.: Lambda-calculus models of programming languages. Ph.D. thesis, MIT (1968)

30.

Morris, J.H.: Types are not sets. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1973, pp. 120–124, New York, NY, USA. ACM (1973)

31.

Perlis, A.J., Samelson, K.: Preliminary report: International algebraic language. Commun. ACM 1(12), 8–22 (1958)CrossRefMATH

32.

Perlis, A.J.: The American side of the development of Algol. In: Wexelblat, R.L. (ed.) History of Programming Languages I, pp. 75–91, ACM, NY, USA (1981)

33.

Priestley, M.: A Science of Operations: Logic and the Invention of Programming. Springer, London (2011)CrossRefMATH

34.

Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed) Programming Symposium, Colloque sur la programmation. LNCS, vol. 19, pp. 408–423. Springer, London (1974)

35.

Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R.E.A. (ed.) Information Processing 83. Proceedings of the IFIP 9th World Computer Congress, pp. 513–523. North-Holland/IFIP, Paris (1983)

36.

Sites, R.L.: Sites. Algol W reference manual. Technical Report STAN-CS-71-230, Computer Science Department, Stanford University (1972)

37.

Alfred North Whitehead and Bertrand Russell. Principia Mathematica. Cambridge University Press (1910)

38.

Whitehead, A.N., Russell, B.: A contribution to the development of ALGOL. Commun. ACM 9(6), 413–432 (1966)CrossRef

Title: Several Types of Types in Programming Languages
Author: Simone Martini
Publisher: Springer International Publishing
Book: History and Philosophy of Computing
Print ISBN: 978-3-319-47285-0

Electronic ISBN: 978-3-319-47286-7

Copyright Year: 2016
DOI: https://doi.org/10.1007/978-3-319-47286-7_15

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner