What do logicians mean by "type"?

I enjoy reading about formal logic as an occasional hobby. However, one thing keeps tripping me up: I seem unable to understand what's being referred to when the word "type" (as in type theory) is mentioned.

Now, I understand what types are in programming, and sometimes I get the impression that types in logic are just the same thing as that: we want to set our formal systems up so that you can't add an integer to a proposition (for example), and types are the formal mechanism to specify this. Indeed, the Wikipedia page for type theory pretty much says this explicitly in the lead section.

However, it also goes on to imply that types are much more powerful than that. Overall, from everything I've read, I get the idea that types are:

• like types in programming
• something that is like a set but different in certain ways
• something that can prevent paradoxes
• the sort of thing that could replace set theory in the foundations of mathematics
• something that is not just analogous to the notion of a proposition but can be thought of as the same thing ("propositions as types")
• a concept that is really, really deep, and closely related to higher category theory

The problem is that I have trouble reconciling these things. Types in programming seem to me quite simple, practical things (alhough the type system for any given programming language can be quite complicated and interesting). But in type theory it seems that somehow the types are the language, or that they are responsible for its expressive power in a much deeper way than is the case in programming.

So I suppose my question is, for someone who understands types in (say) Haskell or C++, and who also understands first-order logic and axiomatic set theory and so on, how can I get from these concepts to the concept of type theory in formal logic? What precisely is a type in type theory, and what is the relationship between types in formal mathematics and types in computer science?

(I am not looking for a formal definition of a type so much as the core idea behind it. I can find several formal definitions, but I've found they don't really help me to understand the underlying concept, partly because they are necessarily tied to the specifics of a particular type theory. If I can understand the motivation better it should make it easier to follow the definitions.)

Solution 1:

tl;dr Types only have meaning within type systems. There is no stand-alone definition of "type" except vague statements like "types classify terms". The notion of type in programming languages and type theory are basically the same, but different type systems correspond to different type theories. Often the term "type theory" is used specifically for a particular family of powerful type theories descended from Martin-Löf Type Theory. Agda and Idris are simultaneously proof assistants for such type theories and programming languages, so in this case there is no distinction whatsoever between the programming language and type theoretic notions of type.

It's not the "types" themselves that are "powerful". First, you could recast first-order logic using types. Indeed, the sorts in multi-sorted first-order logic, are basically the same thing as types.

When people talk about type theory, they often mean specifically Martin-Löf Type Theory (MLTT) or some descendant of it like the Calculus of (Inductive) Constructions. These are powerful higher-order logics that can be viewed as constructive set theories. But it is the specific system(s) that are powerful. The simply typed lambda calculus viewed from a propositions-as-types perspective is basically the proof theory of intuitionistic propositional logic which is a rather weak logical system. On the other hand, considering the equational theory of the simply typed lambda calculus (with some additional axioms) gives you something that is very close to the most direct understanding of higher-order logic as an extension of first-order logic. This view is the basis of the HOL family of theorem provers.

Set theory is an extremely powerful logical system. ZFC set theory is a first-order theory, i.e. a theory axiomatized in first-order logic. And what does set theory accomplish? Why, it's essentially an embedding of higher-order logic into first-order logic. In first-order logic, we can't say something like $$\forall P.P(0)\land(\forall n.P(n)\Rightarrow P(n+1))\Rightarrow\forall n.P(n)$$ but, in the first-order theory of set theory, we can say $$\forall P.0\in P\land (\forall n.n\in P\Rightarrow n+1\in P)\Rightarrow\forall n.n\in P$$ Sets behave like "first-class" predicates.

While ZFC set theory and MLTT go beyond just being higher-order logic, higher-order logic on its own is already a powerful and ergonomic system as demonstrated by the HOL theorem provers for example. At any rate, as far as I can tell, having some story for doing higher-order-logic-like things is necessary to provoke any interest in something as a framework for mathematics from mathematicians. Or you can turn it around a bit and say you need some story for set-like things and "first-class" predicates do a passable job. This latter perspective is more likely to appeal to mathematicians, but to me the higher-order logic perspective better captures the common denominator.

