The dependent-type tag has no usage guidance.
6
votes
1answer
270 views
Proof techniques for showing that dependent type checking is decidable
I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and ...
7
votes
1answer
125 views
If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?
Question
If a pure type system has a terminating proof language, can we have Type : Type at the logic level without causing paradoxes (i.e., without causing ...
6
votes
1answer
154 views
Fixed points in dependent type theories
Most dependent type theories aim for some notion of correctness in two respects:
The type system must be decidable.
The type system must be consistent. e.g. $\forall \tau. \tau$ should not be ...
1
vote
2answers
158 views
What are the limitations of dependent typing?
It seems dependent types can provide lots of desirable guarantees about program behavior. What kinds of program properties can they NOT guarantee (besides what's computationally infeasible)? Is there ...
2
votes
0answers
91 views
What is the proof for the inconsistency of impredicaitivity + excluded middle + large elimination in type theory
Why is the combination of
impredicativity + excluded middle + large elimination
inconsistent in dependent type theory?
My understanding of large elimination is I am doing large elimination if I am ...
8
votes
2answers
177 views
How can you build a coinductive memoization table for recursive functions over binary trees?
The StreamMemo library for Coq illustrates how to memoize a function f : nat -> A over the natural numbers. In particular when ...
13
votes
0answers
153 views
Using Dependent Type Theory for Categories that are not LCCC
I have recently been working with polynomial functors and monads based mostly on Gambino-Kock. There they define polynomial functors in a Locally Cartesian Closed Category (LCCC) and extensively use ...
15
votes
2answers
458 views
In the Hott book, are the most of the type formers redundant? And if so, why?
In chapter 1 and Appendix A of the Hott book, several primitive type families are presented (universe types, dependent function types, dependent pair types, Coproduct types, Empty Type, Unit type, ...
4
votes
0answers
106 views
Completeness of realizability semantics for higher-order type theory
In this answer I mention a paper by Geuvers in which he describes a class of models for a type theory $\lambda P_2$ which is a sub-system of the CoC and roughly corresponds to 2nd order predicate ...
6
votes
2answers
281 views
Explicit set of types and terms in MLTT
Whenever I read a presentation of MLTT, especially in the context of the correspondence of MLTT with LCCCs (eg. Seely's paper), they say "the type constructors/formation rules are..." and then list a ...
6
votes
3answers
194 views
Proving running time upper bounds for algorithms in dependent type theory
Proof assistants are a valuable tool for verifying
the correctness of proofs of mathematical theorems.
When dealing with proofs of correctness of algorithms,
one is not only interested on showing ...
5
votes
0answers
105 views
Relationship between Pataraia's theorem and inductive-recursive definitions?
Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
3
votes
2answers
243 views
Motivation for Dependent Type
By the Curry-Howard Isomorphism we view propositions (or theorems if true/inhabited) as types.
But take the type $\mathbb{N} \implies \mathbb{N} \implies \mathbb{N} $.
We have as witnesses to this ...
6
votes
1answer
112 views
How to mechanically derive the recursor of a type from its constructors?
In Martin-Löf Dependent Type Theory a type is commonly prescribed by how to construct its canonical terms and how to show that its canonical terms are definitionally equal. This means that the ...
6
votes
1answer
197 views
Type checking, Hypothetical judgments, meaning explanations and computational type theory
We say that a system is a computational type theory if it is a type theory defined by not a bunch of inference rules, but some sort of Martin-Löfian meaning explanations (e.g. in the sense of NuPRL). ...
4
votes
1answer
237 views
Is it possible to verify a typechecker for a total dependently-typed language in that language's logic?
I understand the diagonalization argument against implementing an eval function in a total language, and that typechecking in a dependently typed language requires ...
1
vote
1answer
129 views
What's the effect of imposing the following restriction on inductive type families?
Let a simple expression be either:
A free variable
A data constructor of an inductive type family, applied to 0 or more simple expressions
What would be the effect of imposing the following ...
4
votes
1answer
121 views
What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?
In the context of constructive type theory, a term inhabiting some type is said to be in canonical form if it is explicitly built up using the constructors of that type.
Particularly, the only ...
8
votes
1answer
1k views
Dependent Types and Compile Time Types
I am trying to grok dependent types, and there's something that I find unclear.
In C++, templates can have non-type (template) parameters. The values of these parameters have to be specified at ...
6
votes
1answer
268 views
Examples of Universe inconsistency in normal use of dependent types
In dependent types, Type : Type results in inconsistency (Girard's or Hurken's paradox).
Are there examples of universe inconsistency (where assuming ...
9
votes
1answer
352 views
PiSigma: why does 'unfold' bind a variable?
I'm trying to understand the paper ΠΣ: Dependent Types without the Sugar by implementing an interpreter and type checker for the language. In doing so, I've seen that the ...
7
votes
1answer
163 views
Is there a theory of overloading types?
There is a sound theory of overloading operators and functions realized by type classes in Haskell, and to rougher extent by traits in Rust, etc.
In mathematics however, there are many situations ...
11
votes
1answer
297 views
Dependent types over Church-encoded type in PTS/CoC
I'm experimenting with pure type systems in Barendregt's lambda cube, specifically with the most powerfull one, the Calculus of Constructions. This system has sorts ...
13
votes
3answers
543 views
What are the negative consequences of extending CIC with axioms?
Is it true that adding axioms to the CIC might have negative influences in the computational content of definitions and theorems? I understand that, in the theory's normal behavior, any closed term ...
13
votes
2answers
292 views
Church-Rosser property for dependently typed lambda calculus?
It is well-known that the Church-Rosser property holds for $\beta \eta$-reduction in simply-typed lambda calculus. This implies that the calculus is consistent, in the sense that not all equations ...
4
votes
1answer
109 views
Rendering of type-level computation
Programming languages with dependent types and/or higher-kinded types feature what might be called compile-time computation at the type-level. This is usually defined as follows (I'm omitting some ...
16
votes
1answer
766 views
Why it's impossible to declare an induction principle for Church numerals
Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way:
...
10
votes
1answer
240 views
Reference for the fact that (0=1) implies false requires a universe in MLTT
It's a fairly well-known fact that deriving a contradiction from a disequality (for example, $(0=1) \to \bot$) in Martin-Loef type theory requires a universe.
The proof is also fairly ...
9
votes
1answer
118 views
Relating univalence for a theory of cateogries to the skeleton concept
Say I work in homotopy type theory and my sole objects of study are conventional categories.
Equivalences here are given by functors $F:{\bf D}\longrightarrow{\bf C}$ and $G:{\bf C}\longrightarrow{\...
2
votes
1answer
295 views
Dependent Sums and Products
I'm trying to understand the connections between a few different concepts fundamental to dependent type theory.
Dependent functions ($\Pi$-types)
Including non-dependent functions ($A \rightarrow B$)...
2
votes
2answers
181 views
How to translate the axiom schema of induction by Curry-Howard?
I'm trying to understand the Curry-Howard correspondence. I am comfortable with it for propositional logic, but get confused when $\forall, \exists$ quantifiers come in the picture.
The axiom schema ...
17
votes
2answers
536 views
Why an infinite type hierarchy?
Coq, Agda, and Idris have an infinite type hierarchy (Type 1 : Type 2 : Type 3 : ...). But why not do it instead like λC, the system in the lambda cube that's closest to the calculus of constructions, ...
4
votes
1answer
291 views
Rules about Prop and Set in UTT
In Luo's UTT (type theory which is used in Agda, Idris, and other dependently typed programming languages), there're are two rules for $\Pi$ types. One for $\mathsf{Prop}$ and one for $\mathsf{Set}$. ...
5
votes
1answer
222 views
What does consistency mean for “computational theories” corresponding to inductive types?
I am currently reading the book by Luo on computation and reasoning. In the book he contrasts inductive types considered as computational theories with axiomatic theories widespread in "standard" ...
5
votes
2answers
375 views
“Correctness” of type theory
How to "proof" that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one?
When type ...
9
votes
1answer
211 views
Example of where violation of strict positivity condition in inductive types leads to inconsistency
Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?
31
votes
3answers
3k views
Why does Coq have Prop?
Coq has a type Prop of proof irrelevant propositions which are discarded during extraction. What are the reason for having this if we use Coq only for proofs. Prop is impredicative, so Prop : Prop, ...
3
votes
2answers
342 views
Good description of Calculus of Inductive Construction
I want to learn more about Calculus of Inductive Constructions. What can you recommend to read on this topic? All the materials which I found are either in French or too basic (the Coq'Art book).
The ...
3
votes
2answers
147 views
How to use Prop from UTT in Agda
In Ulf Norell's thesis he mentions that Agda is based on Luo's UTT. However, I can't find a way to use Prop there. Is there any way to do so?
4
votes
2answers
137 views
Well-formedness condition for inductive types
I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. ...
10
votes
2answers
596 views
Formalizing the theory of finite sets in type theory
Most proof assistants have a formalization of the concept of "finite set". These formalizations, however, differ wildly (although one hopes that they are all essentially equivalent!). What I don't ...
7
votes
2answers
1k views
Is compiler for dependent type much harder than an intepreter?
I have been learning something about implementing dependent types, like this tutorial, but most of them is implementing interpreters. My question is, it seems that implementing a compiler for ...
4
votes
2answers
182 views
dependent types and higher-order logic applied in the realm of DSLs
(this is a beginner question and English is not my first language)
I am searching for references on using theorem proves based on dependent type theory (or Martin Löf type-theory) and higher-order ...
7
votes
1answer
720 views
Constraint types (IBM/X10) compared to dependent types
Constraint types have been proposed by IBM in their X10 programming language (it's a commercial programming language, not open source software).
Nystrom, Nathaniel, et al. "Constrained types for ...
14
votes
1answer
306 views
How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?
For systems without dependent types, like Hindley-Milner type system, the types correspond to formulas of intuitionistic logic. There we know that its models are Heyting algebras, and in particular, ...
15
votes
1answer
338 views
Parametricity and projective eliminations for dependent records
It's well-known that in System F, you can encode binary products with the type
$$
A \times B \triangleq \forall\alpha.\; (A \to B \to \alpha) \to \alpha
$$
You can then define projection functions $\...
19
votes
2answers
2k views
What's the difference between ADTs, GADTs, and inductive types?
Might anyone be able to explain the difference between:
Algebraic Datatypes (which I am fairly familiar with)
Generalized Algebraic Datatypes (what makes them generalized?)
Inductive Types (e.g. Coq)
...
12
votes
3answers
683 views
Modeling objects (OOP) in dependent type theory
I am interested in modeling objects, from object oriented programming, in dependent type theory. As a possible application, I would like to have a model where I can describe different features of ...
9
votes
1answer
415 views
What is the role of the Bicolored Calculus of Constructions?
So, I'm reading a bit about elaboration, particularly, algorithms based on the Bicolored Calculus of Construction, and I'm a bit confused. I don't understand what exactly the purpose of the $CC^{bi}$ ...
7
votes
1answer
310 views
Implications of the rule of cumulativity in the Calculus of Constructions
Please help me understand some type theory research.
As suggested in "Type Checking with Universes" by Robert Harper and Robert Pollack, we can add the following rule to our otherwise standard COC or ...
