Homotopy Type System

The minimal core of HoTT computability

SYNOPSIS

The history of Type Theory takes its root from MLTT paper 1. Then the Type Theory was fixed for Predicative Universes with Id types, and W, Nat, List types were added 2. The type checker of single axiom system with Pi types only is given in the CoC paper 3.

Then Voevodsky presented HTS with strict Id and homotopical Path types, but without its computational semantics. This later was fixed by Mortberg et all in cubicaltt and Sterling et all in redtt.

Groupoid Infinity is doing research in type theory, model encodings, programs extraction and formalization of mathematics. We believe in high performance certified virtual machines, where certified programs extracted from provers should run on. We also want to use group theory and homotopy theory for proving properties about these programs.

The Erlang language as target extract was chosen not only as example of simple bootstrap on foreign platform, but also because this tool is most known to author and he naively believes that Erlang deserves not only homotopy typechecker in its platform, but type erasure and term extraction as well.

$ ./homotopy CTT-CCHM Homotopy Type System 1.3.1 Usage := homotopy Args Args := Command | Command Args Command := parse | lex | read | fst | snd | file

SYNTAX

The 10 BNF definitions declare syntax that covers: 1) MLTT as pi, sigma and path types; 2) inductive types case analysis; and 3) simple module system. This system is enough to encode core cubical base library.

Module system.

mod := 'module' id 'where' imp dec imp := '$empty' imp := skip imp imp := 'import' id imp

The module system is present in all intermediate languages: PTS, MLTT, HTS. During compilation programs in these languages are being desugared to untyped lambda interpreter called CPS (continuation passing style certified interpreter) that incorporates intercore protocol IP between interpreter instances that are running at processor cores. While CPS could be seen as desugared run-time target of dependently typed lambda calculus or MLTT-based systems, the IP could be seen us untyped desugared run-time target of process calculus or linear type systems (LTS).

The sequence of variables, parsed as application fold.

ids := '$empty' ids := id ids

Telescopes.

tele := '$empty' tele := cotele cotele := '(' exp ':' exp ')' tele

Top-level inductive data and function definitions.

codec := def skip dec codec := def dec dec := '$empty' dec := codec def := 'data' id tele '=' sum def := id tele ':' exp '=' exp def := id tele ':' exp '=' exp 'where' def

Inductive and HIT introductions.

sum := '$empty' sum := rsum rsum := id tele rsum := id tele '|' rsum rsum := id tele '<' ids '>' sys rsum := id tele '<' ids '>' sys '|' rsum

Inductive and HIT eliminators.

cobrs := '|' br brs brs := '$empty' brs := cobrs br := ids arrow exp br := ids '@' ids arrow exp

Lambda and Path applications.

app := exp exp papp := exp '@' formula

Expressions.

exp := 'split' cobrs exp := id exp := id '{' exp '}' exp := '<' ids '>' exp exp := exp '.1' exp := exp '.2' exp := lam cotele arrow exp exp := cotele arrow exp exp := exp arrow exp exp := cotele '*' exp exp := 'comp' exp exp sys exp := 'fill' exp exp sys exp := 'glue' exp sys exp := 'unglue' exp sys exp := exp ',' exp exp := papp exp := '(' exp ')' exp := app

Cubical homogeneous composition system.

sys := '[' sides ']' sides := '$empty' sides := side sides := side ',' sides side := '(' id '=' id ')' arrow exp

CCHM connections (meet and join).

formula := formula forall f1 formula := f1 formula := f2 f1 := f1 meet f2 f1 := f2 f2 := '-' f2 f2 := id

SEMANTICS

The idea of MLTT is a unified layered type checker. We selected 5 levels of type checker awareness from pure type systems up to homotopy calculus HTS. Each layer corresponds to its presheaf.

Definition (Type). A type is interpreted as a presheaf $A$, a family of sets $A_I$ with restriction maps $u \mapsto u\ f, A_I \rightarrow A_J$ for $f: J\rightarrow I$. A dependent type B on A is interpreted by a presheaf on category of elements of $A$: the objects are pairs $(I,u)$ with $u : A_I$ and morphisms $f: (J,v) \rightarrow (I,u)$ are maps $f : J \rightarrow$ such that $v = u\ f$. A dependent type B is thus given by a family of sets $B(I,u)$ and restriction maps $B(I,u) \rightarrow B(J,u\ f)$.

We think of $A$ as a type and $B$ as a family of presheves $B(x)$ varying $x:A$. The operation $\Pi(x:A)B(x)$ generalizes the semantics of implication in a Kripke model.

data lang = PTS (_: pts) | SIGMA (_: exists) | PATH (_: path) | HIT (_: ind) | COMP (_: hts)

Dependent Types

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)

Defintion (Pi). An element $w:[\Pi(x:A)B(x)](I)$ is a family of functions $w_f : \Pi(u:A(J))B(J,u)$ for $f : J \rightarrow I$ such that $(w_f u)g=w_{f\ g}(u\ g)$ when $u:A(J)$ and $g:K\rightarrow J$.

