The type of lists🔗

private variable
  ℓ : Level
  A B : Type ℓ

infixr  _∷_

instance
  Foldable-List : Foldable (eff List)
  Foldable-List .foldr {a = A} {b = B} f b = go module foldr where
    go : List A → B
    go [] = b
    go (x ∷ xs) = f x (go xs)


  Traversable-List : Traversable (eff List)
  Traversable-List = record { traverse = go } where
    go
      : ∀ {M : Effect} ⦃ _ : Idiom M ⦄ (let module M = Effect M) {ℓ ℓ'}
          {a : Type ℓ} {b : Type ℓ'}
      → (a → M.₀ b) → List a → M.₀ (List b)
    go f []       = pure []
    go f (x ∷ xs) = ⦇ f x ∷ go f xs ⦈

{-# DISPLAY foldr.go f b xs = foldr f b xs #-}


foldl : (B → A → B) → B → List A → B
foldl f x []       = x
foldl f x (a ∷ as) = foldl f (f x a) as

map-up : (Nat → A → B) → Nat → List A → List B
map-up f _ []       = []
map-up f n (x ∷ xs) = f n x ∷ map-up f (suc n) xs

length : List A → Nat
length []       = zero
length (x ∷ xs) = suc (length xs)

concat : List (List A) → List A
concat [] = []
concat (x ∷ xs) = x ++ concat xs

count : Nat → List Nat
count zero = []
count (suc n) =  ∷ map suc (count n)

product : List Nat → Nat
product [] = 
product (x ∷ xs) = x * product xs

module reverse where
  go : List A → List A → List A
  go acc [] = acc
  go acc (x ∷ xs) = go (x ∷ acc) xs

  go-β : (acc xs prx : List A) → go (prx ++ acc) xs ≡ go prx xs ++ acc
  go-β acc []       prx = refl
  go-β acc (x ∷ xs) prx = go-β acc xs (x ∷ prx)

reverse : List A → List A
reverse = reverse.go []

reverse' : List A → List A
reverse' []       = []
reverse' (x ∷ xs) = reverse' xs ++ (x ∷ [])

reverse-β : (xs : List A) → reverse xs ≡ reverse' xs
reverse-β [] = refl
reverse-β (x ∷ xs) = reverse.go-β (x ∷ []) xs [] ∙ ap₂ _++_ (reverse-β xs) refl

_∷r_ : List A → A → List A
xs ∷r x = xs ++ (x ∷ [])

infixl  _∷r_

all=? : (A → A → Bool) → List A → List A → Bool
all=? eq=? [] [] = true
all=? eq=? [] (x ∷ ys) = false
all=? eq=? (x ∷ xs) [] = false
all=? eq=? (x ∷ xs) (y ∷ ys) = and (eq=? x y) (all=? eq=? xs ys)

enumerate : ∀ {ℓ} {A : Type ℓ} → List A → List (Nat × A)
enumerate = go  where
  go : Nat → List _ → List (Nat × _)
  go x [] = []
  go x (a ∷ b) = (x , a) ∷ go (suc x) b

take : ∀ {ℓ} {A : Type ℓ} → Nat → List A → List A
take        xs       = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n xs

drop : ∀ {ℓ} {A : Type ℓ} → Nat → List A → List A
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x ∷ xs) = drop n xs

split-at : ∀ {ℓ} {A : Type ℓ} → Nat → List A → List A × List A
split-at        xs       = [] , xs
split-at (suc n) []       = [] , []
split-at (suc n) (x ∷ xs) = ×-map₁ (x ∷_) (split-at n xs)

span : ∀ {ℓ} {A : Type ℓ} (p : A → Bool) → List A → List A × List A
span p [] = [] , []
span p (x ∷ xs) with p x
... | true  = ×-map₁ (x ∷_) (span p xs)
... | false = [] , x ∷ xs

filter : ∀ {ℓ} {A : Type ℓ} (p : A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) with p x
... | true  = x ∷ filter p xs
... | false = filter p xs

intercalate : ∀ {ℓ} {A : Type ℓ} (x : A) (xs : List A) → List A
intercalate x []           = []
intercalate x (y ∷ [])     = y ∷ []
intercalate x (y ∷ z ∷ xs) = y ∷ x ∷ intercalate x (z ∷ xs)

zip : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → List A → List B → List (A × B)
zip [] _ = []
zip _ [] = []
zip (a ∷ as) (b ∷ bs) = (a , b) ∷ zip as bs

unzip : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → List (A × B) → List A × List B
unzip [] = [] , []
unzip ((a , b) ∷ xs) = ×-map (a ∷_) (b ∷_) (unzip xs)

sigma : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → List A → (∀ a → List (B a)) → List (Σ A B)
sigma [] f = []
sigma (x ∷ xs) f = map (x ,_) (f x) <> sigma xs f

instance
  Idiom-List : Idiom (eff List)
  Idiom-List .pure a = a ∷ []
  Idiom-List ._<*>_ f a = concat ((_<$> a) <$> f)

  Bind-List : Bind (eff List)
  Bind-List ._>>=_ a f = concat (f <$> a)

  Alt-List : Alt (eff List)
  Alt-List .Alt.fail  = []
  Alt-List .Alt._<|>_ = _<>_

∷-head-inj : ∀ {x y : A} {xs ys} → (x ∷ xs) ≡ (y ∷ ys) → x ≡ y
∷-head-inj {x = x} p = ap (head x) p

∷-tail-inj : ∀ {x y : A} {xs ys} → (x ∷ xs) ≡ (y ∷ ys) → xs ≡ ys
∷-tail-inj p = ap tail p

∷≠[] : ∀ {x : A} {xs} → ¬ (x ∷ xs) ≡ []
∷≠[] {A = A} p = subst distinguish p tt where
  distinguish : List A → Type
  distinguish []     = ⊥
  distinguish (_ ∷ _) = ⊤

[]≠∷ : ∀ {x : A} {xs} → ¬ [] ≡ (x ∷ xs)
[]≠∷ {A = A} p = ∷≠[] (sym p)

instance
  Discrete-List : ∀ ⦃ d : Discrete A ⦄ → Discrete (List A)
  Discrete-List .decide = go where
    go : ∀ x y → Dec (x ≡ y)
    go []     []         = yes refl
    go []     (x ∷ y)    = no λ p → ∷≠[] (sym p)
    go (x ∷ xs) []       = no ∷≠[]
    go (x ∷ xs) (y ∷ ys) = case x ≡? y of λ where
      (yes x=y) → case go xs ys of λ where
        (yes xs=ys) → yes (ap₂ _∷_ x=y xs=ys)
        (no  xs≠ys) → no λ p → xs≠ys (∷-tail-inj p)
      (no x≠y)      → no λ p → x≠y (∷-head-inj p)

traverse-up
  : ∀ {M : Effect} ⦃ _ : Idiom M ⦄ (let module M = Effect M) {ℓ ℓ'}
    {a : Type ℓ} {b : Type ℓ'}
  → (Nat → a → M.₀ b) → Nat → List a → M.₀ (List b)
traverse-up f n xs = sequence (map-up f n xs)

lookup : ⦃ _ : Discrete A ⦄ → A → List (A × B) → Maybe B
lookup x [] = nothing
lookup x ((k , v) ∷ xs) with x ≡? k
... | yes _ = just v
... | no  _ = lookup x xs

_!_ : (l : List A) → Fin (length l) → A
(x ∷ xs) ! n with fin-view n
... | zero  = x
... | suc i = xs ! i

tabulate : ∀ {n} (f : Fin n → A) → List A
tabulate {n = zero}  f = []
tabulate {n = suc n} f = f fzero ∷ tabulate (f ∘ fsuc)