# Definition

## Universes

The **OM** language is a higher-order dependently typed lambda calculus,
an extension of Coquand's Calculus of Constructions
with the predicative/impredicative hierarchy of indexed universes.
This extension is motivated avoiding paradoxes in dependent theory.
Also there is no fixpoint axiom needed for the definition
of infinity term dependance.

```
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 predicative vs impredicative uninverses by typecheker parameter.

## Impredicative Universes

Propositional contractible bottom space is the only available extension to predicative hierarchy that not leads 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 langauge 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.

```
∀ (x: A) → B x : Type — formation rule
λ (x: A) → b : B x — introduction
f a : B [a/x] — elimination
(λ (x: A) → b) a = b [a/x] : B [a/x] — equation
```

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

```
Record Pi (A: Type) :=
intro: (A → Type) → Type
lambda: (B: A → Type) → ∀ (a: A) → B a → intro B
app: (B: A → Type) → intro B → ∀ (a: A) → B a
app-lam (B: A → Type) (f: ∀ (a: A) → B a): ∀ (a: A) → app (fun f) a ==> f a
lam-app (B: A → Type) (p: intro B): fun (λ (a: A) → app p a) ==> p.
```

## Syntax

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

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

Equivalent tree encoding for parsed terms is following:

```
Inductive OM := Star: nat → OM
| Var: name → OM
| App: OM → OM → OM
| Lambda: name → OM → OM → OM
| Arrow: OM → OM → OM
| Pi: name → OM → OM → OM.
```

## Typechecker

The typechecker is structural recursive function over OM terms. It lookups variables from the context.

```
Definition star(t: OM): nat :=
match t
| Star n => n
| _ => error "star"
Fixpoint type (t: OM, c: Context): OM :=
match t
| Pi n 0 i o => Star max (star (type i c))
(star (type o [(n,norm i)|c]))
| Arrow i o => Star max (star (type i c))
(star (type o c))
| Lambda n 0 i o => let _ = star (type i c) in
let ni = norm i in
Pi n 0 ni (type O [(n,ni)|c])
| App f a => match type f c
| Pi n 0 i o => let _ = eq i (type a c)
in norm (subst o n a)
| _ => error "app"
| Var n => match get c n
| Some x => x
| None => error "var"
| Star n => Star n + 1
```

# Passes

## Normalized

Terms in OM 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)
```

## Extract Language

The untyped lambda language O is the simplest language used in OM 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.
```

## Erased

Terms in untyped lambda pure language.

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

Erlang extracted code. For other targets you may want to read Code Extract notes.

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