Skip to main content

# Questions tagged [dependent-type]

Use this tag for questions about dependent types, which are families of types which vary over elements of another type.

56 questions
Filter by
Sorted by
Tagged with
2 votes
3 answers
266 views

### Uniqueness of proofs for inductively defined predicates

In Init/Peano.v the less-than-or-equal predicate is defined as follows: ...
1 vote
1 answer
105 views

### Trying to use 'Equations'

Examples from Chlipala's book https://mattam82.github.io/Coq-Equations/examples/Examples.MoreDep.html ...
1 vote
2 answers
75 views

### Dependent equality in Coq

Let’s say that cat is the type of categories (I don’t think its precise formalization really matters here). I define the type of « initial structures » of a ...
• 271
1 vote
1 answer
123 views

### Problems with dependent sums

Very simple trees (I trew away everything unnecessary) ...
7 votes
2 answers
543 views

### Why do some people disagree about whether DTT implies not Turing complete?

The idea that being dependently typed as in Agda, Coq, etc., implies not being Turing complete, sometimes crops up (see below for a brief list, though which may be out of date), including on various ...
3 votes
1 answer
166 views

### Error Abstracting over the term leads to a term which is ill-typed when doing a destruct

I'm trying to make a version of nth that cannot fail because it knows that the index is inbounds. So far, so good: ...
• 179
4 votes
1 answer
424 views

### Does "unique mere existence" imply "existence"?

Hopefully this question fits in well here. I'm hoping that more people who know the answer will see it here than on somwehere like mse, but please let me know if you'd rather I move it there! Say you'...
4 votes
2 answers
676 views

### In a dependently typed language, are all types statements?

In dependently typed languages such as Agda, Lean, Coq, Idris (and Pie), a mathematical or logical statement can be expressed as a type, and then proven by writing a program that creates an instance ...
• 141
2 votes
2 answers
162 views

### How exactly solved metas "revisited" in an efficient dependent type checker?

Suppose, for example, we want to type-check the following term: ...
• 123
6 votes
1 answer
535 views

### What are the principal differences between Agda's core type theory and Coq's?

Agda is said to be based on Luo's unifying theory of dependent types while Coq is based on the Calculus of Inductive Constructions. Both of these as I understand it extend the impredicative ...
3 votes
1 answer
150 views

### What are deductive systems associated with raw type theories?

In the answer to a previous question I have been recommended to read this paper by Philipp Haselwarter and Andrej Bauer. In this paper a class of dependent type theories is formally defined. We are ...
• 271
0 votes
1 answer
41 views

### Is type constraint the same as implication in type space?

In reading idris code, I sometimes wondered what's the mysterious type constraint =>. It's said that dependent types are a first-class member of Idris. So can be ...
• 2,320
1 vote
0 answers
32 views

### How to Show a Term in TinyIdris?

I am trying to follow the code of TinyIdris and print out the basic definitions such as Terms. But I couldn't apply the Show ...
• 2,320
3 votes
1 answer
89 views

### How to read/understand the definition of the environment in type-checking?

I am trying to read the code for TinyIdris, but couldn't understand one of the first definitions about environments below (because of my lack of understanding about type-checking and/or dependent ...
• 2,320
5 votes
2 answers
229 views

### What is a context mapping in dependent type checking?

I am reading a dissertation about dependent type programming language (Norell, 2007), and had much trouble understanding the definition of context mappings/substitutions as shown in the figure below . ...
• 2,320
3 votes
1 answer
278 views

### What is a pattern in dependent pattern matching?

I am trying to understand dependent pattern matching while reading Goguen, McBride, and McKinna (2006)'s paper, but couldn't quite grasp the concept. I know regular pattern matching in functional ...
• 2,320
1 vote
1 answer
86 views

### Use proof irrelevance in cast

I'm working using cast in Coq.Vectors. When trying to rewrite with proofs, I'd like to use the fact of proof irrelevance (Coq.Logic.Eqdep_dec), preferably automatically. I.e., when I have a lemma ...
• 23
1 vote
0 answers
62 views

