Natural Encoding of the Inner Space

Dependent λ Calculus /w Infinite Universes

Untyped lambda calculus was discovered as an inner language of the space at origin. Minimal language is well described in LISP systax with named set of inductive type constructors such as Church numerals and list cons. Main constructions of this languages are: cons, nil, eq, atom, car, cdr, lambda, apply and id. Erlang is a form of this language extended with effects, mainly process calculus axioms, and usually untyped lambda calculus is used as a target extract language.

O := I | λ I → O | O O

Functorial

Another breakdown of inner space language was ML language, founded merely on algebraic datatypes and algebra on higher terms rather than categorical semantic. Lately it was fixed with categorical methods in Charity and CPL.

O := ∅ | ( O ) |
□ | ∀ ( I : O ) → O |
* | λ ( I : O ) → O |
I | O → O | O O

CoC

More closely to pure inner space language came the Lean prover, as it has in its core almost pure CoC language with predicative universes and macro extensions. Another languages has additional axioms, thus extending the efforts needed for metacircular interpreter and reasoning about core. We want to design language, where encoding of inductive types is based on categorical semantic of compilation to CoC. All other syntax constructions are inductive definitions, plugged into the stream parser. AST of the CoC language is also defined in terms of inductive constructions and thus allowed in the macros. Really, the language of polynomial functors (data and record) and core language of the process calculus (spawn, receive and send) are just macrosystem over CoC language, its syntax extensions.

In pure CoC we have only arrows, so all inductive type encodings would be Church-encoding variations. Most extended nowadays is Church-Boehm-Berrarducci encoding, which dedicated to inductive types. Another well known are Scott and Parigot encodings.

Exe CoC Macro Language

There was modeled a math model of encoding, which calculate (co)limits in a given cathegory, finding (co)initial objects, an inductive types. Will call such encoding in honour of Lambek lemma that leeds us to the equality of initial object in category of algebras of inductive constructors. Such encoding works with dependent types and its consistency is proved in Lean model.

I := #identifier

O := ∅ | ( O ) |
□ | ∀ ( I : O ) → O |
* | λ ( I : O ) → O |
I | O → O | O O

L := ∅ | L I

A := ∅ | A ( L : O ) | A O

F := ∅ | F ( I : O ) | ()

P := I O , P | I O

E := ∅ | E data L : A := F
| E record L : A [ extend P ] := F
| E let F in O
| E case O [ | I O -> O ]
| E receive O [ | I O -> O ]
| E spawn O raise L := O
| E send O to O