Cubical Language

Design and Implementation

Abstract

1. Genesis of Type Systems

The history of Type Theory takes its root from MLTT paper 1. The 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.

[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.

Then Voevodsky presented HTS with Univalence Axiom, but without its computational semantics. This later was fixed by Mortberg et all in cubicaltt and Harper et all in RedPRL.

Cubical Syntax

The 10 lines BNF declares 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.

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

Infinity Language

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 following works:

[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.

Contextual Categories

Categories with Families is a categorical semantics of dependent type theory that nowadays is formulated as cubical sets or as presheaf model 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

data identity = id (a b: lang) | idpair (a b: lang) | idelim (a b c d e: lang)

[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

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 = 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 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.

[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

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 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)

[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.

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