{- As you discovered in the last coursework variables are tricky. Things get even worse when we have languages with binders (λ,∀,let, etc.). In this coursework we will avoid these problems altogether by considering only combinatory expressions. Schönfinkel and later Curry developed systems of combinators with the same purpose in mind - avoiding the complications of quantifiers and variables. There are no goals to fill in in this buffer. Instead you must extend the language given below in five different ways. For each extension also give at least one test expression which makes use of the new features when evaluated (e.g. projected from a pair, running if then else on a boolean etc.) test : ∀{...} → Exp ? test = ? You can then execute "eval test" to run your test program Please save each extension in a separate file entitled respectively CombQuestion[A-E].agda IMPORTANT: When you extend the language please only introduce terms of the form: newconstructor : ∀{...} → Exp ? i.e. The constructors you add Exp should take no explicit arguments. Otherwise they are not in combinatory style. Scroll down to read the questions. -} module CombQuestions where -- a universe of codes data TyCode : Set where _⇒_ : TyCode → TyCode → TyCode -- interpretation function that inteprets our object level typecodes as real Agda types Val : TyCode → Set Val (σ ⇒ τ) = Val σ → Val τ infixr 10 _⇒_ data Exp : TyCode → Set where K : ∀{σ τ} → Exp (σ ⇒ τ ⇒ σ) S : ∀{σ τ ρ} → Exp ((σ ⇒ τ ⇒ ρ) ⇒ (σ ⇒ τ) ⇒ σ ⇒ ρ) _$_ : ∀{σ τ} → Exp (σ ⇒ τ) → Exp σ → Exp τ infixl 10 _$_ eval : ∀{σ} → Exp σ → Val σ eval K = λ x y → x eval S = λ x y z → x z (y z) eval (t $ u) = eval t (eval u) -- Here is an example of a test test : ∀{σ} → Exp (σ ⇒ σ) test {σ} = S {τ = σ ⇒ σ} $ K $ K -- running (computing to normal form) "eval test" gives λ x → x. It is -- evaluated to the identity function. This test is works for any σ -- but later when you added some base type (e.g. Bool) you may want to -- give a closed term. {- Question A ========== Extend your language to support booleans with the following functionality: -} data Bool : Set where tt : Bool ff : Bool if_then_else_ : {S : Set} → Bool → S → S → S if tt then x else _ = x if ff then _ else y = y {- Question B ========== Extend your language to support natural numbers with the following functionality: -} data Nat : Set where z : Nat s : Nat -> Nat -- Primitive recursion (induction on natural numbers) prim : {S : Set} → S → (Nat → S → S) → Nat → S prim zz ss z = zz prim zz ss (s n) = ss n (prim zz ss n) {- Question C ========== Extend your language to support finite products (a.k.a True and And, cartesian product and singleton, pairs and unit type) with the following functionality: -} data Unit : Set where void : Unit data _×_ (A B : Set) : Set where pr : A → B → A × B fst : ∀{A B} → A × B → A fst (pr a b) = a snd : ∀{A B} → A × B → B snd (pr a b) = b {- Question D ========== Extend your language to support finite coproducts (a.k.a False and Or, disjoint union and empty set) with the following functionality: -} data Empty : Set where naughtE : {A : Set} → Empty → A naughtE () data _+_ (A B : Set) : Set where inl : A → A + B inr : B → A + B +elim : {A B C : Set} → (A → C) → (B → C) → A + B → C +elim f _ (inl a) = f a +elim _ g (inr b) = g b {- Question E ========== Extend your language to support lists with the following functionality: -} data List (X : Set) : Set where ε : List X _<_ : List X → X → List X listrec : {X Y : Set} → Y → (List X → X → Y → Y) → List X → Y listrec mε m< ε = mε listrec mε m< (xs < x) = m< xs x (listrec mε m< xs) {- There are no starred exercises as such this week. If you finish early then please extend the languages discussed in the lectures and in the coursework in any way you see fit. You're welcome to report your findings to me. -}