Questions tagged [dependent-type]

Use this tag for questions about dependent types, which are families of types which vary over elements of another type.

Filter by
Sorted by
Tagged with
5 votes
1 answer
194 views

Very dependent functions

A "very dependent function" is a function whose output type at input $n$ depends on its own output values at inputs $k<n$. Is there a precise definition of such things that makes sense ...
  • 2,215
4 votes
2 answers
146 views

Formalization of abstract definitions

I'm asking about the abstract keyword in Agda and equivalent features in other languages. It marks a definition as non-expandable, potentially speeding up ...
  • 2,916
7 votes
1 answer
201 views

Can you build W-types out of natural numbers predicatively?

I understand that we can use W-types to encode natural numbers and a wide variety of other inductive types in intensional MLTT. Can we encode W-types using only natural numbers within type theory, ...
  • 251
7 votes
0 answers
177 views

Alternatives to universe levels

All of the type theory based proof assistants that I have seen have an infinite hierarchy of type universes to avoid the type of types being a term of itself. Are there alternative systems which could ...
  • 71
5 votes
0 answers
49 views

What are Generic Arguments in Coq and how are they structured in their OCaml code?

I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
6 votes
1 answer
158 views

How do I convince the Lean 4 type checker that addition is commutative?

In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the ...
4 votes
1 answer
121 views

What are instances of a dependent pair type?

Currently I am learning about dependent pair ($\Sigma$-)types, and I'm having some trouble understanding how an instance of a dependent type could be formed. I think I understand how the type of a ...
28 votes
2 answers
3k views

Has anyone ever accidentally "proven" a false theorem with type-in-type?

It is possible (with some cleverness) to prove false from type-in-type. For instance, Girard proved false in Martin Lof's original system (as described in the introduction of An Intuitionistic Theory ...
6 votes
0 answers
113 views

How to write heavily indexed proofs?

I've been playing with hereditary substitution. However, things get very awkward because substitution isn't total unless you index by the environment somehow. In my old approach terms were not indexed ...
18 votes
2 answers
387 views

What are the motivations for different variants of categorical models of dependent type?

I am new to the categorical semantics for dependent type theories, so it is surprising for me to see nLab introduces so many variants of categorical models, including comprehension categories, display ...
  • 427
10 votes
1 answer
181 views

Easy ways to introduce inductive types

I'm working up from elaboration zoo and noticed that you don't use fixed point if you've got type level computation. It causes unification/equality check to hang up. Now, this means that I need ...
  • 671
5 votes
1 answer
91 views

How to elaborate with dependent records present?

Dependent records can be implemented in various ways, but some papers suggests I could do it in the following way: The construction of dependent record type is made by selecting labels and types. The ...
  • 671
15 votes
2 answers
250 views

Are Logics Based on Dependent Types Stronger Than Ones Without?

There have been several times during I came across statements like Isabelle/HOL's logic is not rich enough to formalize X on various places online and in during personal discussions. Or similar ...
  • 998
9 votes
2 answers
223 views

What's the relationship between refinement types and dependent types?

In the F* proof assistant, they use refinement types together with dependent types. Based on my impression of F*, it seems to me that refinement types are just predicates in dependent type theory that ...
  • 4,740
5 votes
1 answer
118 views

How to implement first-order relational structures in Coq?

I'm trying to define a first-order relational structure in Coq. I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough. I also have a ...
  • 2,593
13 votes
2 answers
204 views

What are the upsides and downsides of typed vs untyped conversion?

What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"? Background Generally speaking, in dependent type ...
9 votes
1 answer
200 views

Type Checking Undecidable in Extensional Type Theory

What is the difference between intensional vs extensional type theories and how come the type checking is undecidable for extensional type theory? Also, how does it affect the expressiveness of ...
9 votes
3 answers
153 views

Generic proof assistants/modularity of the proof assistants?

One notable feature of Isabelle is that it allows for the definition and in-built integrated support of alternative object logics via the interface of Isabelle/Pure in combination with Isabelle/Isar. ...
15 votes
3 answers
470 views

Bringing OOP features into proof assistants?

I am aware that some of the proof assistants (e.g., Isabelle/HOL, Coq) provide an implementation of the so-called record types. For example, the library HOL-Algebra associated with the standard ...
12 votes
2 answers
145 views

What about dependent types is useful for theorem provers?

There are a good number of theorem provers which use dependent typing as a part of their type systems. It seems this proportion is much higher than in programming languages. So what is useful about ...
11 votes
1 answer
149 views

In the "Simply Easy!" paper, why is it safe to evaluate types in the empty environment?

The paper in question: An Implementation of a Dependently Typed Lambda Calculus by Andres Löh, Conor McBride and Wouter Swierstra. I'm wondering whether it's correct in what's it is doing. Precisely ...
  • 671
29 votes
3 answers
931 views

What are the bases for different Proof Assistants?

From the Wikipedia article on Proof Assistant it shows some Proof Assistants are based on Higher Order Logic, (HOL Light) and some are based on Dependent Types, (Coq). Are there any other means upon ...
  • 2,786