{-# OPTIONS --without-K --safe #-}
open import Equality
module List
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where
open import Prelude
open Derived-definitions-and-properties eq
open import Monad eq hiding (map)
foldr : ∀ {a b} {A : Set a} {B : Set b} →
(A → B → B) → B → List A → B
foldr _⊕_ ε [] = ε
foldr _⊕_ ε (x ∷ xs) = x ⊕ foldr _⊕_ ε xs
foldl : ∀ {a b} {A : Set a} {B : Set b} →
(B → A → B) → B → List A → B
foldl _⊕_ ε [] = ε
foldl _⊕_ ε (x ∷ xs) = foldl _⊕_ (ε ⊕ x) xs
length : ∀ {a} {A : Set a} → List A → ℕ
length = foldr (const suc) 0
infixr 5 _++_
_++_ : ∀ {a} {A : Set a} → List A → List A → List A
xs ++ ys = foldr _∷_ ys xs
map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
map f = foldr (λ x ys → f x ∷ ys) []
concat : ∀ {a} {A : Set a} → List (List A) → List A
concat = foldr _++_ []
reverse : ∀ {a} {A : Set a} → List A → List A
reverse = foldl (λ xs x → x ∷ xs) []
replicate : ∀ {a} {A : Set a} → ℕ → A → List A
replicate zero x = []
replicate (suc n) x = x ∷ replicate n x
filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
filter p = foldr (λ x xs → if p x then x ∷ xs else xs) []
index : ∀ {a} {A : Set a} (xs : List A) → Fin (length xs) → A
index [] ()
index (x ∷ xs) fzero = x
index (x ∷ xs) (fsuc i) = index xs i
lookup : ∀ {a b} {A : Set a} {B : Set b} →
(A → A → Bool) → A → List (A × B) → Maybe B
lookup _≟_ x [] = nothing
lookup _≟_ x ((y , z) ∷ ps) =
if x ≟ y then just z else lookup _≟_ x ps
foldr-∷-[] : ∀ {a} {A : Set a} (xs : List A) → foldr _∷_ [] xs ≡ xs
foldr-∷-[] [] = refl _
foldr-∷-[] (x ∷ xs) = cong (x ∷_) (foldr-∷-[] xs)
++-associative : ∀ {a} {A : Set a} (xs ys zs : List A) →
xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
++-associative [] ys zs = refl _
++-associative (x ∷ xs) ys zs = cong (x ∷_) (++-associative xs ys zs)
map-++ : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (xs ys : List A) →
map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++ f [] ys = refl _
map-++ f (x ∷ xs) ys = cong (f x ∷_) (map-++ f xs ys)
concat-++ : ∀ {a} {A : Set a} (xss yss : List (List A)) →
concat (xss ++ yss) ≡ concat xss ++ concat yss
concat-++ [] yss = refl _
concat-++ (xs ∷ xss) yss =
concat ((xs ∷ xss) ++ yss) ≡⟨⟩
xs ++ concat (xss ++ yss) ≡⟨ cong (xs ++_) (concat-++ xss yss) ⟩
xs ++ (concat xss ++ concat yss) ≡⟨ ++-associative xs _ _ ⟩
(xs ++ concat xss) ++ concat yss ≡⟨ refl _ ⟩∎
concat (xs ∷ xss) ++ concat yss ∎
instance
raw-monad : ∀ {ℓ} → Raw-monad (List {a = ℓ})
Raw-monad.return raw-monad x = x ∷ []
Raw-monad._>>=_ raw-monad xs f = concat (map f xs)
monad : ∀ {ℓ} → Monad (List {a = ℓ})
Monad.raw-monad monad = raw-monad
Monad.left-identity monad x f = foldr-∷-[] (f x)
Monad.right-identity monad xs = lemma xs
where
lemma : ∀ xs → concat (map (_∷ []) xs) ≡ xs
lemma [] = refl _
lemma (x ∷ xs) =
concat (map (_∷ []) (x ∷ xs)) ≡⟨⟩
x ∷ concat (map (_∷ []) xs) ≡⟨ cong (x ∷_) (lemma xs) ⟩∎
x ∷ xs ∎
Monad.associativity monad xs f g = lemma xs
where
lemma : ∀ xs → concat (map (concat ∘ map g ∘ f) xs) ≡
concat (map g (concat (map f xs)))
lemma [] = refl _
lemma (x ∷ xs) =
concat (map (concat ∘ map g ∘ f) (x ∷ xs)) ≡⟨⟩
concat (map g (f x)) ++ concat (map (concat ∘ map g ∘ f) xs) ≡⟨ cong (concat (map g (f x)) ++_) (lemma xs) ⟩
concat (map g (f x)) ++ concat (map g (concat (map f xs))) ≡⟨ sym $ concat-++ (map g (f x)) _ ⟩
concat (map g (f x) ++ map g (concat (map f xs))) ≡⟨ cong concat (sym $ map-++ g (f x) _) ⟩
concat (map g (f x ++ concat (map f xs))) ≡⟨ refl _ ⟩∎
concat (map g (concat (map f (x ∷ xs)))) ∎