Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [dependent-types]

An overlapping feature of type theory and type systems.

Filter by
Sorted by
Tagged with
0 votes
1 answer
37 views

In what sense do universes solve the problem of not having type $\Pi_{A:\text{Type}}B(A)$?

One motivation for introducing universes, as I see it, is that without universes, we cannot construct types like $\Pi_{A:\text{Type}}B(A)$ because they would require us to have $\Gamma.\text{Type}\...
user125234's user avatar
1 vote
0 answers
37 views

Dependent Types in $\lambda P$ vs MLTT

I am trying to understand the difference between $\lambda P$ and MLT, in particular the dependent type features. What is the difference between dependent types in $\lambda P$ and dependent types in ...
IllogicalUser's user avatar
1 vote
1 answer
40 views

Adding type constructors to universes

Suppse we have a Tarski-style universe $U$, which means, in particular, that the following rules are declared: $$\frac{}{\Gamma \vdash U \text{ type}} \quad \frac{\Gamma \vdash a:U}{\Gamma \vdash \...
user125234's user avatar
0 votes
1 answer
63 views

Application of dependent product

On the proof assistants StackExchange site, someone gave this example of a dependent product: $$\prod_{i\in I}\sum_{j\in J_i}x_{ij}=\sum_{f\in\prod_iJ_i}\prod_{i\in I}x_{if(i)}$$ The dependent product ...
Theo H's user avatar
  • 321
0 votes
1 answer
60 views

How to find a term that proves a given proposition?

I'm reading this book, and there's something basic that I don't exactly get. The authors say that every common noun is declared to be a type. For example, $Human:Type$. Then, they give an example of ...
user avatar
1 vote
1 answer
44 views

Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$

Let $\ast$ stand for "type" and $\square$ stand for "kind" so that $\ast:\square$. Suppose I want to find an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$. The derivation rules are ...
user avatar
1 vote
0 answers
44 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 ...
user32157's user avatar
  • 156
3 votes
2 answers
178 views

What are some examples of proofs that are also themselves "useful" programs?

With dependent types, types can be statements that are true or false and constructing a value with that type constitutes a proof of that statement. This proof/value construction is itself a program ...
ahelwer's user avatar
  • 209
2 votes
1 answer
133 views

What is an explanation of the replace operator in the Pie language?

This is the first concept in The Little Typer to give me quite a bit of trouble, and it appears I am not alone (1 2), so perhaps it would be beneficial to ask here. Hopefully this can be connected ...
ahelwer's user avatar
  • 209
2 votes
0 answers
82 views

What are strong examples of programming languages whose type systems don't embed into their native type theory?

Given a typical popular programming language, its native type theory is a dependent type theory which describes invariants, preconditions, predicates, and other generalizations of typical type-system ...
Corbin's user avatar
  • 230
0 votes
1 answer
98 views

Relationship between cartesian product and dependent product type

Introduction: Hi, I'm quite new to types so apologies in advance for the basic question and for any abuse of terminology. I believe I have a critical misunderstanding of dependent product types (and ...
NNNComplex's user avatar
1 vote
1 answer
152 views

Proving transitivity in an intuitionistic type theory without the K rule

In Agda, if I disable axiom $\mathbb{K}$ I'm not able to prove $$ \forall\{A : \textbf{Set}\}\{a\ b : A\}\{p\ q : a \equiv b\} \to p \equiv q, $$ which I guess is normal since the system does not ...
A confused dove's user avatar
1 vote
0 answers
27 views

How to specify a type for a SQL-like query?

What follows is a pretty complicated object (in an object-oriented, imperative, typed language), which I would like to create a type for with some sort of type annotations. I am open to how it is done,...
Lance's user avatar
  • 2,233
4 votes
3 answers
391 views

What is the runtime/time complexity of Coq’s (Dependent) Type Inference?

I remember learning in a class that type inference is decidable but usually takes a long time (e.g. type inference in OCaml is EXPTIME). I was wondering, since Coq allows programs/values themselves to ...
Charlie Parker's user avatar
3 votes
0 answers
297 views

What is the runtime (time complexity) of Type Inference in Simply Typed Lambda Calculus?

I was told that the runtime of OCAML or Scala is EXPTIME - which seems really bad! However, since people use type inference (deciding the type of a term or program or expression) in practice - it must ...
Charlie Parker's user avatar
2 votes
1 answer
119 views

Why does the CwF definition require a set of types under a context rather than a class of types?

In "Syntax and Semantics of Dependent Types" at the top of page 24, Martin Hoffman describes $\mathit{Ty}_{\mathcal C}(\Gamma)$ as the collection of semantic types under context $\Gamma$. It ...
Kevin Clancy's user avatar
2 votes
0 answers
57 views

"Universe-shrinking" function in Agda

Agda does not allow datatypes in one universe to be indexed by, or non-trivially parametrized by a type in a larger universe (strangely, Coq does not appear to require this for propositional ...
Jason Carr's user avatar
4 votes
0 answers
100 views

Is it possible to recover induction for nat from W-types?

W-types generalize the type of well-founded trees, i.e., possibly infinetely branching trees. I understand that inductive types may be encoded as such in dependent type theory (CIC, MLTT, etc), this ...
paulotorrens's user avatar
2 votes
0 answers
29 views

Data + data schema needs dependent types to be type-checked statically?

I will set this question in a very practical way. Let's say we have a web-form data received as JSON at the backend together with the schema (for instance, some version of JSON schema), something like:...
Roman Susi's user avatar
2 votes
1 answer
90 views

Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda

An observation when defining List in agda with --without-K enabled: The following parameterized inductive definition is accepted:...
Kaa1el's user avatar
  • 191
3 votes
1 answer
262 views

Is mutual inductive type definition essential in coq core language?

I'm studying Coq's core language and I found that mutual inductive type definition is in it. https://coq.inria.fr/refman/language/core/inductive.html#theory-of-inductive-definitions Before I read the ...
12412316's user avatar
  • 133
5 votes
1 answer
762 views

Resources for implementing dependent type theory

I want to implement Martin Löf's intuitionistic type theory in a functional language such as Haskell, preferably also implementing a lexer/parser for the language. How should I start approaching it? ...
thoughtpolice's user avatar
4 votes
1 answer
99 views

Resources for connections between dependent type theory and LCCC

Can someone recommend introductory articles/papers on the connections between dependent type theory and locally cartesian closed category? Many Thanks!
thoughtpolice's user avatar
4 votes
0 answers
66 views

Is there a computer language with optional dependent types?

I'm looking for a computer langauge with "dependent types" but... The problem with it having a full implementation is that you end up having to write formal type proofs to get even anything ...
zooby's user avatar
  • 263
9 votes
1 answer
417 views

Relationship between inductive families and type-returning functions

Dependently typed languages such as Agda support inductive families, also called indexed datatypes, which allow type parameters to vary between constructors. This can be used to define a set of ...
Alexis King's user avatar
4 votes
1 answer
325 views

Is occurrence typing (flow-sensitive typing) a form of dependent typing?

I take occurrence typing to be typing that "... allows the type system to ascribe more precise types based on whether a [check] succeeds or fails." (adapted from the Racket docs with "...
Max Heiber's user avatar
4 votes
1 answer
98 views

Which language is used to construct a type system?

Typically, OCaml and Scala seem to be used for designing any programming languages tool. But what features offer them an edge over other languages. A related question, is a type system for a language ...
mythbuster's user avatar
2 votes
2 answers
146 views

How to express a type that represents an associative array whose keys determine the type of the value?

I'm fairly new to type systems and theory, so I would appreciate some guidance in a problem that sparked my interest. I would like to understand what type system features are required so a compiler ...
fernandomrtnz's user avatar
1 vote
0 answers
38 views

How does this dependently-typed boolean elimination function work?

In the companion code to A Tutorial Implementation of a Dependently Typed Lambda Calculus - prelude.lp - there is a rather intimidating definition of a ...
Matt R's user avatar
  • 141
3 votes
0 answers
132 views

Does Type:Type lead to inconsistency without general inductive types?

In e.g. Agda , it is possible to derive an element of the empty type by enabling the "type in type" option. Every proof I have seen (and come up with) involves making a special inductive type ...
while1fork's user avatar
3 votes
2 answers
311 views

When is cumulative type universes useful?

AFAIK, a hierarchy of type universe(Type^0: Type^1: Type^2: ...) was introduced to avoid inconsistency caused by Type: Type. ...
heartpie2's user avatar
2 votes
0 answers
101 views

Simulating extensible sums with dependent types?

ML-style languages have a concept of "extensible" or "open" sum types, where variants can be declared at any point, and there's not a fixed number of constructors for the type. They're usually used to ...
Joey Eremondi's user avatar
5 votes
0 answers
61 views

Rules for consistency with mutual inductive families?

I'm trying to use a proof assistant to define a type and a relation that are mutually dependent on each other: ...
Joey Eremondi's user avatar
0 votes
1 answer
180 views

Is this statement of P = NP in Agda correct?

Looking for a self-contained statement of P = NP in type theory, I stumbled upon this short Agda formalization (a cleaned up version is reproduced below). The statement here does seem to express the ...
helianthus's user avatar
0 votes
0 answers
79 views

How is substitution in type theory the composition of classifying morphisms in category theory?

In the article at nlab about relation between category theory and type theory, it is said that substitution in type theory is the same as composition of classifying morphisms in category theory. ...
al pal's user avatar
  • 621
11 votes
2 answers
2k views

Why does Coq include let-expressions in its core language

Coq includes let-expressions in its core language. We can translate let-expressions to applications like this: let x : t = v in b ~> (\(x:t). b) v I understand ...
Labbekak's user avatar
  • 565
3 votes
0 answers
113 views

Calculus of constructions, type-in-type and recursion

Does adding type-in-type to the calculus of constructions lead to (general) recursion? Such that one can write the Y combinator.
Labbekak's user avatar
  • 565
8 votes
1 answer
933 views

What does canonicity property mean in Type Theory?

The "Computational Component" section of the Type Theory - Wikipedia (as well as a few papers about cubical type theory and 2d type theory) talk about canonicity property. Would you please explain ...
al pal's user avatar
  • 621
3 votes
1 answer
144 views

Difference between computation in proposition proof and definitional computation?

As stated in equality at nLab, "computational equality" is about computational steps which take for example, $s(s(0))+ s(0)$ to $s(s(s(0)))$ and it acts exactly and can be considered same as ...
al pal's user avatar
  • 621
4 votes
2 answers
177 views

Why values can not be replaced with their extensionally equal values in an intensional system?

Thomas Streicher states in Investigations into Intensional Type Theory(§Introduction p.5) that: Although in Intensional constructive set theory (Intensional Type Theory) one can do most of the ...
al pal's user avatar
  • 621
4 votes
1 answer
239 views

Definition of extensional and propositional equality in Martin-Lof extensional type theory

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.[4-5]) that: A similar situation occurs in extensional Martin-Lof type theory where propositional and definitional ...
al pal's user avatar
  • 621
5 votes
1 answer
410 views

Definitional equality of two propositions about propositional equality

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.3) that: It is important that definition equality is pervasive so if M and N are definitionally equal then P(M) is ...
al pal's user avatar
  • 621
5 votes
1 answer
101 views

What untyped term inhabits induction on natural numbers in CoC?

Induction on Church-encoded natural numbers (which I will call indNat) can not be defined within the Calculus of Constructions. If we assumed ...
Labbekak's user avatar
  • 565
2 votes
2 answers
156 views

Propositional truncation of excluded middle

It is clear to me that it should be impossible to prove : exclMidl = isProp A → ((A) ⊎ (¬ A)) Because it would give deciding oracle for every Proposition. My ...
MJG's user avatar
  • 125
1 vote
1 answer
84 views

Does dependent type checkers need to store lambda parameter type in their core language?

"Core language" refers to the exported well-typed terms that can be evaluated (or reduced). In the core language of MiniAgda, a dependently-typed language, the parameter type of a lambda is not ...
ice1000's user avatar
  • 940
1 vote
1 answer
116 views

Is it possible to interpret some Martin-Löf types as abelian monoids in such a way that any abelian monoid can be represented as a type?

For instance, I can interpret the unit type as the trivial monoid with one element. Non-dependent pairs $A \times B$ can be interpreted as the direct sum $A ⊕ B$ when $A$ and $B$ can both be ...
Andrew Cann's user avatar
5 votes
2 answers
131 views

Identity types and universes

Let us consider Martin-Löf type theory with a cumulative hierarchy of universes $$ \mathcal{U}_0\colon\mathcal{U}_1\colon\ldots $$ If $A, B\colon \mathcal{U}_i$, we can form an identity type $A=_{\...
Cohesion's user avatar
  • 153
5 votes
1 answer
207 views

Dependent type system with different computation model

There exist various Turing-equivalent models of computation, such as lambda calculus, Turing machines, or register machines. It seems that dependent type systems (like Coq, Agda, Idris, homotopy type ...
Jo Liss's user avatar
  • 290
6 votes
1 answer
840 views

Where are C++ templates inside of the lambda cube?

C++ templates have type variables and can express lambdas, so they must have System F embedded. But is that exactly where they are located in the lambda cube? Can C++ templates produce new types or ...
Fomalhaut's user avatar
2 votes
1 answer
148 views

Does co-inductive and co-recursive types also have their recursors?

I'm new to type theory, and recently read introductory materials where dependent type are discussed. One of my friend asked me, "Those dependent types are having recursors & 'inductors'(dependent ...
Bell Fox's user avatar