## Tutorial

- Introduction
- Monday 22 Nov 15:00 - 17:30, Original Completed Video
- Tuesday 23 Nov 15:00 - 16:30, Original Completed Video
- Wednesday 24 Nov 15:00 - 17:30, Original Completed Video
- Thursday 25 Nov 15:00 - 17:30, Original Completed Video

## Tutorials.Thursday-Complete

{-# OPTIONS --guardedness #-} import Tutorials.Monday-Complete as Mon import Tutorials.Tuesday-Complete as Tue import Tutorials.Wednesday-Complete as Wed open Mon using (⊤; tt; ℕ; zero; suc) open Mon.Simple using (_⊎_; inl; inr) open Tue.Product using (Σ; _,_; fst; snd; _×_) module Tutorials.Thursday-Complete where variable A B C S : Set -- Things that we skipped so far -------------------------------- module WithAbstraction where open Mon using (Bool; true; false; Pred; _≡_; refl; _+_; subst; +-comm) open Mon.List using (List; []; _∷_) -- With abstraction -- You can use "with abstraction" to pattern match on intermediary computations -- These can be nested, or executed simultaneously filter : (A → Bool) → List A → List A filter f [] = [] filter f (x ∷ xs) with f x filter f (x ∷ xs) | true = x ∷ filter f xs filter f (x ∷ xs) | false = filter f xs -- Alternative notation filter′ : (A → Bool) → List A → List A filter′ f [] = [] filter′ f (x ∷ xs) with f x ... | true = x ∷ filter′ f xs ... | false = filter′ f xs -- The goal type and the type of the arguments are generalised over the value of the scrutinee thm : {P : Pred ℕ} (n m : ℕ) → P (n + m) → P (m + n) -- 1) Here (p : P (n + m)) and (eq : n + m ≡ m + n) -- thm n m p with +-comm n m -- thm n m p | eq = {!!} -- 2) Here (p : P x) and (eq : x ≡ m + n) -- thm n m p with n + m | +-comm n m -- thm n m p | x | eq = {!!} -- 3) Pattern matching we get (p : P (m + n)), the dot signifies that the argument is uniquely determined thm n m p with n + m | +-comm n m thm n m p | .(m + n) | refl = p -- This is such a common formula that there is special syntax for it thm′ : {P : Pred ℕ} (n m : ℕ) → P (n + m) → P (m + n) thm′ {P} n m pr rewrite +-comm n m = pr -- We could use subst to be more explicit about *where* the rewrite happens thm′′ : {P : Pred ℕ} (n m : ℕ) → P (n + m) → P (m + n) thm′′ {P} n m p = subst {P = P} (+-comm n m) p -- A little on coinductive types -------------------------------- -- Stolen from https://github.com/pigworker/CS410-17/blob/master/lectures/Lec6Done.agda ListT : Set → Set → Set ListT X B = ⊤ ⊎ (X × B) module List where data List (A : Set) : Set where [] : List A _∷_ : A → List A → List A mkList : ListT A (List A) → List A mkList (inl tt) = [] mkList (inr (a , as)) = a ∷ as foldr : (ListT A B → B) → List A → B foldr alg [] = alg (inl tt) foldr alg (x ∷ xs) = alg (inr (x , foldr alg xs)) list-id : List A → List A list-id = foldr mkList incr : ListT A ℕ → ℕ incr (inl tt) = zero incr (inr (_ , n)) = suc n length : List A → ℕ length = foldr incr module CoList where record CoList (A : Set) : Set where coinductive field -- next : ⊤ ⊎ (A × CoList A) next : ListT A (CoList A) open CoList [] : CoList A next [] = inl tt _∷_ : A → CoList A → CoList A next (x ∷ xs) = inr (x , xs) unfoldr : (S → ListT A S) → S → CoList A next (unfoldr coalg s) with coalg s next (unfoldr coalg s) | inl tt = inl tt next (unfoldr coalg s) | inr (a , s') = inr (a , unfoldr coalg s') repeat : A → CoList A repeat = unfoldr λ x → inr (x , x) take : ℕ → CoList A → List.List A take zero xs = List.[] take (suc n) xs with next xs take (suc n) xs | inl tt = List.[] take (suc n) xs | inr (a , xs') = a List.∷ take n xs' module Stream where record Stream (A : Set) : Set where coinductive field head : A tail : Stream A open Stream forever : A → Stream A head (forever x) = x tail (forever x) = forever x unfold : (S → A × S) → S → Stream A head (unfold coalg s) = fst (coalg s) tail (unfold coalg s) = unfold coalg (snd (coalg s)) --------------------------------------------- -- If you are interested in more -- Documentation for Agda: https://agda.readthedocs.io/en/v2.6.0.1/index.html -- Programming Language Foundations in Agda: https://plfa.github.io/ -- Lots of other nice tutorials online -- The standard library: https://agda.github.io/agda-stdlib/