Pure Type System

The minimal language with universal quantifier and infinity number of universes for consistent typechecking and normalization

Abstract

The PTS programming 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.

Universes

The infinite hierarchy of universes allows to avoid paradoxes in type theory.

U₀ : U₁ : U₂ : U₃ : … U₀ — propositions U₁ — values and sets U₂ — types U₃ — sorts
\begin{equation} \tag{S} \dfrac {o : Nat} {Type_o} \end{equation}

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.

$$ \begin{equation} \tag{A₁} \dfrac {i: Nat,\ \ \ \ j: Nat,\ \ \ \ i < j} {Type_i : Type_{j}} \end{equation} $$
$$ \begin{equation} \tag{R₁} \dfrac {i : Nat,\ \ \ \ j : Nat} {Type_i \rightarrow Type_{j} : Type_{max(i,j)}} \end{equation} $$

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
$$ \begin{equation} \tag{A₂} \dfrac {i: Nat} {Type_i : Type_{i+1}} \end{equation} $$
$$ \begin{equation} \tag{R₂} \dfrac {i : Nat,\ \ \ \ j : Nat} {Type_i \rightarrow Type_{j} : Type_{j}} \end{equation} $$

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) =
\begin{equation} \tag{$\Pi$-formation} \dfrac {x:A \vdash B : Type} {\Pi\ (x:A) \rightarrow B : Type} \end{equation}
\begin{equation} \tag{$\lambda$-intro} \dfrac {x:A \vdash b : B} {\lambda\ (x:A) \rightarrow b : \Pi\ (x: A) \rightarrow B } \end{equation}

$$ \begin{equation} \tag{$App$-elim} \dfrac {f: (\Pi\ (x:A) \rightarrow B)\ \ \ a: A} {f\ a : B\ [a/x]} \end{equation} $$
$$ \begin{equation} \tag{$\beta$-comp} \dfrac {x:A \vdash b: B\ \ \ a:A} {(\lambda\ (x:A) \rightarrow b)\ a = b\ [a/x] : B\ [a/x]} \end{equation} $$

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 = ppure (_: 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. 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.

Bibliography

Addendum I: Pure Type System for Erlang