Infinity Language

MLTT Extensions

Article

Introduction

The idea of Infinity Langauge came from the needs of unification and arranging different calculuses as extensions to the core of the language with dependent types (or MLTT core). While been working on distributed systems, data storages and stream processing, the core two languages: pi-calculus and stream calculus discovered to be connected and being driven by a language with quantifiers as primitives. So we started to look forward to a unified type checker.

Layered Core

Pure Type System

From the time Coquand at all discovered Calculus of Constructions6, and Barendregt7 systemized its variations, a Pure Type System theory was developed. It is known also as Single Axiom System with only Pi-Type of MLTT2, representing Functional Completeness3.

data O1 = U : nat → O1 | Var: Ident → O1 | App: O1 → O1 → O1 | Lambda: Binder → O1 → O1 → O1 | Arrow: O1 → O1 → O1 | Pi: name → O1 → O1 → O1

1. S.MacLane. Categories for the Working Mathematician
2. P.Martin-Löf. An Intuitionistic Theory of Types. 1972
3. B.Jacobs. Fibrations with indeterminates. 1994
4. W.Lawvere. Conceptual Mathematics. 1997
5. P.Curien. Category theory: a programming language-oriented introduction. 2008
6. T.Coquand. The Calculus of Constructions. 1988
7. H.Barendregt. Lambda Calculus With Types. 2010

Contextual Completness

The basic Core primitive which is needed for proving things is MLTT Sigma-Type, representing Contextual Completeness. This is needed for building Sigma pairs which are curried records. Usually, type checkers called Pi-Sigma provers as it contains PTS enriched with Sigma primitive.

data O2 = O1 | Sigma: name → O2 → O2 → O2 | Pair: O2 → O2 → O2 | Fst: O2 → O2 | Snd: O2 → O2

Identity Types

data O3 = O2 | Id: O3 → O3 → O3 | IdPair: O3 → O3 → O3 | IdJ: O3 → O3 → O3 → O3 → O3 → O3

1. E.Bishop. Foundations of Constructive Analysis. 1967
2. T.Streicher, M.Hofmann. The groupoid interpretation of type theory. 1996
3. G.Barthe, V.Capretta. Setoids in type theory. 2003
4. M.Sozeau. Internalizing Intensional Type Theory 2013
5. V.Voevodsky. Identity types in the C-systems defined by a universe category. 2015
6. D.Selsam,L.de Moura. Congruence Closure in Intensional Type Theory. 2016

(Co)-Inductive Types

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) = empty | tel: name → A → tele A data branch (A: U) = br: name → list name → A data label (A: U) = lab: name → tele A data O4 = O3 | Sum: name → tele → list (label O4) | Split: name → list (branch O4) | Ctor: name → list O4

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.

1. A.Berarducci. Automatic Synthesis of Typed Lambda-Programs. 1985
2. F.Pfenning. Inductively defined types in the CoC. 1989
3. P.Wadler. Recursive types for free. 1990
4. N.Gambino. Wellfounded Trees and Dependent Polynomial Functors. 1995
5. P.Dybjer. Inductive Famalies. 1997
6. B.Jacobs. (Co)Algebras and (Co)Induction. 1997
7. V.Vene. Categorical programming with (co)inductive types
8. 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 computability7.

data O5 = O4 | Path: O5 → O5 → O4 | PathLam: Binder → O5 → O5 → O5 | PathApp: O5 → Formula → O5 → O5 | Comp: O5 → O5 → O5 | Fill: O5 → O5 → O5 | Glue: O5 → O5 → O5 | GlueElem: O5 → O5 → O5 | UnGlueElem: O5 → O5 → O5

1. T.Streicher. A groupoid model refutes UIP. 1994
2. T.Streicher. The Groupoid Interpretation. 1996
3. B.Jacobs. Categorical Logic and Type Theory. 1999
4. S.Awodey. Homotopy Type Theory and Univalent Foundations. 2013
5. S.Huber. A Cubical Type Theory. 2015
6. A.Joyal. What is an elementary higher topos. 2014
7. A.Mortberg. Cubical Type Theory: a constructive univalence axiom. 2017

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.

record PTS: * := (S: ∀ (n: nat) → star n) (A: ∀ (i: nat) → type i (succ i)) (R: ∀ (i: nat) → ∀ (j: nat) → pi i j (max i j))