Skip to main content
Share Your Experience: Take the 2024 Developer 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 ...
Andrej Bauer's user avatar
  • 29.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,...
Neel Krishnaswami's user avatar
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 ...
cody's user avatar
  • 13.9k
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 ...
András Kovács's user avatar
16 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 ...
Alexis's user avatar
  • 261
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 ...
Neel Krishnaswami's user avatar
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 ...
Andrej Bauer's user avatar
  • 29.1k
15 votes
Accepted

What is the difference between System F and Hindley-Milner type system?

Yes, In Hindley-Milner universal quantifiers are allowed only at the outside of a type (and therefore omitted). For example, in HM you can have the type $\forall \alpha.(\alpha\to\alpha) \to (\alpha\...
Martin Hofmann's user avatar
15 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 ...
Jonathan Sterling's user avatar
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 ...
Damiano Mazza's user avatar
14 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 $...
Andrej Bauer's user avatar
  • 29.1k
14 votes
Accepted

Applications of algebraic geometry in type theory/programming language theory

To my knowledge (which is definitely incomplete), there has been relatively little work on this, presumably because it requires assimilating two relatively intricate bodies of knowledge. However, ...
Neel Krishnaswami's 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 ...
Gilles 'SO- stop being evil''s user avatar
14 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 ...
Jasper Hugunin's user avatar
14 votes

Why is the Curry-Howard isomorphism?

I suspect someone is going to come along with a deep category-theoretic reason for the connection, but in the meantime, here is my insight. Both logic and programming with functions are built around ...
Joey Eremondi's user avatar
14 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, ...
Joey Eremondi's user avatar
14 votes

Where is the model theory in programming language theory?

Let me amend Damiano's answer with more specific comments. Terms of type bool are not logical statements. Expressions like ...
Andrej Bauer's user avatar
  • 29.1k
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 ...
cody's user avatar
  • 13.9k
13 votes
Accepted

Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?

Yes, LEM implies K. See HoTT book Theorem 7.2.5, known as Hedberg's theorem, which shows that any type with decidable equality satisfies axiom $K$. If we assume excluded middle, all types have ...
Andrej Bauer's user avatar
  • 29.1k
13 votes
Accepted

Where is the model theory in programming language theory?

The model theory of programming languages is called denotational semantics. You can google the term to find out more about it, I'll give an extreme synthesis of it. Denotational semantics is a ...
Damiano Mazza's user avatar
12 votes
Accepted

What kind of theoretical object corresponds to a C++ concept?

From a programming language theory perspective, as opposed to the computability perspective other answers and comments have offered, C++ templates combined with concepts correspond to bounded ...
Dave Clarke's user avatar
  • 16.7k
12 votes
Accepted

What is the intuition behind linear logic?

I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an answer somebody might have given had the question been posted on cs.stackexchange. In ...
Martin Berger's user avatar
11 votes

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

Type theory is a mathematical theory in which we can do very many different things (set theory is like that as well). We can use type theory for computability, or homotopy theory, or use it to express ...
Andrej Bauer's user avatar
  • 29.1k
11 votes
Accepted

Can Elementary Affine Logic be used as the core type system of a practical programming language?

Something very similar, but using light affine logic (LAL) instead of EAL, was attempted a few years ago by Baillot, Gaboardi and Mogbil (you may find the paper here). I think their work may be ...
Damiano Mazza's user avatar
11 votes

Proof that the calculus of constructions extended with recursive types isn't strongly normalizing?

With general recursive types you can define the type type T = T -> T With that type you can type self-application -- and in fact, every term of the untyped ...
Andreas Rossberg's user avatar
11 votes

Philosophy behind monotonicity requirement for inductive types

When you write an inductive, you are defining a type by an equation. For example, if we write $F_1(X)=X^X=X\to X$, bad should satisfy $F_1($...
xavierm02's user avatar
  • 556
11 votes
Accepted

How do continuations represent negations (under the Curry–Howard correspondence)?

When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type ...
Dan Doel's user avatar
  • 1,021
11 votes

Applications of Barendregt–Geuvers–Klop conjecture

I'm not (exactly) an expert, but my understanding is that there are very few practical applications of this conjecture, except possibly simplifying the decision procedure for type-checking in ...
cody's user avatar
  • 13.9k
11 votes

$\eta$-reduction not locally confluent on well-typed terms

Yes, $\eta$ reduction for unit is terribly behaved. Suppose you are in a context $\Gamma \triangleq x:1, y:1$. Then, the unit term $\Gamma \vdash \left\langle\right\rangle : 1$ has the following eta-...
Neel Krishnaswami's user avatar
11 votes
Accepted

Stronger "induction" principles than induction-recursion

Anton Setzer has work on type theories that are stronger than standard induction-recursion. In some ways, though, it's still in terms of simultaneous inductive and recursive definitions. The ...
Dan Doel's user avatar
  • 1,021

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