39
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 should note that historically type theory was written using $\in$. Martin-Löf's conception of type was meant to capture sets constructively, and already Russell ...
34
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 Functional Programming and Girard's Proofs and Types.
27
Here are a few things to keep in mind:
Although we generally think we know what we mean by set-theoretic intersection and union, there have been several different takes on what exactly intersection and union types are. So, it's worth pinning this down before you embark on an implementation.
One element which I think is awfully important for understanding ...
24
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 have to forgive me (and correct me!). The basic story is that Curry had uncovered the basic correspondence between simply-typed combinators (or $\lambda$-terms) ...
24
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 propositional to first-order logic. The key contribution of Martin-Löf's is a novel analysis of equality.
There are two main ways of giving Curry-Howard style ...
22
Well, relational parametricity is one of the most important ideas introduces by John Reynolds, so it shouldn't be too much of a surprise that it looks like magic. Here is a fairy tale about how he might have invented it.
Suppose you're trying to formalize the idea that certain functions (identity, map, fold, reversal of lists) act "the same way on many ...
22
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 : \mathsf{Type} \to \mathsf{Type}$, we might be interested in the "minimal" type $A$ satisfying $A \cong T(A)$. In terms of category theory $T$ is a functor and $...
21
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 logic.
The proof generally proceeds by assuming you have a term $\mathrm{absurd}$ of type $\mathrm{False}$, using subject reduction to get a normal form, and ...
21
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, in their 1991 PLDI paper, Refinement Types for ML.
Rowan Davies studied type inference for refinement types in his PhD thesis, Practical Refinement Type ...
20
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 are asking whether there can be uncountably many terms of a given type. The answer is: obviously not since there are only countably many finite strings, and ...
20
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 of $\mathrm{PA}$.
Secondly, and this is really surprising, $\mathrm{PA}$ can actually prove consistency of both those systems! This is done using the so-called ...
19
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 mathematician.
To a constructive mathematician call/cc looks like cheating. Consider how we witness $p \lor \lnot p$ using call/cc:
We provide a function $f$ which ...
19
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 talks about Martin-Löf Type Theory and, perhaps more surprisingly, when one talks about CIC. For example, taking the version of CIC defined in Benjamin Werner's thesis, it doesn't even make sense ...
17
The way I understand the difference is that the two concepts are used to give slightly different emphasis, but ultimately they are kind of the same thing. Since neither has a formal definition we cannot expect an exact answer without first limiting the scope to a particular understanding of "type" and "sort".
"Sort" is used when we want to say that there ...
16
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 purpose programming language has general recursion. This allows it to populate every type, but we would not conclude from this fact that programming is a ...
16
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 reasons.
First, MLTT is predicative. There is a universe hierarchy, and each type lives at a particular universe level, and a type at level $n$ can only quantify ...
15
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 to give up the axiom in the sense of "personally agree, at a basic philosophical level, that it doesn't hold", you just have to think of it in terms like: "As a ...
15
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 mean one of two things:
A single type $E$ which is empty with respect to all types. Such a type has the elimination rule: for every $n$ and type family $A : E \...
14
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 example makes it easier to follow:
((\x.x) (\y.y)) 10
For maximum clarity, let's start by assigning type variables to each sub expression:
x : A
(\x.x) : B
y : C
...
14
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 bad idea to do everything in a minimalist way. For example, we introduce $\mathbb{N}$ separately because it is instructional to see how inductive constructions ...
14
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 types as a ($n$-ary) relation $R \subseteq \cal A^n$.
This works perfectly fine for all kinds of type theories, including dependently typed theories, see e.g. ...
14
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 it and learn about it. The fact that your theory is intuitionistic doesn't mean that your meta-theory has to be! You may freely use proof by contradiction or ...
13
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 of machines in which all programs/computations terminate by no means implies that function equality (i.e., whether two programs/machines compute the same ...
13
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 realize this, you will see that we can obtain $A \times B$ as both a $\sum$ and a $\prod$:
Take $P : \mathtt{bool} \to \mathsf{Type}$ where $P(\mathtt{false}) = A$...
13
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. The second means that the type $\bot$ is not inhabited. CR implies the first kind of consistency, not the second. This, as has been pointed out in the ...
13
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 possibly non-terminating programs.
I won't make a complete survey here, but I'll try and give pointers to the main thrusts of different directions.
The "...
13
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 $\mu$ at the universe of all types. Given a system of mutually recursive equations
\begin{align*}
A &= F(A, B)\\
B &= G(A, B)
\end{align*}
where $F, G : ...
13
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 approach to the foundation of mathematics. Bertrand Russel discovered a paradox in naive set theory, and he worked on type theory as a way to limit the expressive ...
answered May 25 '19 at 20:23
Gilles 'SO- stop being evil'
2,6071 gold badge24 silver badges35 bronze badges
13
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 community, so much was said about "decidability of degeneracies" that we began to give the impression that this was the hard part of the algorithm (since as ...
12
The issue seems to be confusion resulting from a confluence of two factors:
I was using a stale version of Agda (2.3.0.1). It appears that prior to 2.3.2, Agda simply wasn't checking strict positivity of the indices of constructor results (see the bug I linked elsewhere in the thread).
A closer reading of Dybjer's Inductive Families paper suggests that he ...
Only top voted, non community-wiki answers of a minimum length are eligible
