FLOLAC18.agda

-- programming

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

_+_ : Nat → Nat → Nat
zero  + n = n
suc m + n = suc (m + n)

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

sum : List Nat → Nat
sum []       = zero
sum (x ∷ xs) = x + sum xs

map : {A B : Set} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

-- proving

rapp : {A B : Set} → A → (A → B) → B
rapp x f = f x

data _∧_ (A B : Set) : Set where
  _,_ : A → B → A ∧ B

data _∨_ (A B : Set) : Set where
  left  : A → A ∨ B
  right : B → A ∨ B

distr : {A B C : Set} → A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)
distr (x , left  y) = left  (x , y)
distr (x , right z) = right (x , z)

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

¬_ : Set → Set
¬ A = A → ⊥

ex1 : {A : Set} → ¬ ¬ (¬ ¬ A → A)
ex1 x = x (λ y → ⊥-elim (y (λ z → x (λ _ → z))))

ex2 : {A B C : Set} → ¬ ¬ (A ∨ B) → (¬ ¬ A → ¬ ¬ C) → (¬ ¬ B → ¬ ¬ C) → ¬ ¬ C
ex2 x y z w = x (λ { (left u) → y (λ z₁ → z₁ u) w; (right v) → z (λ z₁ → z₁ v) w })

-- equality

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

pm : (suc zero + suc zero) ≡ suc (suc zero)
pm = refl

arith-contradiction : ¬ (zero ≡ suc zero)
arith-contradiction ()

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl eq = eq

cong : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

_∘_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
(f ∘ g) x = f (g x)

map-functorial : {A B C : Set} (f : B → C) (g : A → B) → (xs : List A) → map (f ∘ g) xs ≡ map f (map g xs)
map-functorial f g []       = refl
map-functorial f g (x ∷ xs) = cong (f (g x) ∷_) (map-functorial f g xs)

-- equational reasoning