At this point it should be clear there is no magical essence in "types" themselves, but instead some families of type theories (i.e. type systems from a programming perspective) are very powerful. Most "powerful" type systems for programming languages are closely related to the polymorphic lambda calculus aka System F. From the proposition-as-types perspective, these correspond to intuitionistic second-order propositional logics, not to be confused with second-order (predicate) logics. It allows quantification over propositions (i.e. nullary predicates) but not over terms which don't even exist in this logic. Classical second-order propositional logic is easily reduced to classical propositional logic (sometimes called zero-order logic). This is because $\forall P.\varphi$ is reducible to $\varphi[\top/P]\land\varphi[\bot/P]$ classically. System F is surprisingly expressive, but viewed as a logic it is quite limited and far weaker than MLTT. The type systems of Agda, Idris, and Coq are descendants of MLTT. Idris in particular and Agda to a lesser extent are dependently typed programming languages.¹ Generally, the notion of type in a (static) type system and in type theory are essentially the same, but the significance of a type depends on the type system/type theory it is defined within. There is no real definition of "type" on its own. If you decide to look at e.g. Agda, you should be quickly disabused of the idea that "types are the language". All of these type theories have terms and the terms are not "made out of types". They typically look just like functional programs.

¹ I don't want to give the impression that "dependently typed" = "super powerful" or "MLTT derived". The LF family of languages e.g. Elf and Twelf are intentionally weak dependently typed specification languages that are far weaker than MLTT. From a propositions-as-types perspective, they correspond more to first-order logic.

Solution 2:

I've found they don't really help me to understand the underlying concept, partly because they are necessarily tied to the specifics of a particular type theory. If I can understand the motivation better it should make it easier to follow the definitions.

The basic idea: In ZFC set theory, there is just one kind of object - sets. In type theories, there are multiples kind of objects. Each object has a particular kind, known as its "type".

Type theories typically include ways to form new types from old types. For example, if we have types $A$ and $B$ we also have a new type $A \times B$ whose members are pairs $(a,b)$ where $a$ is of type $A$ and $b$ is of type $B$.

For the simplest type theories, such as higher-order logic, that is essentially the only change from ordinary first-order logic. In this setting, all of the information about "types" is handled in the metatheory. But these systems are barely "type theories", because the theory itself doesn't really know anything about the types. We are really just looking at first-order logic with multiple sorts. By analogy to computer science, these systems are vaguely like statically typed languages - it is not possible to even write a well-formed formula/program which is not type safe, but the program itself has no knowledge about types while it is running.

More typical type theories include ways to reason about types within the theory. In many type theories, such as ML type theory, the types themselves are objects of the theory. So it is possible to prove "$A$ is a type" as a sentence of the theory. It is also possible to prove sentences such as "$t$ has type $A$". These cannot even be expressed in systems like higher-order logic.

In this way, these theories are not just "first order logic with multiple sorts", they are genuinely "a theory about types". Again by analogy, these systems are vaguely analogous to programming languages in which a program can make inferences about types of objects during runtime (analogy: we can reason about types within the theory).

Another key aspect of type theories is that they often have their own internal logic. The Curry-Howard correspondence shows that, in particular settings, formulas of propositional or first-order logic correspond to types in particular type theories. Manipulating the types in a model of type theory corresponds, via the isomorphism, to manipulating formulas of first order logic. The isomorphism holds for many logic/type theory pairs, but it is strongest when the logic is intuitionistic, which is one reason intuitionistic/constructive logic comes up in the context of type theory.

In particular, logical operations on formulas become type-forming operations. The "and" operator of logic becomes the product type operation, for example, while the "or" operator becomes a kind of "union" type. In this way, each model of type theory has its own "internal logic" - which is often a model of intuitionistic logic.

The existence of this internal logic is one of the motivations for type theory. When we look at first-order logic, we treat the "logic" as sitting in the metatheory, and we look at the truth value of each formula within a model using classical connectives. In type theory, that is often a much less important goal. Instead we look at the collection of types in a model, and we are more interested in the way that the type forming operations work in the model than in the way the classical connectives work.

