Tutorial

Tutorials.Thursday-Complete

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/