Questions tagged [dependent-types]
An overlapping feature of type theory and type systems.
26
questions with no upvoted or accepted answers
7
votes
0
answers
148
views
Extensional constructs in minimal extensional type theory without eta equality
The extensional version of Intuitionistic Type Theory is usually formulated in a way that makes extensional concepts like functional extensionality derivable. In particular, equality reflection, ...
- 71
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.9k
5
votes
0
answers
65
views
Can we simulate any dependent datatype with `Eq`?
Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
- 29.9k
4
votes
0
answers
101
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 ...
- 731
4
votes
0
answers
67
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 ...
- 273
3
votes
0
answers
349
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,070
3
votes
0
answers
140
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 ...
- 319
3
votes
0
answers
117
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
3
votes
0
answers
146
views
Test cases for subtyping with dependent types
I implemented a simple type system inside Agda and I'm trying to understand, how expressive it is. The system consists from a predicative hierarchy of universes in the style of Russell, natural ...
- 336
2
votes
0
answers
84
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 ...
- 240
2
votes
0
answers
60
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
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:...
- 283
2
votes
0
answers
105
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.9k
2
votes
0
answers
78
views
Are there any interesting terms in pure LF or $\lambda\Pi$?
In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$.
I know that LF and the dependently typed ...
- 29.9k
2
votes
0
answers
123
views
Dependent types as regular expressions
Would be possible to encode dependent types as regular expressions? if so, ¿is there some work about?
It's common to represent restrictions for elements in a traversable data structure with them, ...
- 129
1
vote
1
answer
68
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
0
answers
43
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
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
1
vote
0
answers
28
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,275
1
vote
0
answers
39
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
1
vote
0
answers
81
views
DML , ML with restricted dependent types
Refering to this paper
Dependent ML: An Approach to Practical
Programming with Dependent Types
Have defined datatype 'alist ( int ) Its not clear why they have used int as a parameter rather than a ...
- 933
1
vote
0
answers
538
views
Type inference and Type checking
I understand that adding the annotations (dependent typing) may cause the type checking of the programming language to become undecidable.
What about type inference ?
Whether type checking and type ...
- 933
1
vote
0
answers
104
views
Representing inductive types
I implemented dependently typed lambda calculus in the spirit of this article: http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
The calculus, works and I experimented with it and like it. However, I ...
0
votes
1
answer
80
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
0
votes
0
answers
80
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