# Tag Info

38

$\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{... 22$\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 ... 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$...

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

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

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

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 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$... 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. 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 ... 12 It turns out that$W$types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types you want, with the expected computation rules, and even canonicity. This is a very recent result of mine, you can read a preprint at Why not W?, which has been accepted for publication in the TYPES 2020 post-proceedings. The idea ... 11 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. 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 ... 11 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 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 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 ... 10 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 ... 10 The most general form of substitution theorems speaks about arbitrary contexts: Define what it means to have a substitution$\sigma : \Gamma \to \Delta$from a context$\Gamma$to a context$\Delta$(it's a simultaneous substitution giving a term$\Gamma \vdash e : A$for every$y : A$appearing in$\Delta$, and in case of type dependencies we have to do it ... 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 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 ... 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 In Agda this is done by tagging types as "irrelevant". It's a kind of quotenting. A function from an irrelevant to a (relevant) type must be constant (and Agda enforces this). You can read more about it on the Agda wiki Irrelevance page. 8 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 ... 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 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

The property, which I would call "typing of substitution" should hold in any type theory, and is not dependent on the exchange property (which I assume is what you mean by permutation) The key is that you need to generalize the inductive hypothesis to when the variable in t appears in a context. So for a dependent type theory you prove If $\Gamma \vdash ... 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 ...

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