2014/10/14 by Stephen Kell · 1 voice · 9 citations
Computer Science · #Abstraction #Artificial intelligence #Computer science #Epistemology #Linguistics #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Philosophy #Programming language #Software Engineering Research #Type (biology) #Word (group theory)
paper · doi:10.1145/2661136.2661154
openalex publication_date 2014/10/14 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/29
The concept of "type" has been used without a consistent, precise definition in discussions about programming languages for 60 years1. 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.