Several Types of Types in Programming Languages

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

  • PDF / 186,300 Bytes
  • 12 Pages / 439.37 x 666.142 pts Page_size
  • 69 Downloads / 220 Views

DOWNLOAD

REPORT


Dipartimento di Informatica–Scienza e Ingegneria, Universit` a di Bologna and INRIA, Bologna, Italy 2 Inria Sophia-Antipolis, Valbonne, France [email protected]

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. Keywords: Types · Programming languages Abstraction mechanisms

1

· History of computing ·

Introduction

Types are an important part of modern programming languages, as one of the prominent abstraction mechanisms over data1 . This is so obvious that we seldom realise that the concept of type we understand nowadays is not the same it was perceived in the sixties, and that it was largely absent (as such) in the programming languages of the fifties. Moreover, we now conflate the concept of “type” in programming languages with the concept of the same name in mathematical logic—an identification which may be (is it?) good for today, but 1

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

c IFIP International Federation for Information Processing 2016  Published by Springer International Publishing AG 2016. All Rights Reserved F. Gadducci and M. Tavosanis (Eds.): HaPoC 2015, IFIP AICT 487, pp. 216–227, 2016. DOI: 10.1007/978-3-319-47286-7 15

Several Types of Types in Programming Languages

217

which is the result of a (slow) convergence of two different paths, that started quite apart with different aims. Tracing and recounting this story in details, with the painstaking accuracy it merits, it is well beyond the limits of this paper—it could be the subject of a doctoral thesis. We will instead make several remarks (some historical, some of more conceptual character) that we hope will be useful 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 mechani