Abstract: The concept of “type” has been used without a consistent,
precise definition in discussions about programming languages for 60 years.1 In this essay I explore various concepts
lurking behind distinct uses of this word, highlighting two
traditions in which the word came into use largely independently: engineering traditions on the one hand, and those of
symbolic logic on the other. These traditions are founded on
differing attitudes to the nature and purpose of abstraction,
but their distinct uses of “type” have never been explicitly
unified. One result is that discourse across these traditions
often finds itself at cross purposes, such as overapplying one
sense of “type” where another is appropriate, and occasionally proceeding to draw wrong conclusions. I illustrate this
with examples from well-known and justly well-regarded literature, and argue that ongoing developments in both the
theory and practice of programming make now a good time
to resolve these problems.
Comments