Questions tagged [dependent-types]

An overlapping feature of type theory and type systems.

Filter by
Sorted by
Tagged with
9
votes
1answer
1k 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 ...
3
votes
0answers
43 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.
4
votes
1answer
128 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
votes
1answer
77 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 ...
4
votes
2answers
57 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 ...
2
votes
1answer
52 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 ...
4
votes
1answer
75 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
1answer
48 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 ...
1
vote
2answers
61 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 ...
1
vote
1answer
42 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 ...
0
votes
1answer
81 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 ...
5
votes
2answers
82 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=_{\...
3
votes
1answer
141 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 ...
5
votes
1answer
600 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 ...
2
votes
1answer
77 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 ...
2
votes
0answers
51 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
2answers
122 views

How to prove this obvious theorem in type theory (LEAN prover)

I have the following code: ...
3
votes
1answer
68 views

How to determine whether a dependent type that doesn't fit the monad instance is categorically a monad

[Using Idris syntax and terminology, but the question is not about Idris] If a monad interface (or type class) has a constraint requiring applicative functor, a monad instance can be written by ...
4
votes
2answers
94 views

Finite list induction principle and the tail eliminator

In Dybjer's Inductive Families the author present a method to derive an eliminator/induction principle for every inductive family of types. In particular for the type of finite lists, namely $$List' \...
-1
votes
2answers
58 views

Defining an HTML Template as an Algebraic Type

Wondering if/how you could define a highly nested structure as a Dependent Type (or an Algebraic or Parameterized type). Specifically, an HTML template. Not that they work like this (HTML templates ...
4
votes
1answer
158 views

Dependent Type Theory Implementation of a Graph

In Haskell you find graphs defined like this: data Graph a = GNode a (Graph a) Or this: ...
0
votes
1answer
51 views

Meaning of $\mu t$ terms in dependent type theory

What is the meaning of the term $\mu t$ in the type theory formalized in this paper (section 2.1, page 2)?
2
votes
1answer
66 views

Show how lack of universe levels would create contradiction in homotopy type theory (in Agda)

The homotopy type theory book claims in section 1.3 that "As in naive set theory, we might wish for a universe of all types" but from this one could "deduce from it that every type, including the ...
4
votes
1answer
66 views

When do we need U(n+2) to solve a problem that can be formulated in U(n)?

I understand the need for a universe hierarchy, and that each new level brings additionnal proof-theoretic strength. In the HoTT book there are examples of proofs that need to use the next level in ...
4
votes
2answers
60 views

Union of fixed and floating point types

Say I have two real number types. They may be floating or fixed point. How can I construct a new type whose values are at least the union of the two with the minimal number of bits? There are 3 cases ...
10
votes
2answers
474 views

How to derive dependently typed eliminators?

In dependently-typed programming, there are two main ways of decomposing data and performing recursion: Dependent pattern matching: function definitions are given as multiple clauses. Unification ...
2
votes
1answer
244 views

Is it possible to implement dependent types by any object oriented language supporting inheritance and classes?

When I was reading Agda tutorial, I noticed resemblance between dependent type declarations and class definitions which I've been primarily used to work with. I'm not totally sure how much sense this ...
3
votes
1answer
174 views

Can we add dependent type into an existing imperative programming language?

As we know, dependent type allows programmers to write bugless programs. But as I know there's only very few languages support dependent type, like Haskell with extensions, Idris, Agda, F*, etc. ...
6
votes
2answers
186 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'...
1
vote
1answer
50 views

Is implication(function) more fundamental than lets say conjunction(product) in type theory?

According to the answer at (How to define function type in AGDA) the function type is kind of a fundamental thing in Agda and needed for bootstrapping, hence end user can not define it like what they ...
11
votes
2answers
182 views

Reducing products in HoTT to church/scott encodings

So I am currently going though the HoTT book with some people. I made the claim that most inductive types we will see can be reduced to types containing only dependent function types and universes by ...
5
votes
1answer
117 views

Relation between Hoare Type Theory and pointers

My understanding is that in Hoare Type Theory every imperative statement has a type of the form {Pre}res:T{Post} where T is the ...
11
votes
1answer
1k 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: ...
8
votes
0answers
127 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, ...
3
votes
1answer
129 views

Partial type inference for dependent types

I'm looking for resources on (partial) type inference for dependent types. For example there could be a type inference scheme that fails if the term doesn't have a principal type, or a scheme that ...
8
votes
1answer
565 views

What fragment of Martin-Löf dependent type theory can be expressed using generic types in Java?

I have recently come to realize that a number of problems I had a few years ago trying to implement various mathematical theories in Java came down to the fact that the typing system in Java is not ...
3
votes
2answers
173 views

partial (and non deterministic) functions in dependently typed lambda calculus

A partial function is one, that that is only defined on a part of its domain. Haskell gives examples: https://wiki.haskell.org/Partial_functions My end goal is to express types $$ \prod_{D:\mathcal{...
4
votes
2answers
143 views

What's the difference between the rank and the degree of a type function?

1 Context Near pg. 184 of Lambda Calculus and Combinators, the author is discussing the theory of dependent types. In particular, we are extending the lambda calculus to look at terms of form $$ \Pi ...
3
votes
1answer
140 views

Is it possible that the universe of types could be closed?

I asked a pretty vague question. I wasn't able to make it precise, but I can now. It seems to be out of the scope of the previous question, so I open another one. In dependently-typed languages such ...
10
votes
1answer
247 views

Why are recursive types needed as primitives for proofs in dependent type systems?

I'm relatively new to type theory and dependent programming. I've been studying the calculus of constructions (CoC) and other pure type systems. I'm particularly interested in using it as a proof-...
2
votes
0answers
96 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, ...
8
votes
2answers
175 views

Domain Theory and Polymorphism

Domain theory gives an amazing theory of computability in the presence of simple types. But when parametric polymorphism is added there doesn't seem to be a nice theory that explains whats going on ...
11
votes
1answer
141 views

Can properties such as memory usage of a function be expressed in a dependently typed language?

Suppose one wants to reason about properties of code beyond things like totality and functional purity - one also cares about the memory consumption, or algorithmic complexity of a function. Can this ...
19
votes
1answer
2k views

if (λ x . x x) has a type, then is the type system inconsistent?

If a type system can assign a type to λ x . x x, or to the non-terminating (λx . x x) (λ x . x x), then is that system ...
6
votes
1answer
161 views

Is it possible to prevent arithmetic errors with a dependent type system?

In a functional programming language I have functions like $$f\colon Int \times Int \times \cdots \times Int \to Int$$ which do some computation. However for certain arguments $(x_0, \dots, x_n)$ the ...
7
votes
1answer
308 views

Is there any difference between extensible records and dependent maps

In a typed setting, records can be thought of as a map from field to type. If there is a well-typed record merge operation (which allows overlapping fields), is there any real difference between the ...
3
votes
2answers
269 views

About the Identity function in Agda

I've defined the identity function in Agda as follows: idd : (∀ {ℓ} {A: Set ℓ}) → A → A idd a = a I want to ask you if the ...
2
votes
1answer
628 views

Examples of Dependent Types

I'm gathering examples from everything that I've read about Dependent Type Theory mainly from Dependent types at Work paper. This is my list so far of some dependent types (with abbreviations of ...
0
votes
1answer
95 views

Indexing a dependent type on a value?

If i'm recalling from Robert Harper's lectures Homotopy type theory A dependent type is a family of type index by a type. If we allow index to be just a value can we gain something instead of allowing ...
1
vote
0answers
60 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 ...