1. History of Type Systems
The history of Type Theory take its root MLTT paper 1. The the Type Theory was fixed with Id types, W, Nat, List types were added 2. The type checker of single axiom system with Pi types only was given in CoC paper 3.
. P.Martin-Löf. An Intuitionistic Theory of Types, 1972. . P.Martin-Löf. Intuitionistic Type Theory, 1984. . T.Coquand. The Calculus of Constructions, 1988. . T.Streicher. The Groupoid Interpretation of Type Theory, 1996. . H.Barendregt. Lambda Calculus With Types, 2010. . S.Awodey et all. Homotopy Type Theory, 2014. . A.Mortberg. Cubical Type Theory, 2017.
Then Voevodsky presented HTS without a computational semantics of univalence axiom. This later was fixed by Mortberg et all in cubicaltt.
The 10 lines BNF declares syntax that covers: 1) MLTT as pi, sigma and path types; 2) inductive types case analisys; and 3) simple module system. This system is enough to encode core cubical base library.
0 := #empty brs := 0 + cobrs app := exp exp id := [ #nat ] ids := [ id ] codec := def dec dec := 0 + codec
imp := [ import id ] tele := 0 + cotele cotele := ( exp : exp ) tele sum := 0 + id tele + id tele | sum br := ids -> exp mod := module id where imp def cobrs := | br brs
def := data id tele = sum + id tele : exp = exp + id tele : exp where def exp := cotele * exp + cotele -> exp + exp -> exp + app + ( exp ) + id + split cobrs + exp.1 + exp.2 + \ cotele -> exp
The idea of Infinity Langauge is a unified layered type checker. We select 5 levels of type checker awareness from pure type systems up to homotopy calculus.
data lang = PTS (_: pts) | SIGMA (_: exists) | ID (_: identity) | INDUCTION (_: ind) | HTS (_: hts)
Dependent Type Theory
data pts = star (n: nat) | var (x: name) (l: nat) | pi (x: name) (l: nat) (d c: lang) | lambda (x: name) (l: nat) (d c: lang) | app (f a: lang)
data exists = sigma (n: name) (a b: lang) | pair (a b: lang) | fst (p: lang) | snd (p: lang)
The categorical methods for lambda calculus and category theory in general could be found in the following works:
. S.MacLane. Categories for the Working Mathematician. . W.Lawvere. Conceptual Mathematics, 1997. . B.Jacobs. Fibrations with indeterminates, 1994. . P.Curien. Category theory: a programming language-oriented introduction, 2008.
Categories with Families is a categorical semantics of dependent type theory that nowadays formulated as cubical sets or as presheaf model of type theory.
. P.Dybjer. The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories -- an Intuitionistic Perspective. . P.Clairambault. From Categories with Families to Locally Cartesian Closed Categories. . P.Dybjer. On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. . R.A.G.Seely. Locally cartesian closed categories and type theory. . M.Hofmann. Revisiting the categorical interpretation of dependent type theory. . S.Castellan. Dependent type theory as the initial category with families. . P.Dybjer. Internal Type Theory. . V.Voevodsky. A C-system defined by a universe category.
data identity = id (a b: lang) | idpair (a b: lang) | idelim (a b c d e: lang)
. E.Bishop. Foundations of Constructive Analysis, 1967. . B.Nordström. Programming in Martin-Löf’s Type Theory. . B.Jacobs. Structural induction and coinduction in a fibrational setting, 1997. . G.Barthe, V.Capretta. Setoids in type theory, 2003. . M.Sozeau. Internalizing Intensional Type Theory, 2013. . V.Voevodsky. Identity types in the C-systems defined by a universe category, 2015. . L.de Moura. Congruence Closure in Intensional Type Theory, 2016.
The further development of induction5 inside MLTT provers led to the theory of polynomial functors and well-founded trees4, known in programming languages as inductive types with data and record core primitives of type checker. In fact recursive inductive types3 could be encoded in PTS using non-recursive representation Berarducci1 or Categorical6 encoding.
data tele (A: U) = emp | tel (n: name) (b: A) (t: tele A) data branch (A: U) = br (n: name) (args: list name) (term: A) data label (A: U) = lab (n: name) (t: tele A) data ind = data_ (n: name) (t: tele lang) (labels: list (label lang)) | case (n: name) (t: lang) (branches: list (branch lang)) | ctor (n: name) (args: list lang)
The non-well-founded trees or infinite coinductive trees6,8 are useful for modeling infinite process running which is part of Milner's Pi-calculus. Coinductive streams are part of any MLTT base library.
. A.Berarducci. Automatic Synthesis of Typed Lambda-Programs, 1985. . F.Pfenning. Inductively defined types in the CoC, 1989. . P.Wadler. Recursive types for free, 1990. . N.Gambino. Wellfounded Trees and Dependent Polynomial Functors, 1995. . P.Dybjer. Inductive Famalies, 1997. . B.Jacobs. (Co)Algebras and (Co)Induction, 1997. . V.Vene. Categorical programming with (co)inductive types. . H.Geuvers. Dependent (Co)Inductive Types are Fibrational Dialgebras, 2015.
Higher Inductive Types
The fundamental development of equality inside MLTT provers led us to the notion of ∞-groupoid2 as spaces. In this was Path identity type appeared in the core of type checker along with de Morgan algebra on built-in interval type. Glue, unglue composition and fill operations are also needed in the core for the univalence computability8.
data hts = path (a b: lang) | path_lam (n: name) (a b: lang) | path_app (f: name) (a b: lang) | comp_ (a b: lang) | fill_ (a b c: lang) | glue_ (a b c: lang) | glue_elem (a b: lang) | unglue_elem (a b: lang)
. T.Streicher. A groupoid model refutes UIP, 1994. . B.Jacobs. Categorical Logic and Type Theory, 1999. . S.Awodey. Homotopy Type Theory and Univalent Foundations, 2013. . S.Huber. A Cubical Type Theory, 2015. . A.Joyal. What is an elementary higher topos, 2014. . M.Shulman. Univalent Categories and the Rezk Completion, 2014. . A.Mortberg. Cubical Type Theory: a constructive univalence axiom, 2017.
The universe system is completely described by the PTS SAR notation, given by Barendregt. Find more info in Axioms and Inference Rules of underlying Om intermediate language.
PTS : U = (S: (n: nat) -> star n) (A: (i: nat) -> type i (succ i)) (R: (i j: nat) -> pi i j (max i j)) * unit