Questions tagged [dependent-type]
An overlapping feature of type theory and type systems.
109
questions
3
votes
1answer
78 views
2
votes
1answer
107 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&...
0
votes
0answers
74 views
CubicalTT: successor of add proof?
Lecture 2 of the cubical type theory lectures provide a proof of
(suc a) + b = suc (a + b):
...
1
vote
0answers
62 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 ...
6
votes
1answer
152 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 ...
3
votes
1answer
69 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 ...
3
votes
1answer
72 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 ...
3
votes
2answers
110 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 ...
2
votes
2answers
405 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 ...
3
votes
2answers
338 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 ...
0
votes
1answer
117 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 ...
0
votes
2answers
71 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 ...
3
votes
0answers
79 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?
3
votes
1answer
203 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 ...
2
votes
0answers
134 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 ...
2
votes
1answer
98 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 ...
1
vote
2answers
107 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 ...
0
votes
0answers
47 views
Complexity of finding typing derivation trees
In type theories where type checking is decidable do we have estimates for how much time/space it takes to find a typing derivation tree of a valid typing judgment? Do any published references do this ...
2
votes
2answers
128 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?
4
votes
1answer
129 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?
4
votes
0answers
145 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 ...
2
votes
1answer
75 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 ...
5
votes
1answer
272 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 ...
3
votes
1answer
141 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 ...
6
votes
1answer
218 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 ...
4
votes
0answers
147 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 ...
7
votes
1answer
112 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 "...
6
votes
2answers
241 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 ...
6
votes
0answers
100 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 ...
6
votes
0answers
136 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
3
votes
0answers
116 views
Would it be possible to derive `transp` natively from Path, Interval and typecase?
Assume for a moment that we extended Agda with an Interval and a Path type, but not transp (which is a primitive currently). I'm ...
2
votes
1answer
175 views
Defining finite sets inductively in a proof assistant?
To represent finite sets within coq, we either use something like ListSet, which are just definitions on top of list, or we ...
6
votes
0answers
144 views
Postulating self types in a proof assistant
Self types introduce two typing new rules (simplified):
$
\frac{\Gamma \; \vdash \; t : [t/x]T}{\Gamma \; \vdash \; t : \iota x. T}$ I-self and
$
\frac{\Gamma \; \vdash \; t : \iota x. T}{\Gamma \; \...
2
votes
1answer
202 views
Non-termination, strict positivity and free monads
Using the standard encoding of a free monad in Haskell and its fmap instance:
...
3
votes
1answer
128 views
Type of induction principle for fixpoint types
To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a ...
3
votes
0answers
143 views
Set:Set or Negative Inductives in a Total Language?
In total dependently typed languages, general recursion is forbidden, since this can allow for non-terimination. However, dependently typed language can still describe Turing-complete computations (...
4
votes
0answers
175 views
Implementations of Dependent Type Theory
I am trying to find a minimal implementation of dependent type theory that supports
Pi Types (obviously)
Modules containing records
Inductive data types
Universe Hierarchy
A notion of equality
...
2
votes
1answer
145 views
Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook
I am working through the Dependent Types chapter from Advanced Topics in Types and Programming Languages (ATTAPL) by Benjamin Pierce et al. I am confused with the calculus presented Fig 2-7 (Calculus ...
0
votes
0answers
78 views
Proposition terms vs types in Coq
Consider the following div function written in Coq. It takes in a proof that the divider is non-zero.
Definition div (n d:nat) (pf: ~(d = 0)) := n/d.
Focus on <...
8
votes
1answer
429 views
PHOAS with extrinsic typing?
Parameterized Higher Order Abstract Syntax (PHOAS) is a representation of syntax trees that allows the host language's binding to be used to represent binding in the language being modelled, while ...
5
votes
1answer
257 views
Small kernel (i.e. proof-verifier) for Agda?
Proof-assistants usually include a lot of machinery that assists in the creation of proofs. The creation process may be unsound without risking the soundness of the proof-assistant if the alleged ...
6
votes
1answer
288 views
Fixed set of type constructors to simulate all intensional inductive families?
I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction ...
6
votes
1answer
208 views
Structural equality of Pi Types with heterogeneous equality?
I'm trying to implement a proof of the following type:
...
3
votes
1answer
96 views
Formalization of dependent record types/kinds in MLTT or variant thereof?
Has anyone formalized Pollack's Dependently Typed Records in Type Theory ? Agda would be preferred, but anyone close to MLTT would work. Weaker versions would be fine too, i.e. what Luo dubs '...
11
votes
2answers
417 views
Intuition Behind Strict Positivity?
I'm wondering if someone can give me the intuition behind why strict positivity of inductive data types guarantees strong normalization.
To be clear, I see how having negative occurrences leads to ...
6
votes
1answer
212 views
What will go wrong if a recursive record type has a negative eta rule?
In the context of Agda like dependent type theory:
This short paper https://jesper.sikanda.be/files/vectors-are-records-too.pdf says some inductive type can be seen as records, for example ...
1
vote
1answer
153 views
First-order multi arity functions in dependent type?
(cross posted from Reddit https://www.reddit.com/r/dependent_types/comments/b1ts8b/firstorder_multi_arity_functions_in_dependent_type/?
Take Agda for example, functions of multi arity is "encoded" as ...
8
votes
0answers
501 views
An axiom for John Major's Equality
In the the standard library of Coq, there is the axiom:
Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
Why isn't it provable? Can it be reduced ...
1
vote
1answer
130 views
Dependent C-style types with subtyping rule
I'm looking for previous work regarding an extension of a C-style type system in which types may have constraints and have a defined subtyping rule. In particular, I'm interested in defining algebra-...
1
vote
1answer
140 views
Definitional equality of recursive function definition by “infinite unfolding”
The context is checking definitional equality in dependent type theory implementations.
Consider in Coq
...
