module ArithExprTypeSystem where {- We shall now define the typing relation for arithmetic expressions. So first we define the whole set of arithmetic expressions, not just the boolean expressions: -} data Expr : Set where true false : Expr if_then_else_ : Expr -> Expr -> Expr -> Expr zero : Expr succ pred iszero : Expr -> Expr {- We then define the set of types with only two inhabitants: -} data Type : Set where bool nat : Type {- Now we can define the typing relation as a data type with one constructor for each typing rule: -} infix 10 _∈_ data _∈_ : Expr -> Type -> Set where true : true ∈ bool false : false ∈ bool if_then_else_ : {T : Type} → {t1 t2 t3 : Expr} → t1 ∈ bool → t2 ∈ T → t3 ∈ T → if t1 then t2 else t3 ∈ T zero : zero ∈ nat succ : ∀ {t : Expr} → t ∈ nat → succ t ∈ nat pred : ∀ {t : Expr} → t ∈ nat → pred t ∈ nat iszero : ∀ {t : Expr} → t ∈ nat → iszero t ∈ bool {- The types t ∈ T are typing statements (typing judgments). The elements of these types der : t ∈ T can be thought of as typing derivations, that is, trees of inferences. Types such as t ∈ T are "propositions" and elements of such propositions are often called "proof objects". We can now formulate, and will later be able to prove, important theorems about typing, such as progress : ∀ {t T} → t ∈ T → Value t ∨ (∃ \ t' → t ⇒ t') and preservation : ∀ {T t t'} → t ∈ T → t ⇒ t' → t' ∈ T Cf Pierce. -}