Solution 3:

I am not looking for a formal definition of a type so much as the core idea behind it. I can find several formal definitions, but I've found they don't really help me to understand the underlying concept, partly because they are necessarily tied to the specifics of a particular type theory. If I can understand the motivation better it should make it easier to follow the definitions.

Let me answer this from a more philosophical point of view, which perhaps would help to answer your implicit question of why logicians call type theories type theories and set theories set theories.

A set theory is a system intended to describes sets, in the specific sense that a set is a collection of objects. This means that the intended universe (also called world/domain) is split by each set $S$ into two parts, the members of $S$ and the non-members of $S$. There are a variety of set theories such as ZF[C] and NF[U] and extensions of them.

A type theory is a system intended to describe types, where a type is a kind of categorization or classification of objects. Whether an object $x$ is of type $S$ or not is typically not a boolean question, in the sense that one cannot form a sentence that is true if and only if $x$ is of type $S$. Instead, type theories have inference rules for typing judgements. Many type theories use syntax like "$x : S$" for the judgement that $x$ is of type $S$. It is not a boolean expression; "$\neg ( x : S )$" is simply syntactically malformed. A typing rule might look like "$x : S \ , \ f : S \to T \vdash f(x) : T$", and in some sense this is one of the fundamental rules that we can expect every type theory to have in some form or other.

In any case, the notion of a type is only made precise via a type theory, just as the notion of a set is only made precise via a set theory. Note that ZFC and NFU are incompatible, and so they describe incompatible notions of sets. Likewise, there are numerous incompatible type theories that describe different notions of types. In the worst case, a notion of sets or types may be inconsistent, which we of course have to discard. Ideally, one would like a philosophically cogent or justifiable notion.

[Types are] something that can prevent paradoxes

There is nothing inherent in types that can prevent paradoxes. As has been pointed out, some attempts at foundational type theories have turned out to be inconsistent in similar manner as naive set theory.

But in type theory it seems that somehow the types are the language, or that they are responsible for its expressive power in a much deeper way than is the case in programming.

Types in programming are very 'weak' in the sense that every modern programming language has a type system with decidable typing, because the compiler must terminate and return success or failure of compilation, and hence must be able to perform whatever type checking is guaranteed by the language. Some languages (like Javascript) have duck typing, which effectively means no type checking. Other languages (like Java) have rather strict typing, and the whole type system (with generics) is decidable (if you do not use type-casting), so every Java program can be statically checked for type correctness (there will be no run-time type error).

In contrast, in classical mathematics we cannot have decidable typing in general, because we want to be able to perform classical arithmetic, which allows us to construct and reason about arbitrary programs (equivalently Turing machines), and Godel's incompleteness theorem forces our hand. Therefore in every type theory that supports constructing partial functions representing programs, it cannot be computably determined for general $x,S$ whether the judgement "$x : S$" is provable or not.

The trade-off is always there. You can never have both decidable type-checking and the ability to handle arbitrary (classical) arithmetic reasoning. In type-theoretic terms, you cannot have both normalization of every term and the ability to construct arbitrary programs before proving their properties.

However, the sorts in higher-order logic can be viewed as types in simple type theory, and in turn the function types in simple type theory could be understood via currying as types of programs.

Solution 4:

Can I recommend a (text)book to you? Types and Programming Languages, by Benjamin C. Pierce. I come from a math background and work as a programmer. I picked up this book because I would look at papers by computer scientists (think Philip Wadler when he's not bothering to be beginner-friendly) and feel uneasy because I didn't know the basis for what they would say, and without that basis it all seemed a little loosey-goosey.

The text is written at the level of a good first-year grad school course in type theory, and I found it to be clear and well written, an enjoyable read. And even though I didn't work my way through hardly any of the exercises I feel a lot more comfortable now when I read things that use or reference types.

To be clear, the book won't answer the core questions you asked, but I think it'll put you in a much better position for understanding the questions and answers, plus you'll have a bunch of concrete examples to anchor everything in.