_≡[_]_ : {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡[ eq ] eq' = trans eq eq'

_∎ : {A : Set} (x : A) → x ≡ x
x ∎ = refl

infixr 1 _≡[_]_
infix 2 _∎

map-functorial' : {A B C : Set} (f : B → C) (g : A → B) → (xs : List A) → map (f ∘ g) xs ≡ map f (map g xs)
map-functorial' f g [] =
  map (f ∘ g) []
    ≡[ refl ]
  []
    ≡[ refl ]
  map f []
    ≡[ refl ]
  map f (map g [])
    ∎
map-functorial' f g (x ∷ xs) =
  map (f ∘ g) (x ∷ xs)
    ≡[ refl ]
  (f ∘ g) x ∷ map (f ∘ g) xs
    ≡[ refl ]
  f (g x) ∷ map (f ∘ g) xs
    ≡[ cong (f (g x) ∷_) (map-functorial' f g xs) ]
  f (g x) ∷ map f (map g xs)
    ≡[ refl ]
  map f (g x ∷ map g xs)
    ≡[ refl ]
  map f (map g (x ∷ xs))
    ∎

-- indexed datatypes

{-# BUILTIN NATURAL Nat #-}

data Vec (A : Set) : Nat → Set where
  []  : Vec A 0
  _∷_ : A → {n : Nat} → Vec A n → Vec A (suc n)

vec3 : Vec Nat 3
vec3 = 0 ∷ (1 ∷ (2 ∷ []))

_++_ : {A : Set} {m n : Nat} → Vec A m → Vec A n → Vec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

data SumList : Nat → Set where
  []  : SumList 0
  _∷_ : (m : Nat) {n : Nat} → SumList n → SumList (m + n)

slist15 : SumList 15
slist15 = 3 ∷ (9 ∷ (2 ∷ (1 ∷ (0 ∷ []))))

expand : {n : Nat} → SumList n → Vec Nat n
expand []       = []
expand (x ∷ xs) = aux x ++ expand xs
  where
    aux : (y : Nat) → Vec Nat y
    aux zero    = []
    aux (suc y) = y ∷ aux y

-- metamorphisms (0.625₁₀ = 0.101₂)

-- coinductive lists

mutual

  record CoList (B : Set) : Set where
    coinductive
    field
      decon : CoListF B

  data CoListF (B : Set) : Set where
    []  : CoListF B
    _∷_ : B → CoList B → CoListF B

downFrom : Nat → CoList Nat
CoList.decon (downFrom zero   ) = []
CoList.decon (downFrom (suc n)) = n ∷ downFrom n

upFrom : Nat → CoList Nat
CoList.decon (upFrom n) = n ∷ upFrom (suc n)

take : {B : Set} → Nat → CoList B → List B
take zero    xs = []
take (suc n) xs with CoList.decon xs
take (suc n) xs | []      = []
take (suc n) xs | b ∷ xs' = b ∷ take n xs'

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A

unfoldr : {B S : Set} (g : S → Maybe (B ∧ S)) → S → CoList B
CoList.decon (unfoldr g s) with g s
CoList.decon (unfoldr g s) | nothing       = []
CoList.decon (unfoldr g s) | just (b , s') = b ∷ unfoldr g s'

downFrom' : Nat → CoList Nat
downFrom' = unfoldr (λ { zero → nothing; (suc n) → just (n , n) })

upFrom' : Nat → CoList Nat
upFrom' = unfoldr (λ n → just (n , suc n))

-- foldl as foldr

foldr : {A S : Set} → (A → S → S) → S → List A → S
foldr f e []       = e
foldr f e (x ∷ xs) = f x (foldr f e xs)

foldl : {A S : Set} → (S → A → S) → S → List A → S
foldl f e []       = e
foldl f e (x ∷ xs) = foldl f (f e x) xs

flip : {A B C : Set} → (A → B → C) → (B → A → C)
flip f y x = f x y

fromLeftAlg : {A S : Set} → (S → A → S) → (A → (S → S) → (S → S))
fromLeftAlg f a t = t ∘ flip f a

id : {A : Set} → A → A
id x = x

foldl-as-foldr : {A S : Set} {f : S → A → S} {e : S} (xs : List A) → foldl f e xs ≡ foldr (fromLeftAlg f) id xs e
foldl-as-foldr []       = refl
foldl-as-foldr (x ∷ xs) = foldl-as-foldr xs

-- algebraic and coalgebraic lists

data AlgList (A : Set) {S : Set} (f : A → S → S) (e : S) : S → Set where
  []  : AlgList A f e e
  _∷_ : (a : A) → {s : S} → AlgList A f e s → AlgList A f e (f a s)

vec3' : AlgList Nat (λ _ n → suc n) 0 3
vec3' = 0 ∷ (1 ∷ (2 ∷ []))

slist15' : AlgList Nat _+_ 0 15
slist15' = 3 ∷ (9 ∷ (2 ∷ (1 ∷ (0 ∷ []))))

mutual

  record CoalgList (B : Set) {S : Set} (g : S → Maybe (B ∧ S)) (s : S) : Set where
    coinductive
    field
      decon : CoalgListF B g s

  data CoalgListF (B : Set) {S : Set} (g : S → Maybe (B ∧ S)) : S → Set where
    ⟨_⟩    : {s : S} → g s ≡ nothing → CoalgListF B g s
    _∷⟨_⟩_ : (b : B) → {s s' : S} → g s ≡ just (b , s') → CoalgList B g s' → CoalgListF B g s

open CoalgList

single : CoalgList Nat (λ { zero → nothing; (suc n) → just (n , n) }) 1
CoalgList.decon single = 0 ∷⟨ refl ⟩ none
  where
    none : CoalgList Nat _ 0
    CoalgList.decon none = ⟨ refl ⟩

-- metamorphic algorithms

data Inspect {A B : Set} (f : A → B) (x : A) (y : B) : Set where
 [[_]] : f x ≡ y → Inspect f x y
 
inspect : {A B : Set} (f : A → B) (x : A) → Inspect f x (f x)
inspect f x = [[ refl ]]

module _ {A B S : Set} (f : S → A → S) (g : S → Maybe (B ∧ S)) where

  meta : {h : S → S} → AlgList A (fromLeftAlg f) id h → (s : S) → CoalgList B g (h s)
  decon (meta [] s) with g s        | inspect g s
  decon (meta [] s) | nothing       | [[ eq ]] = ⟨ eq ⟩
  decon (meta [] s) | just (b , s') | [[ eq ]] = b ∷⟨ eq ⟩ meta [] s'
  decon (meta (a ∷ as) s) = decon (meta as (f s a))

module _ {A B S : Set} (f : S → A → S) (g : S → Maybe (B ∧ S))
         (streaming-condition : {a : A} {b : B} {s s' : S} → g s ≡ just (b , s') → g (f s a) ≡ just (b , f s' a)) where

  lemma : {s : S} {b : B} {s' : S} {h : S → S} →
          AlgList A (fromLeftAlg f) id h →
          g s ≡ just (b , s') → g (h s) ≡ just (b , h s')
  lemma []       eq = eq
  lemma (a ∷ as) eq = lemma as (streaming-condition eq)

  stream : {h : S → S} → AlgList A (fromLeftAlg f) id h → (s : S) → CoalgList B g (h s)
  decon (stream as       s) with g s        | inspect g s
  decon (stream []       s) | nothing       | [[ eq ]] = ⟨ eq ⟩
  decon (stream (a ∷ as) s) | nothing       | [[ eq ]] = decon (stream as (f s a))
  decon (stream as       s) | just (b , s') | [[ eq ]] = b ∷⟨ lemma as eq ⟩ stream as s'