The concept of “type” has been used without a precise definition in discussions about programming languages for 60 years. The set of people with a technical interest in programming languages is a broad one, and although many distinct, precise definitions have been used consistently within distinct subsets, I have long harboured a sense that discourse between such groups is unnecessarily strained by the cross purposes which arise in discussions mentioning the word “type”. In this essay I explore this matter from both a personal perspective and a historical one. I argue that two essential notions of “type” arose independently – one from programming traditions and the other from symbolic logic traditions – and despite a prevailing presumption to the contrary (on both sides), they have never been explicitly unified in the literature. I’ll also argue that having recognised the distinction, it might be more profitable to leave them unreconciled and distinct, owing to some fundamental differences in nature between mathematical truths and “economic truths”. Nevertheless, I argue that trending developments in both the theory and practice of programming make it important to resolve our differences, and offer some personal thoughts about how to do so.