Pure Type System
The OM language is a dependently typed lambda calculus, an extension of Barendregt' and Coquand Calculus of Constructions with the predicative 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
Axioms and Inference Rules
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 type 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
Impredicative Propositional Universe
Propositional contractible bottom space is impredicative by term dependance.
A₂ (n : nat) = U n : U (n + 1) — non-cumulative R₂ (m n : nat) = U m ⟶ U n : U n — impredicative
Type System a la Martin-Löf
This langauge is called one axiom language as it reduction rule is inferred from type formation axiom along with eliminator and introduction adjoint functors.
∀ (x: A) → B x : Type — formation rule λ (x: A) → b : B x — introduction f a : B x — elimination (λ (a: A) → b) a = b [p/a] : B 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.
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).
type (Star n) D : Star n + 1 type (Var n) D : let _ = isVar n D in nth (i + 1) (all n D) type (Arrow i o) D : Star max (star (type i D)) (star (type o D)) type (Pi n 0 i o) D : Star max (star (type i D)) (star (type o [(n norm i)|D])) type (Lambda n 0 i o) D : let _ = star (type i D) in let ni = norm i in Pi n 0 ni (type O [(n ni)|D]) type (App f a) D : let t = type f D in let _ = isFun t in match t | Pi n 0 i o => let _ = eq i (type a D) in norm (subst o n a)
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)
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).
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.