Questions tagged [dependent-types]
An overlapping feature of type theory and type systems.
121
questions
4
votes
1
answer
351
views
Is there a fully combinatorial version of MLTT without lambda abstraction?
I have been learning MLTT and working on implementing its type checker referencing Coq's core language specification. Currently, I am at the stage of implementing its termination checker. I find it ...
- 173
1
vote
1
answer
64
views
Definition of semantics of coinductive type
It is relatively easy to construct an object in set/class theory which has properties of any of the following: dependent sum, dependent product, W-types.
E.g. Dependent sum of a family F is just the ...
- 111
1
vote
1
answer
46
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}\...
user164153
1
vote
0
answers
41
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 ...
- 131
2
votes
1
answer
43
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 \...
user164153
0
votes
1
answer
79
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 ...
- 331
0
votes
1
answer
72
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 ...
user157472
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 ...
user157472
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 ...
- 156
3
votes
2
answers
186
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 ...
- 209
2
votes
1
answer
141
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 ...
- 209
2
votes
0
answers
83
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 ...
- 230
0
votes
1
answer
110
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 ...
1
vote
1
answer
154
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 ...
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,...
- 2,265