{-
Exercises for TYP at MGS 2021
Monday - solutions
type C-c C-l
to load the file
undo = C-_
-}
open import Data.Nat
variable
A B C : Set
{- 1. -}
add3 : ℕ → ℕ
add3 x = x + 3
tw : (A → A) → A → A
tw f n = f (f n)
-- tw = λ f n → f (f n)
-- evaluate
-- tw tw add3 1
-- C-c C-n -- to evaluate a term
-- derive the result (in a comment) step by step
-- why
{-
tw tw add3 1
= tw (tw add3) 1
= (tw add3) (tw add3 1)
= (tw add3) (add3 (add3 1))
= tw add3 7
= add3 (add3 7)
= 13
-}
{- 2. -}
-- derive lambda terms with the following types
f₀ : (A → B) → (B → C) → (A → C)
f₀ = λ x x₁ x₂ → x₁ (x x₂)
--f₀ = λ f g a → g (f a) -- shed
--f₀ f g a = g (f a)
-- f\_0 = f₀
-- C-c C-, shows goal and all the assumptions.
-- C-c C-SPC
-- C-C C-r (refine) use the function
f₁ : (A → B) → ((A → C) → C) → ((B → C) → C)
f₁ = λ f g h → g λ a -> h (f a)
f₂ : (A → B → C) → B → A → C
f₂ = λ f b a → f a b
{- 3. -}
-- Advanced (see lecture notes 2.4)
{-
Derive a function tw-c which behaves the same as tw
using only S, K (and I which is defined using S and K below).
-}
K : A → B → A
K = λ a b → a
S : (A → B → C) → (A → B) → A → C
S = λ f g x → f x (g x)
-- I = λ x → x
I : A → A
I {A} = S K (K {B = A})
{-
x doesn't appear in M
λ x → M = K M
λ x → x = I
x doesn't appear in M
λ x → M x = M
λ x → M N = S (λ x → M) (λ x → N)
-}
-- tw = λ f → λ n → f (f n)
{-
λ f n → f (f n)
= λ f → λ n → f (f n)
= λ f → S (λ n → f) (λ n → f n)
= λ f → S (K f) f
= S (λ f → S (K f) (λ f → f)
= S (S (λ f → S) (λ f → (K f)) I
= S (S (K S) K) I
-}
tw-c : (A → A) → A → A
tw-c = S (S (K S) K) I