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.)
logic soft-question type-theory
NathanielNathaniel
$\begingroup$ In general types are "categories" and thus are exactly as types in programming. We have Type Theory introduced in logic to avoi paradoxes (alternative theory with respect to set theory). $\endgroup$ – Mauro ALLEGRANZA Mar 11 '18 at 11:24
$\begingroup$ Start here en.wikipedia.org/wiki/Type_theory ... the advantage in ZF and other modern set theory formulations is: there is only one type, everything is a "set". A function is a set. A relation is a set. A relation of functions is a set, etc. $\endgroup$ – GEdgar Mar 11 '18 at 11:30
$\begingroup$ @GEdgar that link is already in my question - it doesn't answer it. $\endgroup$ – Nathaniel Mar 11 '18 at 11:31
$\begingroup$ "Types in programming seem to me quite simple"... the concept is simple, as simpe is the concept of set. But the simple (naive) concept of sets led to paradoxes. Axiomatic set theory put "constraints" (specific axioms) on the simple concept of set aimed at salvaging its foundational role but avoiding paradoxes. $\endgroup$ – Mauro ALLEGRANZA Mar 11 '18 at 12:27
$\begingroup$ Following up on @Mauro ALLEGRANZA's nice comments - just as early set theory was inconsistent and had to be fixed, early type theory was also inconsistent and had to be fixed (this is the origin of Curry's paradox). In both cases, the problem was that the authors of the original axioms tried to do "too much", and so modern systems only try to capture part (hopefully consistent) of the original systems. $\endgroup$ – Carl Mummert Mar 11 '18 at 12:54
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.1 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.
1 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.
Derek Elkins left SEDerek Elkins left SE
$\begingroup$ Incidentally one of the best things I'm getting out of this is looking into Agda, which I hadn't heard of before. It seems to not only be quite a neat language with features that are helping me "get" what dependent types are, but also to have more than one very nicely written tutorial. $\endgroup$ – Nathaniel Mar 13 '18 at 13:52
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.
Carl MummertCarl Mummert
$\begingroup$ "More typical type theories include ways to reason about types within the theory." <--- this is probably the key concept that I needed to understand. I will sleep now and look more into this tomorrow. $\endgroup$ – Nathaniel Mar 11 '18 at 14:34
$\begingroup$ @Nathaniel: this is one reason why the syntax of type theories and the way that their deductive systems look is so different than the way the syntax of first-order logic (even with multiple sorts) looks. The syntax and deductive system of type theories need to accommodate the fact that the "types" in one model may not be the same as the "types" in another model. $\endgroup$ – Carl Mummert Mar 11 '18 at 14:58
$\begingroup$ "[T]hese systems are vaguely analogous to dynamically typed programming languages in which a program can make inferences about types of objects during runtime[.]" This is extremely misleading. You can't directly do something like if typeof(x)=Nat then ... else ... in MLTT say. (You can accomplish something similar but more limited by encoding a Tarskian universe.) The experience of working within MLTT is totally unlike working in a dynamically typed language. There is generally still a phase separation. ZFC set theory is more like a dynamically typed language than MLTT. $\endgroup$ – Derek Elkins left SE Mar 11 '18 at 22:36
$\begingroup$ @Derek Elkins: I was hoping that the weasel words would be enough to avoid too much criticism :) But anyway, in any model of MLTT we can use the usual T-schema to assign truth values to sentences such as "if $t:\sigma$ then .. .else ..." where the ... are also basic propositions that are true or false in the model, and we can easily add inference rules to allow us to deduce these more complicated judgments. Of course, the reason for not doing this from the start is that the basic judgments themselves - which are directly about types and terms - are the main source of interest. $\endgroup$ – Carl Mummert Mar 12 '18 at 0:01
$\begingroup$ Can you give an example of what you mean? MLTT doesn't have formulas and $t:\sigma$ doesn't have a value (or a truth-value) within the system. It's not an expression of MLTT. (It can be viewed as a metalogical statement though.) By "Tarskian universe" I mean something like what's described at the bottom of this page. You can then have values of type $\sum_{u:U}T(u)$ and since $U$ is just a normal data type, you can case analyze it. But this doesn't help with an arbitrary variable in the actual universe. $\endgroup$ – Derek Elkins left SE Mar 12 '18 at 0:22
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.
$\begingroup$ The last part is not true at all. Type checking in Martin-Löf Type Theory is decidable, and variants of MLTT are often the systems most viewed as being potential alternate foundations of math. The lack of decidable type checking would be a huge problem for most type theories, or at least would dramatically change the character (e.g. the difference between NuPRL and Agda). As for programming languages, most do have relatively weak type systems, but some like Idris and Agda are straight-up implementations of variants of MLTT. $\endgroup$ – Derek Elkins left SE Mar 11 '18 at 22:44
$\begingroup$ In particular, the sort of way that incompleteness will manifest itself is that you will have a type $S$, and you cannot prove whether or not it is possible to construct a term of type $S$. $\endgroup$ – user14972 Mar 12 '18 at 2:25
$\begingroup$ @DerekElkins I believe the last statement wasn't about decidable type-checking (which is often true and desirable), but rather about decidable propositions, or more broadly, that it is decidable whether every type is inhabited. This indeed cannot be true for any foundational type theory. $\endgroup$ – Anton Fetisov Mar 12 '18 at 3:36
$\begingroup$ @DerekElkins: Sorry I didn't mean type-checking in the sense you mean. I meant that to permit construction of arbitrary programs you cannot have decidable checking of whether a program satisfies some requirements or not, which could be viewed as asking whether it is of some type or not. In languages like MLTT one cannot construct and analyze all possible programs for precisely this reason. Unless you reject classical logic, MLTT cannot serve as a complete alternative foundation for mathematics. However, I will edit my post since it was unclear. $\endgroup$ – user21820 Mar 12 '18 at 4:59
$\begingroup$ @Wildcard: That's wrong. Russell's construction can be done using just one instance of the specification schema over the underlying first-order logic, and no other axioms! The inconsistency of naive set theory does not depend on anything to do with infinity. $\endgroup$ – user21820 Mar 14 '18 at 8:39
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.
JonathanZ supports MonicaCJonathanZ supports MonicaC
The types of type theory are the same as the types of theoretical computer science. In type theory an objects inhabits a type but do not share types. The important thing about types is that that there is a correspondence between types and intuistic logic.
Sum/Union types which in Haskell you define by using the | correspond to the logical or.
data Either x y = Left x | Right y
The product types correspond to the logical and
data Both x y = Both x y
Finally the logical implies corresponds to the function type
data Implies x y = x -> y
You can translate any mathematical statement into a type using product, sum, function and a few other extra types. If you can then write a computer program that can implement the type given that computer program is a proof of the mathematical statement.
Q the PlatypusQ the Platypus
Not the answer you're looking for? Browse other questions tagged logic soft-question type-theory or ask your own question.
Computability viewpoint of Godel/Rosser's incompleteness theorem
Rigorous definition of a type
Variables in Types in type theory
Type theory as foundations
Relationship between propositional logic, first-order logic, second-order logic higher-order logic, and type theory
Logic within Type theory. Is there a rough academic consensus on how this should be done?
What does it mean to axiomatize a logic?
Group theory vs Type theory
(Higher order) logic/type theory/category theory like (meta-)grammar/language/machine?
If Type Theories are all Logics.
Axiom checking as type checking?