Questions tagged [dependent-type]
An overlapping feature of type theory and type systems.
82
questions
5
votes
2answers
208 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 ...
5
votes
0answers
84 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
112 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
114 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
150 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
131 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
180 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
116 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
138 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
155 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
...
1
vote
1answer
136 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
69 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
407 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
244 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
271 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
198 views
Structural equality of Pi Types with heterogeneous equality?
I'm trying to implement a proof of the following type:
...
3
votes
1answer
87 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 '...
10
votes
2answers
346 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
195 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
149 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
1answer
446 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
126 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-...
0
votes
1answer
134 views
Definitional equality of recursive function definition by “infinite unfolding”
The context is checking definitional equality in dependent type theory implementations.
Consider in Coq
...
4
votes
0answers
99 views
Proof that CIC or Dybjer-style eliminators are strongly-normalizing?
Related to this question
I'm wondering, what is the standard technique for showing that dependent types with eliminators are strongly normalizing? I'm thinking something like the Calculus of ...
4
votes
0answers
143 views
Hereditary Substitution with Inductives and Eliminators?
I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators?
In particular, normalizing the application of an eliminator to an ...
7
votes
3answers
345 views
When a type is a value?
In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...
5
votes
1answer
190 views
Strong Normalization of Extended Calculus of Constructions (CC with cumulative universes)
There are some proofs around to prove the strong normalization of the calculus of constructions (i.e. that all type systems in the lambda cube are strongly normalizing). I have analyzed the proof ...
6
votes
1answer
192 views
General Induction Principle
Let us suppose that we want to provide for each inductive type an axiom describing the associated elimination/induction principle. For example, given a definition for the naturals:
...
5
votes
2answers
360 views
Preservation under Substitution with Telescopes
In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution":
If $\Gamma \vdash v : \tau_1$ and $(x : \tau_1) \vdash t : \tau_2$,
then $\Gamma \...
11
votes
1answer
566 views
Proof techniques for showing that dependent type checking is decidable
I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and ...
7
votes
1answer
188 views
If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?
Question
If a pure type system has a terminating proof language, can we have Type : Type at the logic level without causing paradoxes (i.e., without causing ...
8
votes
1answer
408 views
Fixed points in dependent type theories
Most dependent type theories aim for some notion of correctness in two respects:
The type system must be decidable.
The type system must be consistent. e.g. $\forall \tau. \tau$ should not be ...
1
vote
2answers
396 views
What are the limitations of dependent typing?
It seems dependent types can provide lots of desirable guarantees about program behavior. What kinds of program properties can they NOT guarantee (besides what's computationally infeasible)? Is there ...
2
votes
0answers
264 views
What is the proof for the inconsistency of impredicaitivity + excluded middle + large elimination in type theory
Why is the combination of
impredicativity + excluded middle + large elimination
inconsistent in dependent type theory?
My understanding of large elimination is I am doing large elimination if I am ...
8
votes
2answers
265 views
How can you build a coinductive memoization table for recursive functions over binary trees?
The StreamMemo library for Coq illustrates how to memoize a function f : nat -> A over the natural numbers. In particular when ...
16
votes
0answers
212 views
Using Dependent Type Theory for Categories that are not LCCC
I have recently been working with polynomial functors and monads based mostly on Gambino-Kock. There they define polynomial functors in a Locally Cartesian Closed Category (LCCC) and extensively use ...
14
votes
2answers
751 views
In the Hott book, are the most of the type formers redundant? And if so, why?
In chapter 1 and Appendix A of the Hott book, several primitive type families are presented (universe types, dependent function types, dependent pair types, Coproduct types, Empty Type, Unit type, ...
4
votes
0answers
130 views
Completeness of realizability semantics for higher-order type theory
In this answer I mention a paper by Geuvers in which he describes a class of models for a type theory $\lambda P_2$ which is a sub-system of the CoC and roughly corresponds to 2nd order predicate ...
6
votes
2answers
350 views
Explicit set of types and terms in MLTT
Whenever I read a presentation of MLTT, especially in the context of the correspondence of MLTT with LCCCs (eg. Seely's paper), they say "the type constructors/formation rules are..." and then list a ...
6
votes
3answers
423 views
Proving running time upper bounds for algorithms in dependent type theory
Proof assistants are a valuable tool for verifying
the correctness of proofs of mathematical theorems.
When dealing with proofs of correctness of algorithms,
one is not only interested on showing ...
6
votes
0answers
162 views
Relationship between Pataraia's theorem and inductive-recursive definitions?
Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
3
votes
2answers
366 views
Motivation for Dependent Type
By the Curry-Howard Isomorphism we view propositions (or theorems if true/inhabited) as types.
But take the type $\mathbb{N} \implies \mathbb{N} \implies \mathbb{N} $.
We have as witnesses to this ...
6
votes
1answer
140 views
How to mechanically derive the recursor of a type from its constructors?
In Martin-Löf Dependent Type Theory a type is commonly prescribed by how to construct its canonical terms and how to show that its canonical terms are definitionally equal. This means that the ...
6
votes
1answer
247 views
Type checking, Hypothetical judgments, meaning explanations and computational type theory
We say that a system is a computational type theory if it is a type theory defined by not a bunch of inference rules, but some sort of Martin-Löfian meaning explanations (e.g. in the sense of NuPRL). ...
4
votes
1answer
252 views
Is it possible to verify a typechecker for a total dependently-typed language in that language's logic?
I understand the diagonalization argument against implementing an eval function in a total language, and that typechecking in a dependently typed language requires ...
1
vote
1answer
155 views
What's the effect of imposing the following restriction on inductive type families?
Let a simple expression be either:
A free variable
A data constructor of an inductive type family, applied to 0 or more simple expressions
What would be the effect of imposing the following ...
3
votes
1answer
149 views
What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?
In the context of constructive type theory, a term inhabiting some type is said to be in canonical form if it is explicitly built up using the constructors of that type.
Particularly, the only ...
7
votes
1answer
2k views
Dependent Types and Compile Time Types
I am trying to grok dependent types, and there's something that I find unclear.
In C++, templates can have non-type (template) parameters. The values of these parameters have to be specified at ...
7
votes
1answer
453 views
Examples of Universe inconsistency in normal use of dependent types
In dependent types, Type : Type results in inconsistency (Girard's or Hurken's paradox).
Are there examples of universe inconsistency (where assuming ...
8
votes
1answer
391 views
PiSigma: why does 'unfold' bind a variable?
I'm trying to understand the paper ΠΣ: Dependent Types without the Sugar by implementing an interpreter and type checker for the language. In doing so, I've seen that the ...