Defintion (Sigma). The set $\Sigma(x:A)B(x)$ is the set of pairs $(u,v)$ when $u:A(I),v:B(I,u)$ and restriction map $(u,v)\ f=(u\ f,v\ f)$.

Path Types

The fundamental development of equality inside MLTT provers led us to the notion of ∞-groupoid as spaces. In this way 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 computability and coherence.

data path (a b: lang) | path_lam (n: name) (a b: lang) | path_app (f: name) (a b: lang)

Definition (Cubical Presheaf $\mathbb{I}$). The identity types modeled with another presheaf, the presheaf on Lawvere category of distributive lattices (theory of de Morgan algebras) denoted with $\Box$ — $\mathbb{I} : \Box^{op} \rightarrow \mathrm{Set}$.

Properties of $\mathbb{I}$. The presheaf $\mathbb{I}$: i) has to distinct global elements $0$ and $1$ (B$_1$); ii) $\mathbb{I}$(I) has a decidable equality for each $I$ (B$_2$); iii) $\mathbb{I}$ is tiny so the path functor $X \mapsto X^\mathbb{I}$ has right adjoint (B$_3$).; iv) $\mathbb{I}$ has meet and join (connections).

Higher Inductive Types

The further development of induction inside MLTT provers led to the theory of polynomial functors and well-founded trees, known in programming languages as inductive types with data and record core primitives of type checker. In fact, recursive inductive types could be encoded in PTS using non-recursive representation of Bohm-Berarducci schemes or Categorical Impredicative encoding by Steve Awodey.

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 = intro (n: name) (t: tele lang) (labels: list (label lang)) | case (n: name) (t: lang) (branches: list (branch lang)) | ctor (n: name) (args: list lang) | htor (n: name) (args: list lang) (ids: list lang) (sys: lang)

The non-well-founded trees or infinite coinductive trees are useful for modeling infinite processes and are part of Milner's Pi-calculus. Coinductive streams could be found in many MLTT base libraries.

Partial Elements and Structured Types

HIT Composition structure.

data structure = comp_ (a b: lang) | fill_ (a b c: lang)

Glue Types

Glue Types are needed to prove univalence.

data ua = glue_ (a b c: lang) | glue_intro (a b: lang) | unglue_elim (a b: lang)

Universes

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

Bibliography

Issue I: Internalizing MLTT

MLTT and PTS

[1]. P. Martin-Löf and G. Sambin, The Theory of Types. Studies in proof theory, 1972. [2]. P. Martin-Löf and G. Sambin, Intuitionistic type theory. Studies in proof theory, Bibliopolis, 1984. [3]. T. Coquand and G. Huet, “The calculus of constructions,” in Information and Computation, (Duluth, MN, USA), pp. 95–120, Academic Press, Inc., 1988. [4]. M. Hofmann and T. Streicher, “The groupoid interpretation of type theory,” in In Venice Festschrift, pp. 83–111, Oxford University Press, 1996. [5]. H. P. Barendregt, “Lambda calculi with types,” in Handbook of Logic in Computer Science (Vol. 2) (S. Abramsky, D. M. Gabbay, and S. E. Maibaum, eds.), (New York, NY, USA), pp. 117–309, Oxford University Press, Inc., 1992. [6]. S. P. Jones and E. Meijer, “Henk: A typed intermediate language,” in In Proc. First Int’l Workshop on Types in Compilation, 1997.

Categorical Methods

[10]. C. Hermida and B. Jacobs, “Fibrations with indeterminates: Contextual and functional completeness for polymorphic lambda calculi,” Mathematical Structures in Computer Science, vol. 5, pp. 501–531, 1995. [11]. P.-L. Curien, “Category theory: a programming language-oriented introduction,” 2008. [12]. S. MacLane, Categories for the Working Mathematician. New York: Springer-Verlag, 1971. Graduate Texts in Mathematics, Vol. 5. [13]. F. Lawvere and S. Schanuel, Conceptual Mathematics: A First Introduction to Categories. Cambridge University Press, 2009.

Categorical Models of Type Theory

[20]. A. Buisse and P. Dybjer, “The interpretation of intuitionistic type theory in locally cartesian closed categories – an intuitionistic perspective,” Electron. Notes Theor. Comput. Sci., vol. 218, pp. 21–32, Oct. 2008. [21]. P. Clairambault, “From categories with families to locally cartesian closed categories,” [22]. A. Abel, T. Coquand, and P. Dybjer, “On the algebraic foundation of proof assistants for intuitionistic type theory,” in Functional and Logic Programming (J. Garrigue and M. V. Hermenegildo, eds.), (Berlin, Heidelberg), pp. 3–13, Springer Berlin Heidelberg, 2008. [23]. R. A. Seely, “Locally cartesian closed categories and type theory,” in Mathematical proceedings of the Cambridge philosophical society, vol. 95, pp. 33–48, Cambridge University Press, 1984. [24]. P.-L. Curien, R. Garner, and M. Hofmann, “Revisiting the categorical interpretation of dependent type theory,” Theoretical Computer Science, vol. 546, pp. 99–119, 2014. [25]. S. Castellan, “Dependent type theory as the initial category with families,” Internship Report, 2014. [26]. V. Voevodsky, “A c-system defined by a universe in a category,” 2014. [27]. P. Dybjer, “Internal type theory,” in International Workshop on Types for Proofs and Programs, pp. 120–134, Springer, 1995.

