40
A type $C$ has a logarithm to base $X$ of $P$ exactly when $C \cong P\to X$. That is, $C$ can be seen as a container of $X$ elements in positions given by $P$. Indeed, it's a matter of asking to what power $P$ we must raise $X$ to obtain $C$.
It makes sense to work with $\mathop{log}F$ where $F$ is a functor, whenever the logarithm exists, meaning $\mathop{...
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
One is internal and the other is external.
A category $\mathcal{C}$ consists of objects and morphisms. When we write $f : A \to B$ we mean that $f$ is a morphism from object $A$ to object $B$. We may collect all morphisms from $A$ to $B$ into a set of morphisms $\mathrm{Hom}_{\mathcal{C}}(A,B)$, called the "hom-set". This set is not an object of $\mathcal{C}...
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.
26
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 ...
21
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 ...
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 ...
18
LCF is indeed the grand-father of all these system: Coq, Isabelle, HOLs, including the ML programming language (which we see today as OCaml, SML, also F#). Yes, I am including Coq as a member of the greater LCF family. Compared to the US-American proof assistants (notably ACL2), or the totally unrelated Mizar, Coq is culturally quite close to Isabelle and ...
18
Semantically, a coercion $c : A \leq B$ is just a morphism $c : A \to B$, which gets added to the interpretation of terms at the appropriate points. The basic problem this creates is the issue of coherence: are you guaranteed that a term will have a unique meaning, given that the same term can potentially have coercions hidden in many possible places in the ...
18
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 ...
18
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 ...
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 ...
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
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 ...
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
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 \...
13
Here's a slightly different perspective on Fredrik's answer. It's generally the case that impredicative Church encodings of types will satisfy the relevant $\beta$ laws, but will not satisfy the $\eta$ laws.
So this means we can define a dependent pair as follows:
$$
\exists x:X.\;Y[x] \triangleq \forall \alpha:\ast.\; (\Pi x:X.\;Y[x] \to \alpha) \to \...
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
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
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 : ...
Only top voted, non community-wiki answers of a minimum length are eligible
