Skip to main content

Questions tagged [dependent-type]

An overlapping feature of type theory and type systems.

Filter by
Sorted by
Tagged with
1 vote
1 answer
142 views

Can the Sigma type be defined in terms of the pi type in dependent type theory?

Using the Curry-Howard Correspondence and the fact we can write: $$\forall x: f(x) \equiv \not \exists x: \lnot f(x)$$ Can we write the $\sum$ type in terms of the $\prod$ type? $$\sum(x:A)B(x) \...
zooby's user avatar
  • 113
3 votes
1 answer
79 views

What are some practical applications of inductive-inductive and inductive-recursive types?

Since this question got not many answers Im hoping asking again could convey that this has some importance. Anyway so in undergraduate education, I was working on research to implement dependent-...
AnonymousThunk's user avatar
2 votes
1 answer
121 views

Derivability of `Vector` in pure calculus of constructions

I am learning pure type systems to better understand functional (and general) programming. My question arises mainly from the two facts: It is known that we can define (co)inductive types in pure ...
Andrew's user avatar
  • 121
2 votes
1 answer
79 views

What Pure Type Systems have dependent types

What precisely are dependent types? Is it a syntactic property of some type system? This seems to suggest that dependent types are defined through phase distinctions. For example, if a variable is ...
Trebor's user avatar
  • 345
1 vote
1 answer
65 views

Are there any books or articles that contain information on the P weak omega or second order predicate calculi?

I have been trying to learn about the lambda cube, but cannot find any sources covering the P weak omega and P2 nodes. Is the problem that these nodes are not frequently used/ offer little benefits ...
hugofin's user avatar
  • 11
3 votes
2 answers
216 views

Generalizations, or extensions of W-types in MLTT

I'm interested in making a very stripped down implementation of MLTT, or possibly HoTT or cubical type theory (though I've yet to grok the glue rule in cubical type theory and both it and composition ...
Jake's user avatar
  • 1,203
2 votes
1 answer
121 views

Is beta normalization used for program optimization?

Beta normalization reduces a lambda term to its beta normal form, if it exists. The beta normal form is a computationally equivalent term with no "redundant" computation, in a sense; for ...
Hirrolot's user avatar
  • 105
-1 votes
1 answer
87 views

Notation problem

The following problem arises when I try to define a new notation. I have a function f : A -> A -> A -> A -> Type Then I want special notation for the ...
coqbeginner's user avatar
3 votes
0 answers
63 views

What are some practical applications of inductive-inductive types?

By "practical applications" I mean in usual programming/industry. I am particularly interested in cases where the inductive-inductive types cannot be easily replaced by inductive-recursive ...
Fernando Chu's user avatar
1 vote
1 answer
97 views

Can I define nested mutually dependent types in Coq?

I am trying to model the following in Coq, which works fine in Haskell (below is Haskell code): ...
Henri_S's user avatar
  • 13
3 votes
1 answer
271 views

Model foreign keys as dependent types?

A database consists a list of tables. For example you have a table of Worker and a table of Project where each project needs a ...
molikto's user avatar
  • 347
2 votes
1 answer
170 views

Where can I find more information about "dependent elimination"?

I am trying to find more information (preferably an academic paper) for the concept of "dependent elimination". I understand the concept itself: it means constructing a type by eliminating a ...
Valmir Junior's user avatar
1 vote
1 answer
95 views

Intuition behind UTT's internal logic

The "internal logic" of type theory UTT is defined in LF as follows: What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - ...
user175254's user avatar
1 vote
1 answer
145 views

Formulation of Tarski-style universes in LF

Lately I've been asking questions on type theory on MSE, and I've been getting great answers, but I decided to give a try to this site and see if it will be helpful as well. I'm looking at this note ...
user175254's user avatar
5 votes
1 answer
324 views

Dependent type theory and definitions of cumulativity