Identity Types

[30]. E. Bishop, Foundations of constructive analysis. 1967. [31]. B.Nordström, K.Petersson, and J.M.Smith, Programming in Martin-Löf’s type theory, vol. 200. Oxford University Press Oxford, 1990. [32]. C. Hermida and B. Jacobs, “Structural induction and coinduction in a fibrational setting,” Information and computation, vol. 145, no. 2, pp. 107–152, 1998. [33]. G. Barthe, V. Capretta, and O. Pons, “Setoids in type theory,” 2000. [34]. V. Voevodsky, “A c-system defined by a universe category,” Theory Appl. Categ, vol. 30, no. 37, pp. 1181–1215, 2015. [35]. M. Sozeau and N. Tabareau, “Internalizing intensional type theory,” [36]. D. Selsam and L. de Moura, “Congruence closure in intensional type theory,” in International Joint Conference on Automated Reasoning, pp. 99–115, Springer, 2016.

Inductive Types

[40]. C. Böhm and A. Berarducci, “Automatic synthesis of typed lambda- programs on term algebras,” in Theoretical Computer Science, vol. 39, pp. 135–154, 1985. [41]. F. Pfenning and C. Paulin-Mohring, “Inductively defined types in the calculus of constructions,” in Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29 - April 1, 1989, Proceedings, pp. 209–228, 1989. [42]. P. Wadler in Recursive types for free, manuscript, 1990.N. Gambino and M. Hyland, “Wellfounded trees and dependent polynomial functors,” in International Workshop on Types for Proofs and Programs, pp. 210–225, Springer, 2003. [43].N. Gambino and M. Hyland, “Wellfounded trees and dependent polynomial functors,” in International Workshop on Types for Proofs and Programs, pp. 210–225, Springer, 2003. [44]. P. Dybjer in Inductive families, vol. 6, pp. 440–465, Springer, 1994. [45]. B. Jacobs and J. Rutten in A tutorial on (co) algebras and (co) induction, vol. 62, pp. 222–259, EUROPEAN ASSOCIATION FOR THEORETICAL COMPUTER, 1997. [46]. V. Vene, Categorical programming with inductive and coinductive types. Tartu University Press, 2000. [47]. H. Basold and H. Geuvers, “Type theory based on dependent inductive and coinductive types,” in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 327–336, ACM, 2016.

Higher Inductive Types

[50]. M. Hofmann and T. Streicher, “The groupoid model refutes uniqueness of identity proofs,” in Logic in Computer Science, 1994. LICS’94. Proceedings., Symposium on, pp. 208–212, IEEE, 1994. [51]. B. Jacobs, Categorical logic and type theory, vol. 141. Elsevier, 1999. [52]. A. Joyal, “Categorical homotopy type theory,” Slides from a talk at MIT dated, vol. 17, 2014. [53]. T. Coquand, P. Martin-Löf, V. Voevodsky, A. Joyal, A. Bauer, S. Awodey, M. Sozeau, M. Shulman, D. Licata, Y. Bertot, P. Dybjer, and N. Gambino, Homotopy Type Theory: Univalent Foundations of Mathematics. 2013. [54]. C. Cohen, T. Coquand, S. Huber, and A. Mörtberg in Cubical Type Theory: a constructive interpretation of the univalence axiom, vol. abs/1611.02108, 2017. [55]. B. Ahrens, K. Kapulkin, and M. Shulman, “Univalent categories and the rezk completion,” in Extended Abstracts Fall 2013 (M. d. M. González, P. C. Yang, N. Gambino, and J. Kock, eds.), (Cham), pp. 75– 76, Springer International Publishing, 2015. [56]. I. Orton and A. M. Pitts, “Axioms for modelling cubical type theory in a topos,” arXiv preprint arXiv:1712.04864, 2017. [57]. S. Huber, “Cubical intepretations of type theory,” 2016. [58]. S. Huber, “Canonicity for cubical type theory,” Journal of Automated Reasoning, pp. 1–38, 2017. [59]. C. Angiuli, R. Harper, and T. Wilson, “Computational higher type theory i: Abstract cubical realizability,” arXiv preprint arXiv:1604.08873, 2016. [60]. C. Angiuli and R. Harper, “Computational higher type theory ii: Dependent cubical realizability,” arXiv preprint arXiv:1606.09638, 2016. [61]. T.Coquand, S.Huber, and A.Mörtberg , “On Higher Inductive Types in Cubical Type Theory”, arXiv preprint arXiv:1802.01170, 2018.