Reference. A simpler encoding of indexed types

Tesla Zhang · TyDe · 2021 · type-theory · DOI · arXiv
In functional programming languages, generalized algebraic data types (GADTs) are very useful as the unnecessary pattern matching over them can be ruled out by the failure of unification of type arguments. In dependent type systems, this is usually called indexed types and it’s particularly useful as the identity type is a special case of it. However, pattern matching over indexed types is very complicated as it requires term unification in general. We study a simplified version of indexed types (called simpler indexed types) where we explicitly specify the selection process of constructors, and we discuss its expressiveness, limitations, and properties.

Cite
Cite as @zhang-2021-a (helia, typst) · \cite{zhang-2021-a} (LaTeX)
BibTeX
bibtex · 10 lines
@inproceedings{zhang-2021-a,
  author = {Tesla Zhang},
  title = {A simpler encoding of indexed types},
  booktitle = {Proceedings of the 6th ACM SIGPLAN International Workshop on Type-Driven Development},
  publisher = {ACM},
  year = {2021},
  month = {8},
  pages = {14--22},
  doi = {10.1145/3471875.3472991}
}
hayagriva YAML (typst)
yaml · 12 lines
zhang-2021-a:
  type: article
  title: A simpler encoding of indexed types
  author: Zhang, Tesla
  date: 2021-08
  page-range: 14-22
  serial-number:
    doi: 10.1145/3471875.3472991
  parent:
    type: proceedings
    title: Proceedings of the 6th ACM SIGPLAN International Workshop on Type-Driven Development
    publisher: ACM
Download: zhang-2021-a.bib · zhang-2021-a.yml
Cited by (3)

(Co)condition hits the Path zhang-2024-coarXiv · 2024
We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax of higher inductive types in homotopy type theory, while coconditions generalize the cubical path type. (Co)conditions are also useful without an interval type. The duality between conditions and coconditions is presented in an interesting way: The elimination principles of inductive types with conditions can be internalized with records with coconditions and vice versa. However, we do not develop the metatheory of conditions and coconditions in this paper. Instead, we only present the type checking.
arXiv

Two tricks to trivialize higher-indexed families zhang-2023-twoarXiv · 2023
The conventional general syntax of indexed families in dependent type theories follow the style of “constructors returning a special case”, as in Agda, Lean, Idris, Coq, and probably many other systems. Fording is a method to encode indexed families of this style with index-free inductive types and an identity type. There is another trick that merges interleaved higher inductive-inductive types into a single big family of types. It makes use of a small universe as the index to distinguish the original types. In this paper, we show that these two methods can trivialize some very fancy-looking indexed families with higher inductive indices (which we refer to as higher indexed families).
arXiv

Elegant elaboration with function invocation zhang-2021-elegantarXiv · 2021
We present an elegant design of the core language in a dependently-typed lambda calculus with 𝛿-reduction and an elaboration algorithm.
arXiv
Cites 31 works (3 here)
With notes (3)

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types VezzosiMortbergAbel2019ICFP · 2019
Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.
PDF · DOI · pldb

Type-and-scope safe programs and their proofs allais-2017-typeCPP · 2017
PDF · DOI · pldb

Homotopy Type Theory: Univalent Foundations of Mathematics hottbookarXiv · 2013
Web · arXiv
External (28)
zhang-2021-a reference entries/refs/zhang-2021-a/zhang-2021-a.hel