# Abstract

The **PTS ^{∞}** programming language is a higher-order dependently typed lambda calculus,
an extension of Calculus of Constructions (Coquand, Huet) with the
predicative/impredicative hierarchy of indexed universes.

## Universes

The infinite hierarchy of universes allows to avoid paradoxes (Girard, Russel, Hurkens) in type theory (Martin-Löf).

```
U₀ : U₁ : U₂ : U₃ : …
U₀ — propositions
U₁ — values and sets
U₂ — types
U₃ — sorts
```

## Predicative Universes

All terms obey the **A** ranking inside the sequence of **S** universes,
and the complexity **R** of the dependent term is equal to a maximum of
the term's complexity and its dependency.
The universes system is completely described by the following
PTS notation (due to Barendregt):

```
S (n : nat) = U n
A₁ (n m : nat) = U n : U m where m > n — cumulative
R₁ (m n : nat) = U m ⟶ U n : U (max m n) — predicative
```

Note that predicative universes are incompatible with Church lambda term encoding. You can switch between predicative and impredicative uninverses using typecheker parameter.

## Impredicative Universes

Propositional contractible bottom space is the only available extension to predicative hierarchy that does not lead to inconsistency. However, there is another option to have infinite impredicative hierarchy.

```
A₂ (n : nat) = U n : U (n + 1) — non-cumulative
R₂ (m n : nat) = U m ⟶ U n : U n — impredicative
```

## Single Axiom Language

This language is called one axiom language (or pure) as eliminator and introduction adjoint functors inferred from type formation rule. The only computation rule of Pi type is called beta-reduction.

```
Pi (A: U) (B: A -> U): U = (x: A) -> B x
lambda (A: U) (B: A -> U) (b: Pi A B): Pi A B = \ (x: A) -> b x
app (A: U) (B: A -> U) (f: Pi A B) (a: A): B a = f a
beta (A: U) (B: A -> U) (a:A) (f: Pi A B): Equ (B a) (app A B (lambda A B f) a) (f a) =
```

This language could be embedded in itself and used as Logical Framework for the Pi type:

```
PTS (A: U): U
= (intro: (A -> U) -> U)
* (lambda: (B: A -> U) -> pi A B -> intro B)
* (app: (B: A -> U) -> intro B -> pi A B)
* ((B: A -> U) (f: pi A B) -> (a: A)
-> Path (B a) ((app B (lambda B f)) a) (f a))
```

# Implementation

## Syntax

The terms of PTS^{∞} consist of **nat** indexed stars, variables, applications,
abstractions, and universal quantifications. This language is called Calculus
of Construction and exists in various syntaxes.
PTS^{∞} supports **Morte's** syntax.

```
<> = #option
I = #identifier
U = * < #number >
PTS = U | I | PTS → PTS | ∀ ( I : PTS ) → PTS
| PTS PTS | ( PTS ) | λ ( I : PTS ) → PTS
```

Equivalent HOAS tree encoding for parsed terms is following:

```
data pts (lang: U)
= star (n: nat)
| var (x: name) (l: nat)
| pi (x: name) (l: nat) (f: lang)
| lambda (x: name) (l: nat) (f: lang)
| app (f a: lang)
data PTS
= pure (_: pts PTS)
```

## Universes

```
star (:star,N) -> N
star _ -> (:error, "*")
```

## Functions

```
func ((:forall,),(I,O)) -> true
func T -> (:error,(:forall,T))
```

## Variables

```
var N B -> var N B (proplists:is_defined N B)
var N B true -> true
var N B false -> (:error,("free var",N,proplists:get_keys(B)))
```

## Shift

```
sh (:var,(N,I)),N,P) when I>=P -> (:var,(N,I+1))
sh ((:forall,(N,0)),(I,O)),N,P) -> ((:forall,(N,0)),sh I N P,sh O N P+1)
sh ((:lambda,(N,0)),(I,O)),N,P) -> ((:lambda,(N,0)),sh I N P,sh O N P+1)
sh (Q,(L,R),N,P) -> (Q,sh L N P,sh R N P)
sh (T,N,P) -> T
```

## Substitution

