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
2 answers
204 views

What is a context mapping in dependent type checking?

I am reading a dissertation about dependent type programming language (Norell, 2007), and had much trouble understanding the definition of context mappings/substitutions as shown in the figure below . ...
tinlyx's user avatar
  • 1,772
2 votes
1 answer
185 views

What is a pattern in dependent pattern matching?

I am trying to understand dependent pattern matching while reading Goguen, McBride, and McKinna (2006)'s paper, but couldn't quite grasp the concept. I know regular pattern matching in functional ...
tinlyx's user avatar
  • 1,772
1 vote
1 answer
68 views

Use proof irrelevance in cast

I'm working using cast in Coq.Vectors. When trying to rewrite with proofs, I'd like to use the fact of proof irrelevance (Coq.Logic.Eqdep_dec), preferably automatically. I.e., when I have a lemma ...
Adrian L's user avatar
1 vote
0 answers
58 views

Embedding proof assistance in an application

Context Perhaps this is too open-ended a question for StackExchange, in which case I apologize, but otherwise here goes: I have a project I'm toying around with, the core of which is what I'd call &...
Eric Anderson's user avatar
2 votes
1 answer
58 views

Eliminating dependent destruction in Coq

I'm working on developing a theory of arithmetic within a framework for first-order logic I constructed in Coq. The following is a simplified version of the scenario I'm working with. ...
Circuit Craft's user avatar
2 votes
1 answer
122 views

Provable `fun-ext`and "rewriting under binders" in intensional MLTT

I've noticed that the underlying judgemental machinery of intensional MLTT can be extended such that function extensionality becomes provable. Or in other words it becomes possible to "rewrite ...
Russoul's user avatar
  • 345
1 vote
1 answer
86 views

Type of Sets with an Assocaitive Operation in Lean

This is probably a really simple question, but I am no able to find something in the Lean reference manual. I want to define a type of sets equipped with an associative operation. I have tried the ...
Nico's user avatar
  • 722
2 votes
2 answers
134 views

What if identity type in extensional type theory were possibly non-deterministic?

In extensional type theory, identity types are lifted to the definitional equality mechanism, this lead to a bunch of problems, and I imagine that's why they are not very popular. My question is if we ...
Tiago Campos's user avatar
3 votes
1 answer
80 views

Tricks for proving equalities under type cast

I sometimes stumble across proofs that prove equalities in the form of forall a b (p: a = b), C a = match p with | eq_refl => C b end without resorting to ...
shooqie's user avatar
  • 171
4 votes
1 answer
168 views

Co-induction principle

It's known that Nat-ind = Nat-rec ⨯ Nat-initiality Has someone figured out how to define a suitable Conat-coind such that ...
Russoul's user avatar
  • 345
4 votes
3 answers
261 views

Rewrite with definitional equality and dependent types

In Coq, there are some terms that are equal by definition, but there's not an easy way to replace one value with the other inside a proof. The two ways that I know that work in general are to use the ...
sudgy's user avatar
  • 193
3 votes
2 answers
211 views

How to abstract over function arity in Lean and Coq?

Given types $A, B$ I would like to express the type of all functions $f$ for which there exists an $n \in ℕ$ such that $f$ has type $A^n \to B$. And possibly in such a way, that for $a_1, \dots, a_n : ...
8bc3 457f's user avatar
  • 224
2 votes
0 answers
57 views

Elimination rules of inductive types

Why does the elimination rule of inductive types sometimes allow the target type to depend on the inductive type and sometimes not? I am confused by that. Is it correct that it makes no difference in ...
Nico's user avatar
  • 722
1 vote
1 answer
89 views

Destruction of bound dependent types

I'm having an issue with dependent typing. I have reduced it to the following minimal example: ...
Adrian L's user avatar
4 votes
1 answer
232 views

What types can be written in Kind but not Lean?

The Kind programming language has a sufficiently powerful type system to support proving theorems like in Lean, Coq, Idris, or Agda. I've seen it said that Kind has an even more powerful type system ...
user32157's user avatar
  • 151
0 votes
0 answers
61 views

Cardinals, universe levels, sheaves and predicativity

This question stems from some of my attempts to understand topos of coalgebras over a comonad from type-theoretic point of view. Paraphrasing the statement I am trying to understand (proposition 2.1, ...
Ilk's user avatar
  • 517
10 votes
1 answer
218 views

Universe inconsistency as an effect

The Internet tells me there is some work on languages that permit general recursion but carry information about possible divergence in the type system. For instance, the simply-typed language Koka ...
Mike Shulman's user avatar
  • 2,912
9 votes
1 answer
159 views

Interpretation of dependent types: Coherence

I have trouble understanding precisely how dependent type theories are intepreted in categories (in the most simple case, for example in a locally cartesian closed category). I know that a type in ...
Nico's user avatar
  • 722
3 votes
0 answers
84 views

Using crude but effective stratification & cong to implement transitivity of `=`

Suppose I have cong : {A B : Type} (f : A -> B) (p : a = b) : f a = f b coe : (A : I -> Type) -> A 0 -> A 1 It is ...
ice1000's user avatar
  • 5,877
4 votes
1 answer
239 views

How can you represent a dependent type visually?

So, obviously for a term $t$ of type $T$, I would represent it as: T +-----------+ | | | t | | | +-----------+ That is a node ...
Daniel Donnelly's user avatar
6 votes
1 answer
369 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 ...
Mike Shulman's user avatar
  • 2,912
4 votes
2 answers
173 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 ...
Trebor's user avatar
  • 3,688
7 votes
1 answer
290 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, ...
Ilk's user avatar
  • 517
8 votes
0 answers
253 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 ...
Shuchy's user avatar
  • 81
6 votes
0 answers
73 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 ...
Charlie Parker's user avatar
7 votes
1 answer
415 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 ...
BackusNaur's user avatar
4 votes
1 answer
196 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 ...
aradarbel10's user avatar
31 votes
2 answers
4k 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 ...
user833970's user avatar
6 votes
0 answers
127 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 ...
Molly Stewart-Gallus's user avatar
18 votes
2 answers
492 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 ...
Ende Jin's user avatar
  • 429
11 votes
1 answer
292 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 ...
Cheery's user avatar
  • 681
5 votes
1 answer
116 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 ...
Cheery's user avatar
  • 681
15 votes
2 answers
325 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 ...
Wno-all's user avatar
  • 1,098
9 votes
2 answers
304 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 ...
ice1000's user avatar
  • 5,877
5 votes
1 answer
143 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 ...
Greg Nisbet's user avatar
  • 2,711
16 votes
2 answers
343 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 ...
Blaisorblade's user avatar
9 votes
1 answer
337 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 ...
keep_learning's user avatar
9 votes
3 answers
190 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. ...
user9716869 - supports Ukraine's user avatar
17 votes
3 answers
585 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 ...
user9716869 - supports Ukraine's user avatar
13 votes
2 answers
267 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 ...
Wheat Wizard's user avatar
11 votes
1 answer
168 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 ...
Cheery's user avatar
  • 681
32 votes
3 answers
1k 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 ...
Guy Coder's user avatar
  • 2,826