Questions tagged [dependent-types]

An overlapping feature of type theory and type systems.

Filter by
Sorted by
Tagged with
0
votes
1answer
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 ...
2
votes
0answers
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 ...
5
votes
0answers
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: ...
0
votes
1answer
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 ...
0
votes
0answers
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. ...
13
votes
2answers
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 ...
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
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.
5
votes
1answer
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 ...
2
votes
1answer
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 ...
4
votes
2answers
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 ...
2
votes
1answer
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 ...
4
votes
1answer
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 ...
5
votes
1answer
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 ...
1
vote
2answers
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 ...
1
vote
1answer
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 ...
3
votes
2answers
184 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{...
5
votes
2answers
85 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
150 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
608 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
81 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
52 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
174 views
3
votes
1answer
70 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 ...
3
votes
1answer
144 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 ...
4
votes
1answer
68 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
96 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
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 ...
5
votes
1answer
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: ...
0
votes
1answer
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)?
2
votes
1answer
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 ...
22
votes
1answer
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 ...
4
votes
2answers
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 ...
10
votes
2answers
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 ...
3
votes
1answer
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 ...
42
votes
1answer
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 ...
3
votes
1answer
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. ...
6
votes
2answers
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'...
1
vote
1answer
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 ...
11
votes
2answers
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 ...
5
votes
1answer
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 ...
12
votes
1answer
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: ...
8
votes
0answers
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, ...
8
votes
2answers
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?
3
votes
1answer
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 ...
8
votes
2answers
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 ...
8
votes
1answer
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 ...
4
votes
2answers
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 ...
18
votes
2answers
431 views

“Minimal” intuitionistic type theory?

I'm surprised that people keep adding new types in type theories but no one seems to mention a minimal theory (or I can't find it). I thought mathaticians love minimal stuff, don't they? If I ...
10
votes
1answer
251 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-...