```
sub Term Name Value -> sub Term Name Value 0
sub (:arrow, (I,O)) N V L -> (:arrow, sub I N V L,sub O N V L);
sub ((:forall,(N,0)),(I,O)) N V L -> ((:forall,(N,0)),sub I N V L,sub O N(sh V N 0)L+1)
sub ((:forall,(F,X)),(I,O)) N V L -> ((:forall,(F,X)),sub I N V L,sub O N(sh V F 0)L)
sub ((:lambda,(N,0)),(I,O)) N V L -> ((:lambda,(N,0)),sub I N V L,sub O N(sh V N 0)L+1)
sub ((:lambda,(F,X)),(I,O)) N V L -> ((:lambda,(F,X)),sub I N V L,sub O N(sh V F 0)L)
sub (:app, (F,A)) N V L -> (:app,sub F N V L,sub A N V L)
sub (:var, (N,L)) N V L -> V
sub (:var, (N,I)) N V L when I>L -> (:var,(N,I-1))
sub T _ _ _ -> T.
```

## Normalization

```
norm :none -> :none
norm :any -> :any
norm (:app,(F,A)) -> case norm F of
((:lambda,(N,0)),(I,O)) -> norm (sub O N A)
NF -> (:app,(NF,norm A)) end
norm (:remote,N) -> cache (norm N [])
norm (:arrow, (I,O)) -> ((:forall,("_",0)), (norm I,norm O))
norm ((:forall,(N,0)),(I,O)) -> ((:forall,(N,0)), (norm I,norm O))
norm ((:lambda,(N,0)),(I,O)) -> ((:lambda,(N,0)), (norm I,norm O))
norm T -> T
```

## Definitional Equality

```
eq ((:forall,("_",0)), X) (:arrow,Y) -> eq X Y
eq (:app,(F1,A1)) (:app,(F2,A2)) -> let true = eq F1 F2 in eq A1 A2
eq (:star,N) (:star,N) -> true
eq (:var,(N,I)) (:var,(N,I)) -> true
eq (:remote,N) (:remote,N) -> true
eq ((:farall,(N1,0)),(I1,O1))
((:forall,(N2,0)),(I2,O2)) ->
let true = eq I1 I2 in eq O1 (sub (sh O2 N1 0) N2 (:var,(N1,0)) 0)
eq ((:lambda,(N1,0)),(I1,O1))
((:lambda,(N2,0)),(I2,O2)) ->
let true = eq I1 I2 in eq O1 (sub (sh O2 N1 0) N2 (:var,(N1,0)) 0)
eq (A,B) -> (:error,(:eq,A,B))
```

## Type Checker

```
type (:star,N) _ -> (:star,N+1)
type (:var,(N,I)) D -> let true = var N D in keyget N D I
type (:remote,N) D -> cache type N D
type (:arrow,(I,O)) D -> (:star,h(star(type I D)),star(type O D))
type ((:forall,(N,0)),(I,O)) D -> (:star,h(star(type I D)),star(type O [(N,norm I)|D]))
type ((:lambda,(N,0)),(I,O)) D -> let star (type I D),
NI = norm I in ((:forall,(N,0)),(NI,type O [(N,NI)|D])))
type (:app,(F,A)) D -> let T = type(F,D),
true = func T,
((:forall,(N,0)),(I,O)) = T,
Q = type A D,
true = eq I Q in norm (sub O N A)
```

# USAGE

## Normalization (by Evaluation)

Terms in PTS^{∞} language.

```
$ om show List/Cons
λ (A: *)
→ λ (Head: A)
→ λ (Tail:
∀ (List: *)
→ ∀ (Cons:
∀ (Head: A)
→ ∀ (Tail: List)
→ List)
→ ∀ (Nil: List)
→ List)
→ λ (List: *)
→ λ (Cons:
∀ (Head: A)
→ ∀ (Tail: List)
→ List)
→ λ (Nil: List)
→ Cons Head (Tail List Cons Nil)
```

## Type Erasure

The untyped lambda language O is the simplest language used in
PTS^{∞} to generate backend programs. This O is used as the output of type erasure.

```
I = #identifier
O = I | ( O ) | O O | λ I -> O
```

`Inductive O := Var: nat → O | App: O → O → O | Lambda: nat → O → O → O`

Terms in untyped lambda pure language.

```
$ om print fst erase a "#List/Cons"
( λ Head
→ ( λ Tail
→ ( λ Cons
→ ( λ Nil
→ ((Cons Head) ((Tail Cons) Nil))))))
ok
```

## Extraction

Erlang extracted code O-BEAM. For other targets you may want to read about lazy continuation-passing style O-CPS interpreter (Rust).

```
'Cons'() -> fun (Head) -> fun (Tail) -> fun (Cons) -> fun (Nil) ->
((Cons(Head))((Tail(Cons))(Nil))) end end end end.
```

# Bibliography

[1]. Addendum I: Pure Type System for Erlang

[2]. Some remarks about Dependent Type Theory