{-
Computer Aided Formal Reasoning (G53CFR, G54CFR)
Thorsten Altenkirch
Lecture 13: Evaluator and type checker
In this lecture we investigate an evaluator for a simple language of
expressions over natural numbers and booleans. We first implement an
untyped evaluator (which may fail and is slow) and then an evaluator
for a typed language which will always succeed and is faster. To go
from an untyped expression to a typed expression we implement a type
checker. The type checker may also fail but this is early (before
evaluation) and doesn't affect the efficiency of evaluations.
-}
module l13 where
open import Data.Nat
open import Data.Bool
open import Data.Maybe
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
{- an untyped language of expressions -}
infix 3 _≤E_
infix 4 _+E_
data Expr : Set where
nat : ℕ → Expr
bool : Bool → Expr
_+E_ : Expr → Expr → Expr
_≤E_ : Expr → Expr → Expr
ifE_then_else_ : Expr → Expr → Expr → Expr
{- Examples of expressions: -}
e1 : Expr -- if 3 ≤ 4 then 4 + 1 else 0
e1 = ifE (nat 3) ≤E (nat 4) then (nat 4) +E (nat 1) else (nat 0)
e2 : Expr -- 3 ≤ 4 + 5
e2 = (nat 3) ≤E (nat 4) +E (nat 5)
e3 : Expr -- (3 ≤ 4) + 5
e3 = ((nat 3) ≤E (nat 4)) +E (nat 5)
{- The result of evaluating an expression is a value -}
data Val : Set where
nat : ℕ → Val
bool : Bool → Val
{- To accomodate errors we introduce the Maybe monad.
A Monad M is an operation on Sets such that M A is the type of
computations over A. In the case of Maybe a computation is
something that may go wrong (i.e. returns nothing).
Each monad comes with two functions:
return : {A : Set} → A → M A
turns a value into a (trivial) computation.
_>>=_ : {A B : Set} → M A → (A → M B) → M B
(bind) m >>= f runs first the computation m and if it returns a
value runs f in it. The effects are a combination of running both
computations.
-}
-- for Maybe return is just (no error)
return : {A : Set} → A → Maybe A
return a = just a
infix 2 _>>=_
-- bind does error propagation
_>>=_ : {A B : Set} → Maybe A → (A → Maybe B) → Maybe B
just a >>= f = f a
nothing >>= f = nothing
{- To implement the evaluator we implement some convenience
functions. -}
{- Addition of two values has to check wether the values are indeed
numbers -}
_+v_ : Val → Val → Maybe Val
nat m +v nat n = return (nat (m + n))
_ +v _ = nothing
{- dec2bool coerces decidability into bool by forgetting the
evidence. -}
dec2bool : {A : Set} → Dec A → Bool
dec2bool (yes p) = true
dec2bool (no ¬p) = false
{- This is used to implement ≤ for values. As +v this has to check
wether the arguments are numbers. -}
_≤v_ : Val → Val → Maybe Val
nat m ≤v nat n = return (bool (dec2bool (m ≤? n)))
_ ≤v _ = nothing
{- if-then-else for values. May return an error if the first argument
is not a boolean.
-}
ifV_then_else_ : Val → Val → Val → Maybe Val
ifV bool b then v else v' = return (if b then v else v')
ifV _ then _ else _ = nothing
{- The evaluator. We use Scott-brackets (⟦ = \[[, ⟧ = \]]) as it is
tradition to mark the borderline between syntax and semantics.
Evlauation an expression may return a value of fail. -}
⟦_⟧ : Expr → Maybe Val
⟦ nat n ⟧ = return (nat n)
⟦ bool b ⟧ = return (bool b)
⟦ e +E e' ⟧ = ⟦ e ⟧ >>= λ v →
⟦ e' ⟧ >>= λ v' →
v +v v'
{- In Haskell we would use "do" syntax:
do v <- ⟦ e ⟧
v' <- ⟦ e' ⟧
v +v v'
-}
⟦ e ≤E e' ⟧ = ⟦ e ⟧ >>= λ v →
⟦ e' ⟧ >>= λ v' →
v ≤v v'
⟦ ifE e then e' else e'' ⟧ = ⟦ e ⟧ >>= λ v →
⟦ e' ⟧ >>= λ v' →
⟦ e'' ⟧ >>= λ v'' →
ifV v then v' else v''
{- Evaluation the examples: -}
v1 : Maybe Val -- just (nat 5)
v1 = ⟦ e1 ⟧
v2 : Maybe Val -- just (bool true)
v2 = ⟦ e2 ⟧
v3 : Maybe Val
v3 = ⟦ e3 ⟧ -- nothing
{- We do everything again but this time for a typed language. -}
{- the types -}
data Ty : Set where
nat : Ty
bool : Ty
{- typed values -}
data TVal : Ty → Set where
nat : ℕ → TVal nat
bool : Bool → TVal bool
{- typed expressions -}
data TExpr : Ty → Set where
nat : ℕ → TExpr nat
bool : Bool → TExpr bool
_+E_ : TExpr nat → TExpr nat → TExpr nat
_≤E_ : TExpr nat → TExpr nat → TExpr bool
ifE_then_else_ : {σ : Ty} → TExpr bool → TExpr σ → TExpr σ → TExpr σ
{- the typed evaluator
doesn't need to use the Maybe monad because it will never fail. -}
⟦_⟧T : {σ : Ty} → TExpr σ → TVal σ
⟦ nat n ⟧T = nat n
⟦ bool b ⟧T = bool b
⟦ e +E e' ⟧T with ⟦ e ⟧T | ⟦ e' ⟧T
... | nat m | nat n = nat (m + n)
⟦ e ≤E e' ⟧T with ⟦ e ⟧T | ⟦ e' ⟧T
... | nat m | nat n = bool (dec2bool (m ≤? n))
⟦ ifE e then e' else e'' ⟧T with ⟦ e ⟧T
... | bool b = if b then ⟦ e' ⟧T else ⟦ e'' ⟧T
{- But what to do if just have got an untyped expression (maybe read
from a file)? We use a type checker to lift an untyped expression
to an equivalent typed expression (or fail).
-}
{- A forgetful map from typed expressions to untyped expressions -}
⌊_⌋ : {σ : Ty} → TExpr σ → Expr
⌊ nat n ⌋ = nat n
⌊ bool b ⌋ = bool b
⌊ e +E e' ⌋ = ⌊ e ⌋ +E ⌊ e' ⌋
⌊ e ≤E e' ⌋ = ⌊ e ⌋ ≤E ⌊ e' ⌋
⌊ ifE e then e' else e'' ⌋ = ifE ⌊ e ⌋ then ⌊ e' ⌋ else ⌊ e'' ⌋
{- equality of types is clearly decidable -}
_≡Ty?_ : (σ τ : Ty) → Dec (σ ≡ τ)
nat ≡Ty? nat = yes refl
nat ≡Ty? bool = no (λ ())
bool ≡Ty? nat = no (λ ())
bool ≡Ty? bool = yes refl
{- The result of checking an expression e is a record containing: -}
record Check (e : Expr) : Set where
constructor check
field
σ : Ty -- a type
te : TExpr σ -- a typed expression
te≡e : ⌊ te ⌋ ≡ e -- if we forget the types we recover e
{- This is the first time we use records in Agda.
Look up the reference manual for a decription of records in Agda. -}
open Check
{- Records also use modules which hide the projection functions. By
opening it we have direct access to the projection functions
corresponding to the field names.
E.g. we have
σ : Check e → Ty
te : (c : Check e) → TExpr (σ c)
-}
{- We implement type inference by recursion over the expression. -}
infer : (e : Expr) → Maybe (Check e)
infer (nat n) = just (check nat (nat n) refl)
infer (bool b) = just (check bool (bool b) refl)
{- To infer a type for e + e' we recursively infer types for e and e'
(which may fail) and make sure that there are nat in which case we
return a typed expression of type nat. -}
infer (e +E e') with infer e | infer e'
infer (.(⌊ te ⌋) +E .(⌊ te' ⌋)) | just (check nat te refl) | just (check nat te' refl)
= just (check nat (te +E te') refl)
infer (e +E e') | _ | _ = nothing
{- ≤ uses the same technique -}
infer (e ≤E e') with infer e | infer e'
infer (.(⌊ te ⌋) ≤E .(⌊ te' ⌋)) | just (check nat te refl) | just (check nat te' refl)
= just (check bool (te ≤E te') refl)
infer (e ≤E e') | _ | _ = nothing
{- if-then-else also has to make sure that both branches have the same
type, which is the type of the result. -}
infer (ifE e then e' else e'') with infer e | infer e' | infer e''
infer (ifE .(⌊ te ⌋) then .(⌊ te' ⌋) else .(⌊ te'' ⌋))
| just (check bool te refl) | just (check σ te' refl) | just (check σ' te'' refl) with σ ≡Ty? σ'
infer (ifE .(⌊ te ⌋) then .(⌊ te' ⌋) else .(⌊ te'' ⌋))
| just (check bool te refl) | just (check σ te' refl) | just (check .σ te'' refl) | yes refl
= just (check σ (ifE te then te' else te'') refl)
infer (ifE .(⌊ te ⌋) then .(⌊ te' ⌋) else .(⌊ te'' ⌋))
| just (check bool te refl) | just (check σ te' refl) | just (check σ' te'' refl) | no _ = nothing
infer (ifE e then e' else e'') | _ | _ | _ = nothing
{- A safe evaluator -}
{- We can also forget the types of typed values -}
⌊_⌋v : {σ : Ty} → TVal σ → Val
⌊ nat n ⌋v = nat n
⌊ bool b ⌋v = bool b
{- We implement a safe evaluator which has the same type as the
untyped evaluator. It exploits the type checker to first produce a
typed expression (or fail) and then runs the fast and safe typed
evaluator.
-}
⟦_⟧s : Expr → Maybe Val
⟦ e ⟧s = infer e >>= λ c → return (⌊ ⟦ Check.te c ⟧T ⌋v)
{- For our examples that safe evaluator produces the same results: -}
v1' : Maybe Val
v1' = ⟦ e1 ⟧s
v2' : Maybe Val
v2' = ⟦ e2 ⟧s
v3' : Maybe Val
v3' = ⟦ e3 ⟧s
{- Is this always the case ? -}