# Questions tagged [dependent-type]

An overlapping feature of type theory and type systems.

81 questions
Filter by
Sorted by
Tagged with
81 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 ...
102 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
109 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 ...
142 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 ...
127 views

534 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 ...
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 ...
378 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 ...
385 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 ...
255 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 ...
253 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 ...
211 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 ...
736 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, ...
129 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 ...
346 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 ...
408 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 ...
159 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 ...
360 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 ...
139 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 ...
245 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). ...
251 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 ...
153 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 ...
146 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 ...
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 ...
430 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 ...