Questions tagged [dependent-types]
An overlapping feature of type theory and type systems.
117
questions
3
votes
1
answer
143
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 ...
- 30k
0
votes
1
answer
52
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 ...
CommunityBot
- 1
9
votes
1
answer
394
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 ...
- 304
4
votes
1
answer
91
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!
- 111
0
votes
0
answers
26
views
Introduction to Calculus of Inductive Constructions
Which books/notes teach Calculus of Inductive Constructions (CIC) without using a specific programming languages like Coq or Lean? I would like a reference that also doesn’t assume (naive) set theory, ...
- 101
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 ...
- 30k
1
vote
0
answers
40
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
1
vote
0
answers
93
views
Can the Calculus of Constructions (without inductives) be used to axiomatize mathematics?
I'm aware that proof assistants like Coq and Agda are based on CIC rather than CoC because there is e.g. no inductive natural number type in CoC. Therefore, for example the proof that addition is ...
- 329
3
votes
2
answers
155
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 ...
- 156
2
votes
1
answer
109
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 ...
- 1,589
2
votes
0
answers
77
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 ...
- 220
0
votes
1
answer
76
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,589
1
vote
1
answer
146
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 ...
- 2,619
5
votes
2
answers
633
views
Decidability of dependent typing on primitive recursive languages
With a dependent type system in a normal functional language type checking may never halt. This is partially because dependent typing removes the isolation between types, and code. My question is this:...
- 220
1
vote
0
answers
24
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,163
6
votes
2
answers
488
views
What are the rules for positive recursive types in dependent type theory?
I've recently started independently learning type theory, using a combination of papers found online and ncatlab.org (but have not worked with category theory), and am about to start reading TAPL.
I'...
- 5,091
20
votes
3
answers
2k
views
Is path induction constructive?
I'm reading through the HoTT book and I have a hard time with path induction.
When I look at the type in the section 1.12.1:
$$\text{ind}_{=_A}:\prod_{C:\prod\limits_{x,y:A}(x=_Ay)\to \mathcal{U}}
\...
- 23
4
votes
3
answers
301
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 ...
- 8,114
3
votes
0
answers
239
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 ...
- 3,000
2
votes
1
answer
110
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 ...
- 908
16
votes
1
answer
5k
views
What is different between Set and Type in Coq? [closed]
AFAIU types can be a Set whose elements are programs or a proposition whose elements are Proofs. So based on this understanding:
...
- 29.7k
2
votes
0
answers
53
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 ...
- 326
4
votes
0
answers
95
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 ...
- 711
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:...
- 273
2
votes
1
answer
79
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:...
- 2,619
3
votes
1
answer
212
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 ...
- 8,114
5
votes
1
answer
573
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? ...
- 29.7k
4
votes
1
answer
314
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 "...
CommunityBot
- 1
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 ...
- 263
4
votes
1
answer
94
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 ...
- 29.7k
2
votes
2
answers
137
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 ...
- 30k
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 ...
CommunityBot
- 1
27
votes
1
answer
3k
views
What are the strongest known type systems for which inference is decidable?
It's well known that Hindley–Milner type inference (the simply-typed $\lambda$-calculus with polymorphism) has decidable type inference: you can reconstruct principle types for any programs without ...
76
votes
4
answers
16k
views
Dependent types vs refinement types
Could somebody explain the difference between dependent types and refinement types? As I understand it, a refinement type contains all values of a type fulfilling a predicate. Is there a feature of ...
- 121
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 ...
- 141
9
votes
2
answers
2k
views
Is it possible to do Dependent Types in Typed Racket?
Is it possible to use Dependent Types in the existing Typed Racket implementation? (ie do they exist in it?)
Is it reasonably possible to implement a Dependent Types System using Typed Racket?
- 103
3
votes
0
answers
116
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 ...
- 329
3
votes
2
answers
288
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.
...
- 31
2
votes
0
answers
97
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 ...
- 29.7k
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:
...
- 29.7k
0
votes
1
answer
178
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 ...
- 101
0
votes
0
answers
76
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.
...
- 621
16
votes
2
answers
884
views
Can I have a "dependent coproduct type"?
I'm reading through the HoTT book and I have a (probably very naive) question about the stuff in the chapter one.
The chapter introduces the function type
$$ f:A\to B $$
and then generalizes it by ...
CommunityBot
- 1
11
votes
1
answer
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 ...
- 30k
3
votes
0
answers
107
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.
- 565
8
votes
1
answer
819
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 ...
- 2,619
4
votes
2
answers
171
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 ...
4
votes
1
answer
231
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 ...
- 29.7k
5
votes
1
answer
400
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 ...
5
votes
1
answer
98
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 ...
- 29.7k