# Questions tagged [dependent-types]

An overlapping feature of type theory and type systems.

88 questions
Filter by
Sorted by
Tagged with
86 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 ...
36 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 ...
39 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: ...
96 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 ...
33 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. ...
439 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 ...
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 ...
54 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.
138 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 ...
80 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 ...
66 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 ...
62 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 ...
111 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 ...
51 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 ...
67 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 ...
44 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 ...
184 views

62 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 ...
175 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: ...
53 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)?
68 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 ...
2k 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 ...
61 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 ...
494 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 ...
272 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 ...
5k views

### What makes type inference for dependent types undecidable?

I have seen it mentioned that dependent type systems are not inferable, but are checkable. I was wondering if there is a simple explanation of why that is so, and whether or not there is there a limit ...
201 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. ...
203 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'...
51 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 ...
187 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 ...
123 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 ...
2k 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: ...
131 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, ...
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?
132 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 ...
179 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 ...
615 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 ...
160 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 ...