module FunWithAgda where data Bool : Set where false : Bool true : Bool data Ty : Set where _→_ : (σ τ : Ty) -> Ty bool : Ty 〚_〛 : Ty -> Set 〚 σ → τ 〛 = 〚 σ 〛 -> 〚 τ 〛 〚 bool 〛 = Bool ex₁ = bool → bool data Tm : Ty -> Set where _\$_ : forall {σ τ} (t1 : Tm (σ → τ)) (t2 : Tm σ) -> Tm τ lit : forall {σ} (v : 〚 σ 〛) -> Tm σ ¬ : (t : Tm bool) -> Tm bool eval : forall {σ} -> Tm σ -> 〚 σ 〛 eval (t1 \$ t2) = eval t1 (eval t2) eval (lit v) = v eval (¬ t) with eval t eval (¬ t) | false = true eval (¬ t) | true = false data Raw : Set where _\$_ : (t1 t2 : Raw) -> Raw lit : forall {σ} (v : 〚 σ 〛) -> Raw ¬ : (t : Raw) -> Raw erase : forall {σ} -> Tm σ -> Raw erase (t1 \$ t2) = erase t1 \$ erase t2 erase (lit v) = lit v erase (¬ t) = ¬ (erase t) data WellTyped? : Raw -> Set where fail : forall t -> WellTyped? t ok : forall σ (t : Tm σ) -> WellTyped? (erase t) infer : (t : Raw) -> WellTyped? t infer (t1 \$ t2) = {! !} infer (lit v) = ok _ (lit v) infer (¬ t) with infer t infer (¬ t) | fail .t = fail _ infer (¬ .(erase t')) | ok (σ → τ) t' = fail _ infer (¬ .(erase t')) | ok bool t' = ok bool (¬ t')