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