Many dependent type theories employ an universe hierarchy to compensate for the fact that Type : Type is inconsistent (due to Girard's paradox). A cumulativity relation is then defined to lift terms ...
Qiancheng Fu's user avatar
2 votes
0 answers
136 views

Why Multiple Clocks in Guarded Dependent Type Theories?

The main purpose of clocks in guarded type theories (originating in Atkey & McBride ICFP 2013) is so that we can define coinductive constructions from guarded recursive definitions. Semantically ...
Max New's user avatar
  • 1,695
3 votes
1 answer
415 views

Similarities and differences between Pie and popular languages with dependent types

The book The Little Typer explains dependent types using a toy language called Pie (https://github.com/the-little-typer/pie). How similar is Pie to the popular languages with dependent types: Coq, ...
CrabMan's user avatar
  • 133
4 votes
1 answer
303 views

Dependently typed monad

I have came across something that looks like a dependently typed monad. I would like to know if something like this is studied and where can I find more information about it. Let's have these two ...
tom's user avatar
  • 171
5 votes
1 answer
346 views

How do we use directed univalence in directed type theory?

In directed type theory of Riehl and Shulman, we have a new type, $hom_A\:x\:y$ representing arrows between elements $x$, $y$ of type $A$, note that these are not a priori functions. I will call the ...
Ilk's user avatar
  • 920
6 votes
1 answer
214 views

Is there a way to define dependent types without explicit substitutions internally within agda?

I am playing around the Programming Language Foundations in Agda exercises and wondering if we can achieve the same level of theories with dependent types. With simple types, the definition usually ...
Kaa1el's user avatar
  • 163
8 votes
0 answers
142 views

For which type systems have normalizaton proofs been formalized?

I am trying to understand what the open problems are in the area of formalizing proofs of normalization for type systems. Obviously STLC has been done many times. For predicative System F, I found one ...
while1fork's user avatar
8 votes
4 answers
552 views

Type theory and fixed points of datatypes

For the purposes of this question, say that a datatype is a type constructor with one type parameter (this is sometimes called a type operator). In Haskell, we can define a fixed point ...
Ilk's user avatar
  • 920
3 votes
1 answer
120 views

Implementation of vectors as dependent types in CoC

I'm trying to understand dependent types in CoC and I am having trouble finding examples that are actually carried out in CoC, specifically without inductive types or pattern matching. The most ...
Cristian Gratie's user avatar
4 votes
1 answer
202 views

Effect of HoTT/Univalence Axiom on equality between terms of inductive types?

It is well known that Univalence contradicts Axiom K, for example there are two ways $\mathbf{2} = \mathbf{2}$ may be proved using Univalence, via $\mathtt{id}_{\mathbf{2}}$ or $\mathtt{not}$. But ...
Guest0x0's user avatar
  • 151
8 votes
2 answers
563 views

What's the categorical semantics of definitional equality?

The categorical semantics of a dependent type theory is normally described as a CwA/CwF/CompCat/etc. and in these models, we can talk about propositional equality by interpreting an 'identity type'. ...
ice1000's user avatar
  • 957
6 votes
3 answers
2k views

How does type theory change how one thinks about programming?

I have been dabbling in HoTT and I am convinced that dependent type theory is much more suitable than set theory for proof assistants. Now, this made me wonder - how fundamental is Type Theory ...
Arjo's user avatar
  • 169
3 votes
1 answer
196 views

Counterexample request: ill-scoped metavariable solution

This is a question on metavariable (aka holes) resolution in (dependent) type theories. In many referential implementations (such as Andras Kovacs' elaboration-zoo), there is one step called 'scope ...
ice1000's user avatar
  • 957
9 votes
0 answers
207 views

Constructive Strong Normalization of the Extended Calculus of Constructions

The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ...
helmut's user avatar
  • 375
3 votes
1 answer
216 views

How to think about `comp` in cubical type theory

Consider the definition: ...
Siddharth Bhat's user avatar
5 votes
1 answer
459 views

Example use cases for induction-recursion

I know of only two uses of induction-recursion: Encoding universes as a type, as shown in the Agda docs for recursion Encoding Finite sets as shown in Conor Mc'Bride's "datatypes of datatypes&...
Siddharth Bhat's user avatar
1 vote
0 answers
104 views

CubicalTT: successor of add proof?

Lecture 2 of the cubical type theory lectures provide a proof of (suc a) + b = suc (a + b): ...
Siddharth Bhat's user avatar
2 votes
0 answers
102 views

MLTT/MiniTT: why do normal forms of sum types carry environments?

I am learning how to implement MiniTT: a simple type theoretic language, which is a dependently typed language with sum types, mutual recursive/inductive definitions and a universe of small types. A ...
Siddharth Bhat's user avatar
6 votes
1 answer
272 views

What are the pros and cons for type cases in dependent type theories?

Pattern matching on $\cal U$ is allowed in XTT and Idris2 (for unerased types), and that implies the injectivity of type constructors (that's just my intuition, though -- I also wonder how do I prove ...
ice1000's user avatar
  • 957
4 votes
1 answer
134 views

NBE for MiniTT: Why is labelled sum eliminator both a normal form and a neutral value?

I am studying A simple type-theoretic language: MiniTT, which introduces a dependently typed language with The language contains data types, mutual recursive/inductive definitions and a universe of ...
Siddharth Bhat's user avatar
3 votes
1 answer
193 views

References on implementing universe levels over MLTT?

I've followed the tutorial on Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen, where we implement a small dependently typed kernel with the axiom ...
Siddharth Bhat's user avatar
3 votes
2 answers
262 views

Bidirectional typing for dependent types: Why are Sigma, Pi synthesized?

According to the Pfenning philosphy of bidirectional typing, as also explained by Dunfield and Krishnaswamy 2013, constructors should be checked, while eliminators should be synthesized. Cconvention ...
Siddharth Bhat's user avatar
2 votes
2 answers
509 views

Does univ : univ always lead to a contradiction in a dependently typed language?

I am currently following Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen, where we consider the type of U (the universe ...
Siddharth Bhat's user avatar
3 votes
2 answers
548 views

What technique is used to implement type checking for CoC?

I am studying David Christiansen's tutorial on implementing a dependently typed language, where it says: Typed normalization by evaluation is far from the only way to implement conversion checking ...
Siddharth Bhat's user avatar
0 votes
1 answer
250 views

Calculus of constructions: Why forall when pi exists?

I'm studying the calculus of constructions from ATAPL, Chapter 2. I'm trying to understand the Type Equivalence rule, which describes the meaning of the new type family ...
Siddharth Bhat's user avatar
0 votes
2 answers
123 views

Pi-type over a list in dependent type theory

In a formalization I need to create an inductive type which has a term for each element in a list, something like this (I'll use Agda in the following, but everything here is standard dependent type ...
Max's user avatar
  • 113
3 votes
0 answers
96 views

Boltzmann sampling for containers/dependent polynomials?

I’d like to randomly sample from dependently-typed data structures. Has anyone looked at extending Boltzmann sampling to containers or dependent polynomials?
Neel Krishnaswami's user avatar
3 votes
1 answer
255 views

Is just one W-type enough for formalizing mathematics?

We work in intensional Martin-Löf type theory with $0$, $1$, $2$, $\Pi$, $\Sigma$, $W$ and a cumulative hierarchy of universes. Suppose our goal is to formalize constructive mathematics. Now if we ...
user avatar
2 votes
0 answers
162 views

Set-theoretic encoding of functions in type theory

Functions usually get encoded in set theory as follows. A function $A\to B$ is a subset $f\subset A\times B$ such that $\pi_1:f\to A$ is a bijection. In type theory to give a function $A\to B$ is to ...
user avatar
2 votes
1 answer
184 views

Dependent eliminator for empty type in intensional Martin-Löf type theory

In calculus of inductive constructions you can just say that the empty type is the type with no constructors and it automatically builds the dependent eliminator. But let's say I'm setting up ...
user avatar
1 vote
2 answers
205 views

Explicit type system with infinite non-cumulative universe hierarchy

Is there an open-source proof assistant or at least an explicit set of rules written down somewhere for a type system with an infinite non-cumulative universe hierarchy and unique typing? I want to ...
user avatar
2 votes
2 answers
158 views

$\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$

Is there a way to implement natural numbers in intensional Martin-Löf type theory so that addition and multiplication is judgmentally commutative?
user avatar
4 votes
1 answer
236 views

Model of MLTT with $\eta$ rule where function extensionality fails

Consider intensional Martin-Löf type theory with judgmental $\eta$ rule for dependent product types. Is there a model of it where function extensionality fails?
user avatar
4 votes
0 answers
176 views

Model of homotopy type theory where propositional & judgmental equality coincide for closed terms

In intensional Martin-Löf type theory we can prove the metatheorem that two closed terms are propositionally equal iff they are judgmentally equal. Is there a non-empty model of homotopy type theory ...
user avatar
2 votes
1 answer
90 views

Normal term of double negation of W-type

Consider the intensional Martin-Löf type theory without axiom of choice or the law of excluded middle. Let $A:U_0$ be a type and $B:A\to U_0$ be a function such that $\Sigma_{a:A}(B(a)\to 0)$is ...
user avatar
6 votes
1 answer
536 views

Defining inductive types in intensional type theory purely in terms of type-theoretic data

To define a (non-indexed) W-type all we need is a type $A:U$ and a function $B:A\to U$ and we get a type $W_{a:A}B(a)$. To check that this definition is valid we only need to check that the ...
user avatar