### Embedding proof assistance in an application

Context Perhaps this is too open-ended a question for StackExchange, in which case I apologize, but otherwise here goes: I have a project I'm toying around with, the core of which is what I'd call &...
2 votes
1 answer
158 views

### Eliminating dependent destruction in Coq

I'm working on developing a theory of arithmetic within a framework for first-order logic I constructed in Coq. The following is a simplified version of the scenario I'm working with. ...
2 votes
1 answer
145 views

### Provable fun-extand "rewriting under binders" in intensional MLTT

I've noticed that the underlying judgemental machinery of intensional MLTT can be extended such that function extensionality becomes provable. Or in other words it becomes possible to "rewrite ...
• 345
1 vote
1 answer
110 views

### Type of Sets with an Assocaitive Operation in Lean

This is probably a really simple question, but I am no able to find something in the Lean reference manual. I want to define a type of sets equipped with an associative operation. I have tried the ...
• 722
2 votes
2 answers
145 views

### What if identity type in extensional type theory were possibly non-deterministic?

In extensional type theory, identity types are lifted to the definitional equality mechanism, this lead to a bunch of problems, and I imagine that's why they are not very popular. My question is if we ...
• 125
3 votes
1 answer
113 views

### Tricks for proving equalities under type cast

I sometimes stumble across proofs that prove equalities in the form of forall a b (p: a = b), C a = match p with | eq_refl => C b end without resorting to ...
• 171
4 votes
1 answer
181 views

### Co-induction principle

It's known that Nat-ind = Nat-rec ⨯ Nat-initiality Has someone figured out how to define a suitable Conat-coind such that ...
• 345
4 votes
3 answers
499 views

### Rewrite with definitional equality and dependent types

In Coq, there are some terms that are equal by definition, but there's not an easy way to replace one value with the other inside a proof. The two ways that I know that work in general are to use the ...
• 193
3 votes
2 answers
251 views

• 319
31 votes
2 answers
4k views

### Has anyone ever accidentally "proven" a false theorem with type-in-type?

It is possible (with some cleverness) to prove false from type-in-type. For instance, Girard proved false in Martin Lof's original system (as described in the introduction of An Intuitionistic Theory ...
• 443
6 votes
0 answers
137 views

### How to write heavily indexed proofs?

I've been playing with hereditary substitution. However, things get very awkward because substitution isn't total unless you index by the environment somehow. In my old approach terms were not indexed ...
18 votes
2 answers
580 views

### What are the motivations for different variants of categorical models of dependent type?

I am new to the categorical semantics for dependent type theories, so it is surprising for me to see nLab introduces so many variants of categorical models, including comprehension categories, display ...
• 429
12 votes
1 answer
424 views

### Easy ways to introduce inductive types

I'm working up from elaboration zoo and noticed that you don't use fixed point if you've got type level computation. It causes unification/equality check to hang up. Now, this means that I need ...
• 731
6 votes
1 answer
136 views

### How to elaborate with dependent records present?

Dependent records can be implemented in various ways, but some papers suggests I could do it in the following way: The construction of dependent record type is made by selecting labels and types. The ...
• 731
15 votes
2 answers
401 views

### Are Logics Based on Dependent Types Stronger Than Ones Without?

There have been several times during I came across statements like Isabelle/HOL's logic is not rich enough to formalize X on various places online and in during personal discussions. Or similar ...
• 1,128
9 votes
2 answers
412 views

### What's the relationship between refinement types and dependent types?

In the F* proof assistant, they use refinement types together with dependent types. Based on my impression of F*, it seems to me that refinement types are just predicates in dependent type theory that ...
• 6,346
5 votes
1 answer
180 views

### How to implement first-order relational structures in Coq?

I'm trying to define a first-order relational structure in Coq. I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough. I also have a ...
• 3,105
16 votes
2 answers
417 views

### What are the upsides and downsides of typed vs untyped conversion?

What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"? Background Generally speaking, in dependent type ...
• 394