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
2
votes
3
answers
247
views
Uniqueness of proofs for inductively defined predicates
In Init/Peano.v the less-than-or-equal predicate is defined as follows:
...
- 127
1
vote
1
answer
98
views
Trying to use 'Equations'
Examples from Chlipala's book
https://mattam82.github.io/Coq-Equations/examples/Examples.MoreDep.html
...
- 127
1
vote
2
answers
70
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 ...
- 249
1
vote
1
answer
118
views
6
votes
2
answers
436
views
Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?
I myself have fallen prey to this misconception, i.e., that being dependently typed as in Agda, Coq, etc., implies not being Turing complete, which can be (whether now or previously) found at quite a ...
3
votes
1
answer
155
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:
...
- 167
4
votes
1
answer
420
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'...
- 329
4
votes
2
answers
665
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
156
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
430
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
149
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 ...
- 249
0
votes
1
answer
40
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,220
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,220
3
votes
1
answer
84
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,220
5
votes
2
answers
226
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,220