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.
-}