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
266
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
105
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
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
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'...
- 329
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 &...
- 111
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.
...
- 195
2
votes
1
answer
145
views
Provable `fun-ext`and "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
How to abstract over function arity in Lean and Coq?
Given types $A, B$ I would like to express the type of all functions $f$ for which there exists an $n \in ℕ$ such that $f$ has type $A^n \to B$. And possibly in such a way, that for $a_1, \dots, a_n : ...
- 224
2
votes
0
answers
64
views
Elimination rules of inductive types
Why does the elimination rule of inductive types sometimes allow the target type to depend on the inductive type and sometimes not? I am confused by that. Is it correct that it makes no difference in ...
- 722
1
vote
1
answer
130
views
Destruction of bound dependent types
I'm having an issue with dependent typing. I have reduced it to the following minimal example:
...
- 23
4
votes
1
answer
302
views
What types can be written in Kind but not Lean?
The Kind programming language has a sufficiently powerful type system to support proving theorems like in Lean, Coq, Idris, or Agda. I've seen it said that Kind has an even more powerful type system ...
- 151
0
votes
0
answers
65
views
Cardinals, universe levels, sheaves and predicativity
This question stems from some of my attempts to understand topos of coalgebras over a comonad from type-theoretic point of view.
Paraphrasing the statement I am trying to understand (proposition 2.1, ...
- 547
11
votes
1
answer
264
views
Universe inconsistency as an effect
The Internet tells me there is some work on languages that permit general recursion but carry information about possible divergence in the type system. For instance, the simply-typed language Koka ...
- 3,240
9
votes
1
answer
181
views
Interpretation of dependent types: Coherence
I have trouble understanding precisely how dependent type theories are intepreted in categories (in the most simple case, for example in a locally cartesian closed category). I know that a type in ...
- 722
3
votes
0
answers
106
views
Using crude but effective stratification & cong to implement transitivity of `=`
Suppose I have
cong : {A B : Type} (f : A -> B) (p : a = b) : f a = f b
coe : (A : I -> Type) -> A 0 -> A 1
It is ...
- 6,346
4
votes
1
answer
261
views
How can you represent a dependent type visually?
So, obviously for a term $t$ of type $T$, I would represent it as:
T
+-----------+
| |
| t |
| |
+-----------+
That is a node ...
- 303
7
votes
1
answer
463
views
Very dependent functions
A "very dependent function" is a function whose output type at input $n$ depends on its own output values at inputs $k<n$. Is there a precise definition of such things that makes sense ...
- 3,240
4
votes
2
answers
183
views
Formalization of abstract definitions
I'm asking about the abstract keyword in Agda and equivalent features in other languages. It marks a definition as non-expandable, potentially speeding up ...
- 4,087
10
votes
1
answer
433
views
Can you build W-types out of natural numbers predicatively?
I understand that we can use W-types to encode natural numbers and a wide variety of other inductive types in intensional MLTT. Can we encode W-types using only natural numbers within type theory, ...
- 547
9
votes
0
answers
318
views
Alternatives to universe levels
All of the type theory based proof assistants that I have seen have an infinite hierarchy of type universes to avoid the type of types being a term of itself. Are there alternative systems which could ...
- 91
6
votes
0
answers
87
views
What are Generic Arguments in Coq and how are they structured in their OCaml code?
I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
- 333
7
votes
1
answer
666
views
How do I convince the Lean 4 type checker that addition is commutative?
In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the ...
- 73
4
votes
1
answer
281
views
What are instances of a dependent pair type?
Currently I am learning about dependent pair ($\Sigma$-)types, and I'm having some trouble understanding how an instance of a dependent type could be formed. I think I understand how the type of a ...
- 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 ...
- 2,868
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