36

$\mathtt{Prop}$ is very useful for program extraction because it allows us to delete parts of code that are useless. For example, to extract a sorting algorithm we would prove the statement "for every list $\ell$ there is a list $k$ such that $k$ is ordered and $k$ is a permutatiom of $\ell$". If we write this down in Coq and extract without using $\mathtt{...


20

$\mathrm{Prop}$ is impredicative, which create a very expressive proof system. However it is "too" expressive in the following sense: $$ \mathrm{impredicative\ Prop} + \mathrm{large\ elimination} + \mathrm{excluded\ middle} $$ is inconsistent. Usually you want to keep the possibility to add the excluded middle, so one solution is to keep large elimination ...


20

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 $...


19

Actually, the approach of the CoC is more expressive -- it permits arbitrary impredicative quantification. For example, the type $\forall a.\; a \to a$ can be instantiated with itself to get $(\forall a.\; a \to a) \to (\forall a.\; a \to a)$, which is not possible with a universe hierarchy. The reason it is not widely used is because impredicative ...


15

A language can be thought of as having both a static semantics, which determines the compile-time analysis that occurs; and a dynamic semantics, which determines the execution-time behavior of programs. In Standard ML, for example, the static semantics concerns a language of Modules and a language of Types. The semantics show how types are assigned to terms ...


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

Even if you are not interested in extracting programs, the fact that Prop is impredicative allows you to build some models which you can't build using a predicative tower of universes. IIRC Thorsten Altenkirch has a model of System F using Coq's impredicativity.


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

That a formula is not provable can essentially be done in two ways. With some luck we might be able to show within type theory that the formula implies one which is already known to be not provable. The other way is to find a model in which the formula is invalid, and this can be quite hard. For example, it took a very long time to find the groupoid model of ...


13

This is an interesting question! As Anthony's answer suggests, one can use the usual approaches to compiling a non-dependent functional language, provided you already have an interpreter to evaluate terms for type-checking. This is the approach taken by Edwin Brady. Now this is conceptually simpler, but it does lose the speed advantages of compilation when ...


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$...


11

I refer you to Chapter 9 of the HoTT book. In particular, a category is defined in such a way that isomorphic objects are equal, see Definition 9.1.6. As Example 9.1.15 points out, there really isn't a reasonable notion of "skeletality" in HoTT. This is so because equality is so weak that it already means "isomorphic". Furthermore, Theorem 9.4.16 says ...


10

Edwin Brady's PhD thesis outlines how to construct a compiler for a dependently typed programming language. I'm not an expert, but I'd say it's not extremely harder than implementing a System F-like compiler. Many of the principles are quite similar and some are the same (e.g. supercombinator compilation.) The thesis covers many other concerns.


10

As they explain in the related work section of the 2008 paper, the constraint types they describe are most closely related to refinement types. I wont give references, as there are plenty in the bibliography of the aforementioned paper, but I can give a quick overview. Refinement types are a language that allow the expression of refinements of the values of ...


10

I know of: Jan M. Smith, The independence of Peano's fourth axiom from Martin-Löf's type theory without universes, The Journal of Symbolic Logic 53(3), p. 840-845, 1988.


10

Type theories have multiple uses, and with each kind of usage comes a different notion of correctness. They two key uses are As a foundation of mathematics. In this context correctness means primarily that we can't deduce falisity. As a tool in programming. Here correctness means primarily that that well-typed programs "don't go wrong" in Milner's famous ...


10

It is actually possible to relax strict positivity and remain consistent. For instance, it suffices to only have a positivity condition. That is, we can accept type definitions like $$ T \triangleq \mu\alpha. (\alpha \to 2) \to 2 $$ where recursive type variables occur to the left of an even number of arrows and retain consistency. However, theories ...


9

I'll compliment Neel's (excellent, as usual) answer with a bit more exposition on why levels are used in practice. The first important limitation of CoC is that it is trivial! A surprising observation is that there is no type for which you can prove that it has more than one element, much less an infinite number of them. Adding just 2 universes gives you ...


9

You can't do this using the traditional Church encoding for Bool: #Bool = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool ... because you can't write a (useful) function of type: #Bool → * The reason why, as you noted, is that you can't pass in * as the first argument to #Bool, which in turn means that the True and False arguments may not be types. ...


9

There is indeed a subtlety here, though things work out nicely in the case of type checking. I'll write down the issue here, since it seems to come up in many related threads, and try to explain why things work out all right when type-checking in a "standard" dependent type theory (I'll be deliberately vague, since these issues tend to crop up ...


8

I know it can be done 'elegantly' in a dependently typed system. But, from a classical point of view, the resulting definitions seem extremely alien. Can you explain what you mean by "alien"? It seems to me that you formalize the concept of finite set in precisely the same way in type theory and in set theory. In set theory, you proceed by defining the ...


8

Quite a bit is know about this. The concept of Pure Type Systems (PTS) is useful for showing Church-Rosser (CR) for large classes of typed $\lambda$-calculi. Paraphrasing (1): PTS with only β reduction satisfy CR on typed terms. This follows immediately from CR on 'pseudoterms', together with subject reduction. For PTS with βη-reduction, CR on the set of ...


8

It might be useful to quickly give the counter-example to CR in typed calculi with $\beta$ and $\eta$: $$ t=\lambda x:A.(\lambda y:B.\ y)\ x$$ And we have $$ t\rightarrow_\beta \lambda x: A.x$$ and $$ t\rightarrow_\eta \lambda y:B.y$$ It is immediate that if $A\equiv B$, then the two resulting terms are, in fact, $\alpha$ equivalent, but there is no ...


8

This is a hard question to answer, in part because it's unclear what it means to get something "by accident". Regularly, though, people run into the Universe Inconsistency error of Coq, as some quick googling will show (e.g. here). This certainly sometimes happens by accident, sometimes in the attempt at showing inconsistencies or testing the limits of the ...


8

Actually, the motivation for introducing dependent types goes in the opposite direction! Curry had noticed that there was a direct correspondence between typed terms in the $SK$ calculus and proofs in (minimal implicational) propositional logic, but there was no programing language known to correspond in such a way to predicate logic. Indeed, introducing $\...


8

The 'logic' of the contradiction with Type:Type is that you can create a term of any type including 'empty' type by 'cheating' by never returning. This is essentially the only way to cheat because of subject reduction and the subformula properties. Subject reduction states that evaluation of terms preserves their type. If you have subject reduction and ...


8

It sounds like you want an overview of normalization arguments for type systems with positive datatypes. I'd recommend Nax Mendler's PhD dissertation: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html. As the date suggests, this is pretty classic work. The basic intuition is that an ordinal $\lambda$ can be associated to any element of a ...


7

Say that a universe $U$ is impredicative if the product $\prod_{x : A} B(x)$ is in $U$ whenever $B(x)$ is in $U$ for all $x$, and $A$ is arbitrary, i.e., not necessarily in $U$. Are there any impredicative universes? Let us think about what an impredicative universe would be for sets: a set $U$ such that for every family of sets $B : A \to U$, no matter how ...


7

One first reason to reject axioms is that they might be inconsistent. Even for the axioms that are proved consistent, some of them have a computational interpretation (we know how to extend definitional equality with a reduction principle for them) and some do not -- those break canonicity. This is "bad" for different reasons: In theory, canonicity lets you ...


7

As usual, (a) the high-level conceptual approach is basically the same as it is on paper, but (b) mechanization makes new things reasonable to attempt. The way you do things is to define a cost semantics for a programming language, where you assign a cost for each of the operations in the language. Next, you define a machine model, with its own cost ...


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