Last call to make your voice heard! Our 2022 Developer Survey closes in less than a week. Take survey.
39 votes

Why colon to denote that a value belongs to a type?

The main reason to prefer the colon notation $t : T$ to the membership relation $t \in T$ is that the membership relation can be misleading because types are not (just) collections. [Supplemental: I ...
user avatar
  • 26.4k
36 votes
Accepted

What are some good introductory books on type theory?

Software Foundations by Benjamin C. Pierce would be a good place to start. It would be a make a good precursor to his Types and Programming Languages. There is also Simon Thompson's Type Theory and ...
user avatar
27 votes

What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?

I've already answered somewhat, but I'll try to give a more detailed overview of the type theoretical horizon, if you will. I'm a bit fuzzy on the historical specifics, so more informed readers will ...
user avatar
  • 13.1k
24 votes
Accepted

Why was there a need for Martin-Löf to create intuitionistic type theory?

Very briefly: the simply-typed $\lambda$-calculus does not have dependent types. Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from ...
user avatar
22 votes
Accepted

Why it's impossible to declare an induction principle for Church numerals

The question you are asking is interesting and known. You are using the so-called impredicative encoding of the natural numbers. Let me explain a bit of the background. Given a type constructor $T : \...
user avatar
  • 26.4k
21 votes

Is there a typed lambda calculus which is consistent and Turing complete?

Alright I'll give a crack at it: In general for a given type system $T$, the following is true: If all well-type terms in the calculus $T$ are normalizing, then $T$ is consistent when viewed as a ...
user avatar
  • 13.1k
21 votes
Accepted

Subtypes as subsets of SML datatypes

These kinds of types -- where you define a subtype (basically) by giving a grammar of the acceptable values -- are called datasort refinements. They were introduced by Tim Freeman and Frank Pfenning,...
user avatar
20 votes
Accepted

Types which correspond to sets of cardinality of continuum

You must be careful here. You are using set-theoretic concepts (cardinal, continuum) outside set theory. There is potential for confusion. Your question can be understood in several ways. Maybe you ...
user avatar
  • 26.4k
20 votes
Accepted

Why do constructivists not seem to care too much about call/cc

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive ...
user avatar
  • 26.4k
20 votes
Accepted

Is MLTT effectively pCiC without Prop?

The short answer is yes, MLTT can reasonably be equated with CIC without impredicative Prop. The main technical issue is that there are dozens of variants when one ...
user avatar
  • 13.1k
20 votes
Accepted

Relative consistency of PA and some type theories

The short answer to your question 1 is no, but for perhaps subtle reasons. First of all, System $F$ and $F_\omega$ cannot express the first-order theory of arithmetic, and even less the consistency ...
user avatar
  • 13.1k
20 votes
Accepted

Swapping arguments of variables in higher-order pattern unification

I have developed this, but haven't yet published it in a more strucured/formal manner. "Enhanced pattern unification" abstract here. Demo implementation. Video recording. You're absolutely ...
user avatar
17 votes
Accepted

Dependent Sums and Products

I think what's confusing you is that $A \times B$ is both a product and a coproduct: It is the product of two factors, namely $A$ and $B$. It is the coproduct of $A$-many copies of $B$. Once you ...
user avatar
  • 26.4k
17 votes

Why study type theory?

Type theories in which every type is inhabited are far from being useless. True enough, through the eyes of logic they are inconsistent, but there are other things in life apart from logic. A general ...
user avatar
  • 26.4k
16 votes

In the Hott book, are the most of the type formers redundant? And if so, why?

You are asking several questions which are similar but distinct. Why doesn't the HoTT book use Church encodings for data types? Church encodings do not work in Martin-Löf type theory, for two ...
user avatar
15 votes

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

To me, your question seems analogous to saying "I've heard that non-Euclidean geometry requires me to give up Euclid's fifth axiom, which is very useful in many mathematical contexts." You don't have ...
user avatar
  • 251
15 votes
Accepted

In the Hott book, are the most of the type formers redundant? And if so, why?

Let me explain why the suggested encoding of the empty type does not work. We need to be explicit about universe levels and not sweep them under the rug. When people say "the empty type", they might ...
user avatar
  • 26.4k
14 votes
Accepted

Algorithm to determine function equality on the simply typed lambda calculus?

As I said in my comment, the answer in general is no. The important point to understand (I say this for Viclib, who seems to be learning about these things) is that having a programming language/set ...
user avatar
14 votes
Accepted

Is this behavior in a programming language inconsistent?

Yes, your type inference seems incomplete. This example can be dealt with fairly trivially, by computing the respective type equations, e.g. in the style Hindley/Milner does it. Alpha-renaming the ...
user avatar
14 votes
Accepted

Minimal specification of Martin-Löf type theory

The purpose of the system described in the appendix of the HoTT book is to present something that corresponds to what is used by the book. The book is aiming to be educational. Therefore it would be a ...
user avatar
  • 26.4k
14 votes
Accepted

Logical Reations for an Impredicative System in a Predicative MetaTheory

In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent ...
user avatar
  • 13.1k
14 votes
Accepted

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

You seem to be confusing several things here. First of all, like Alexis said in her answer, I don't see why you would need to accept/reject the principles of a given logical theory in order to study ...
user avatar
14 votes
Accepted

Why colon to denote that a value belongs to a type?

Because what's on the right of the colon isn't necessarily a set and what's on the left of the colon isn't necessarily a member of that set. Type theory started out in the early 20th century as an ...
user avatar
13 votes
Accepted

Ramification of An Impredicative Type Theory

I'm going to elaborate my comments into an answer. The origins of predicative type theory are almost as old as type theory itself, since one of Russel's motivations was to ban "circular" definitions ...
user avatar
  • 13.1k
13 votes
Accepted

Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?

First, you are confusing consistency of CIC as an equational theory with consistency of CIC as a logical theory. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent....
user avatar
13 votes
Accepted

Is there a good notion of non-termination and halting proofs in type theory?

Because one of the principal applications of Type Theory in formalizations has been to study programing languages and computation in general, a lot of thought has gone into ways of representing ...
user avatar
  • 13.1k
13 votes
Accepted

Can Isorecursive types capture mutually recursive data types?

In general, for any type (or domain, or complete lattice) $X$ we can consider the least fixed-point operator $\mu_X : (X \to X) \to X$. For recursive types we take $X = \mathsf{Type}$, i.e., we apply $...
user avatar
  • 26.4k
13 votes
Accepted

Defining inductive types in intensional type theory purely in terms of type-theoretic data

It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types ...
user avatar
13 votes
Accepted

Why is regularity a problem in cubical type theory?

The difficulty is in making such a reduction compatible with all the other reductions involving transport/coe. From one perspective it is a “confluence” problem. It is unfortunate that in the ...
user avatar
13 votes
Accepted

Which universities in the U.S. are doing research in type theory?

Any such list is always subjective, but the best approach to answer this question is: Look at journals/conferences in the area you're interested in. For type theory, I'd look at LICS, LMCS, POPL, ...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible