Questions tagged [dependent-types]

An overlapping feature of type theory and type systems.

15 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
8
votes
0answers
138 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, ...
5
votes
0answers
48 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: ...
5
votes
0answers
60 views

Can we simulate any dependent datatype with `Eq`?

Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
3
votes
0answers
62 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.
3
votes
0answers
125 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 ...
2
votes
0answers
38 views

Can HOL be simulated in the CiC?

I was wondering if HOL (higher-order logic) can be simulated in the Calculus of Inductive constructions (CiC)
2
votes
0answers
58 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 ...
2
votes
0answers
53 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 ...
2
votes
0answers
102 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, ...
1
vote
0answers
50 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 ...
1
vote
0answers
65 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 ...
1
vote
0answers
90 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
0answers
29 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 ...
0
votes
0answers
46 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. ...
0
votes
0answers
430 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 ...