Questions tagged [dependent-type]
An overlapping feature of type theory and type systems.
129
questions
-1
votes
1
answer
83
views
Notation problem
The following problem arises when I try to define a new notation. I have a function
f : A -> A -> A -> A -> Type
Then I want special notation for the ...
3
votes
0
answers
55
views
What are some practical applications of inductive-inductive types?
By "practical applications" I mean in usual programming/industry. I am particularly interested in cases where the inductive-inductive types cannot be easily replaced by inductive-recursive ...
- 131
1
vote
1
answer
76
views
Can I define nested mutually dependent types in Coq?
I am trying to model the following in Coq, which works fine in Haskell (below is Haskell code):
...
- 13
3
votes
1
answer
257
views
Model foreign keys as dependent types?
A database consists a list of tables. For example you have a table of Worker and a table of Project where each project needs a ...
- 347
2
votes
1
answer
118
views
Where can I find more information about "dependent elimination"?
I am trying to find more information (preferably an academic paper) for the concept of "dependent elimination". I understand the concept itself: it means constructing a type by eliminating a ...
1
vote
1
answer
81
views
Intuition behind UTT's internal logic
The "internal logic" of type theory UTT is defined in LF as follows:
What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - ...
- 125
1
vote
1
answer
115
views
Formulation of Tarski-style universes in LF
Lately I've been asking questions on type theory on MSE, and I've been getting great answers, but I decided to give a try to this site and see if it will be helpful as well.
I'm looking at this note ...
- 125
5
votes
1
answer
278
views
Dependent type theory and definitions of cumulativity
Many dependent type theories employ an universe hierarchy to compensate for the fact that Type : Type is inconsistent (due to Girard's paradox). A cumulativity relation is then defined to lift terms ...
- 53
2
votes
0
answers
119
views
Why Multiple Clocks in Guarded Dependent Type Theories?
The main purpose of clocks in guarded type theories (originating in Atkey & McBride ICFP 2013) is so that we can define coinductive constructions from guarded recursive definitions.
Semantically ...
- 1,653
3
votes
1
answer
374
views
Similarities and differences between Pie and popular languages with dependent types
The book The Little Typer explains dependent types using a toy language called Pie (https://github.com/the-little-typer/pie).
How similar is Pie to the popular languages with dependent types: Coq, ...
- 133
3
votes
1
answer
251
views
Dependently typed monad
I have came across something that looks like a dependently typed monad. I would like to know if something like this is studied and where can I find more information about it.
Let's have these two ...
- 161
5
votes
1
answer
311
views
How do we use directed univalence in directed type theory?
In directed type theory of Riehl and Shulman, we have a new type, $hom_A\:x\:y$ representing arrows between elements $x$, $y$ of type $A$, note that these are not a priori functions.
I will call the ...
- 900
6
votes
1
answer
194
views
Is there a way to define dependent types without explicit substitutions internally within agda?
I am playing around the Programming Language Foundations in Agda exercises and wondering if we can achieve the same level of theories with dependent types. With simple types, the definition usually ...
- 163
8
votes
0
answers
139
views
For which type systems have normalizaton proofs been formalized?
I am trying to understand what the open problems are in the area of formalizing proofs of normalization for type systems.
Obviously STLC has been done many times.
For predicative System F, I found one ...
- 181
8
votes
4
answers
468
views
Type theory and fixed points of datatypes
For the purposes of this question, say that a datatype is a type constructor with one type parameter (this is sometimes called a type operator).
In Haskell, we can define a fixed point ...
- 900
3
votes
1
answer
113
views
Implementation of vectors as dependent types in CoC
I'm trying to understand dependent types in CoC and I am having trouble finding examples that are actually carried out in CoC, specifically without inductive types or pattern matching. The most ...
- 161
4
votes
1
answer
190
views
Effect of HoTT/Univalence Axiom on equality between terms of inductive types?
It is well known that Univalence contradicts Axiom K,
for example there are two ways $\mathbf{2} = \mathbf{2}$ may be proved using Univalence, via $\mathtt{id}_{\mathbf{2}}$ or $\mathtt{not}$.
But ...
- 151
8
votes
2
answers
509
views
What's the categorical semantics of definitional equality?
The categorical semantics of a dependent type theory is normally described as a CwA/CwF/CompCat/etc. and in these models, we can talk about propositional equality by interpreting an 'identity type'. ...
- 965
6
votes
3
answers
1k
views
How does type theory change how one thinks about programming?
I have been dabbling in HoTT and I am convinced that dependent type theory is much more suitable than set theory for proof assistants.
Now, this made me wonder - how fundamental is Type Theory ...
- 169
3
votes
1
answer
188
views
Counterexample request: ill-scoped metavariable solution
This is a question on metavariable (aka holes) resolution in (dependent) type theories.
In many referential implementations (such as Andras Kovacs' elaboration-zoo), there is one step called 'scope ...
- 965
9
votes
0
answers
201
views
Constructive Strong Normalization of the Extended Calculus of Constructions
The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ...
- 375
3
votes
1
answer
206
views
5
votes
1
answer
393
views
Example use cases for induction-recursion
I know of only two uses of induction-recursion:
Encoding universes as a type, as shown in the Agda docs for recursion
Encoding Finite sets as shown in Conor Mc'Bride's "datatypes of datatypes&...
- 595
1
vote
0
answers
102
views
CubicalTT: successor of add proof?
Lecture 2 of the cubical type theory lectures provide a proof of
(suc a) + b = suc (a + b):
...
- 595
2
votes
0
answers
89
views
MLTT/MiniTT: why do normal forms of sum types carry environments?
I am learning how to implement MiniTT: a simple type theoretic language, which is a dependently typed language with sum types, mutual recursive/inductive definitions and a universe of small types.
A ...
- 595
6
votes
1
answer
248
views
What are the pros and cons for type cases in dependent type theories?
Pattern matching on $\cal U$ is allowed in XTT and Idris2 (for unerased types), and that implies the injectivity of type constructors (that's just my intuition, though -- I also wonder how do I prove ...
- 965
4
votes
1
answer
112
views
NBE for MiniTT: Why is labelled sum eliminator both a normal form and a neutral value?
I am studying A simple type-theoretic language: MiniTT, which introduces a dependently typed language with The language contains data types, mutual recursive/inductive definitions and a universe of ...
- 595
3
votes
1
answer
174
views
References on implementing universe levels over MLTT?
I've followed the tutorial on Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen, where we implement a small dependently typed kernel with the axiom ...
- 595
3
votes
2
answers
244
views
Bidirectional typing for dependent types: Why are Sigma, Pi synthesized?
According to the Pfenning philosphy of bidirectional typing, as also explained by Dunfield and Krishnaswamy 2013, constructors should be checked, while eliminators should be synthesized. Cconvention ...
- 595
2
votes
2
answers
493
views
Does univ : univ always lead to a contradiction in a dependently typed language?
I am currently following Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen, where we consider the type of U (the universe ...
- 595
3
votes
2
answers
521
views
What technique is used to implement type checking for CoC?
I am studying David Christiansen's tutorial on implementing a dependently typed language, where it says:
Typed normalization by evaluation is far from the only way to implement conversion checking ...
- 595
0
votes
1
answer
235
views
Calculus of constructions: Why forall when pi exists?
I'm studying the calculus of constructions from ATAPL, Chapter 2. I'm trying to understand the Type Equivalence rule, which describes the meaning of the new type family ...
- 595
0
votes
2
answers
117
views
Pi-type over a list in dependent type theory
In a formalization I need to create an inductive type which has a term for each element in a list, something like this (I'll use Agda in the following, but everything here is standard dependent type ...
- 113
3
votes
0
answers
95
views
Boltzmann sampling for containers/dependent polynomials?
I’d like to randomly sample from dependently-typed data structures.
Has anyone looked at extending Boltzmann sampling to containers or dependent polynomials?
- 32.4k
3
votes
1
answer
246
views
Is just one W-type enough for formalizing mathematics?
We work in intensional Martin-Löf type theory with $0$, $1$, $2$, $\Pi$, $\Sigma$, $W$ and a cumulative hierarchy of universes. Suppose our goal is to formalize constructive mathematics.
Now if we ...
user61651
2
votes
0
answers
161
views
Set-theoretic encoding of functions in type theory
Functions usually get encoded in set theory as follows. A function $A\to B$ is a subset $f\subset A\times B$ such that $\pi_1:f\to A$ is a bijection.
In type theory to give a function $A\to B$ is to ...
user61651
2
votes
1
answer
172
views
Dependent eliminator for empty type in intensional Martin-Löf type theory
In calculus of inductive constructions you can just say that the empty type is the type with no constructors and it automatically builds the dependent eliminator.
But let's say I'm setting up ...
user61651
1
vote
2
answers
186
views
Explicit type system with infinite non-cumulative universe hierarchy
Is there an open-source proof assistant or at least an explicit set of rules written down somewhere for a type system with an infinite non-cumulative universe hierarchy and unique typing?
I want to ...
user61651
2
votes
2
answers
150
views
$\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$
Is there a way to implement natural numbers in intensional Martin-Löf type theory so that addition and multiplication is judgmentally commutative?
user61651
4
votes
1
answer
219
views
Model of MLTT with $\eta$ rule where function extensionality fails
Consider intensional Martin-Löf type theory with judgmental $\eta$ rule for dependent product types. Is there a model of it where function extensionality fails?
user61651
4
votes
0
answers
172
views
Model of homotopy type theory where propositional & judgmental equality coincide for closed terms
In intensional Martin-Löf type theory we can prove the metatheorem that two closed terms are propositionally equal iff they are judgmentally equal.
Is there a non-empty model of homotopy type theory ...
user61651
2
votes
1
answer
88
views
Normal term of double negation of W-type
Consider the intensional Martin-Löf type theory without axiom of choice or the law of excluded middle.
Let $A:U_0$ be a type and $B:A\to U_0$ be a function such that $\Sigma_{a:A}(B(a)\to 0)$is ...
user61651
6
votes
1
answer
504
views
Defining inductive types in intensional type theory purely in terms of type-theoretic data
To define a (non-indexed) W-type all we need is a type $A:U$ and a function $B:A\to U$ and we get a type $W_{a:A}B(a)$. To check that this definition is valid we only need to check that the ...
user61651
3
votes
1
answer
178
views
Defining binary natural numbers without quotient types
Let's say we work in a dependent type theory with W-types and we want to have a type for binary natural numbers. We don't want to add quotient types or higher inductive types to the system.
How to ...
user61651
6
votes
1
answer
553
views
Impredicativity + large eliminations (with no excluded middle) in Coq
It is known that impredicativity + large eliminations + excluded middle is inconsistent. Prop is impredicative and consistent with excluded middle, but does not ...
- 117
4
votes
0
answers
194
views
What logic do refinement types correspond to?
I'm interested in applicability of refinement types to theorem-proving hence the questions about their logical expressiveness. Let's say, we have a type system which corresponds to some logic ...
- 41
7
votes
1
answer
181
views
"Interesting" categories whose internal logic is a dependent-linear type theory
Dependent-linear type theories may be a functional programmer's dream, but is it categorically interesting, i.e. is it the internal language of an "interesting" category? By "...
- 1,175
6
votes
2
answers
321
views
Intuition behind nested positivity and counterexamples
I'm looking at the nested positivity conditions for inductive types stated in the Coq manual. First off, are there any other references (not necessarily for Coq, but in dependent type theories ...
- 325
6
votes
0
answers
122
views
Is there a known notion of "stochastic dependent pair"?
I came upon this when thinking about the semantics of probabilistic programs. Say you have a generative model
N ~ Poisson()
for n = 1:N
X[i] ~ Normal()
Then the ...
- 229
7
votes
0
answers
232
views
Category theory lambda cube?
If simply typed lambda calculus corresponds to cartesian closed categories, what types of categories do other calculi in the lambda cube correspond to?
https://en.m.wikipedia.org/wiki/Lambda_cube
- 163