module Data.List.Base where

The type of listsπŸ”—

This module contains the definition of the type of lists, and some basic operations on lists. Properties of these operations are in the module Data.List, not here.

data List {β„“} (A : Type β„“) : Type β„“ where
  [] : List A
  _∷_ : A β†’ List A β†’ List A

{-# BUILTIN LIST List #-}

One of the first things we set up is list literal syntax (the From-product class) for lists. The list corresponding to an n-ary product is the list of its elements.

instance
  From-prod-List : From-product A (Ξ» _ β†’ List A)
  From-prod-List .From-product.from-prod = go where
    go : βˆ€ n β†’ Vecβ‚“ A n β†’ List A
    go zero xs                = []
    go (suc zero) xs          = xs ∷ []
    go (suc (suc n)) (x , xs) = x ∷ go (suc n) xs

-- Test:
_ : Path (List Nat) [ 1 , 2 , 3 ] (1 ∷ 2 ∷ 3 ∷ [])
_ = refl

β€œFieldsβ€πŸ”—

head : A β†’ List A β†’ A
head def []     = def
head _   (x ∷ _) = x

tail : List A β†’ List A
tail []       = []
tail (_ ∷ xs) = xs

EliminationπŸ”—

As with any inductive type, the type of lists-of-As has a canonically-defined eliminator, but it also has some fairly popular recursors, called β€œfolds”:

List-elim
  : βˆ€ {β„“ β„“'} {A : Type β„“} (P : List A β†’ Type β„“')
  β†’ P []
  β†’ (βˆ€ x xs β†’ P xs β†’ P (x ∷ xs))
  β†’ βˆ€ x β†’ P x
List-elim P p[] p∷ []       = p[]
List-elim P p[] p∷ (x ∷ xs) = p∷ x xs (List-elim P p[] p∷ xs)

Functorial actionπŸ”—

It’s also possible to lift a function A β†’ B to a function List A β†’ List B.

instance
  Map-List : Map (eff List)
  Map-List = record { map = go } where
    go : (A β†’ B) β†’ List A β†’ List B
    go f []       = []
    go f (x ∷ xs) = f x ∷ go f xs

Monoidal structureπŸ”—

We can define concatenation of lists by recursion:

_++_ : βˆ€ {β„“} {A : Type β„“} β†’ List A β†’ List A β†’ List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

infixr 8 _++_

instance
  Append-List : βˆ€ {β„“} {A : Type β„“} β†’ Append (List A)
  Append-List = record { mempty = [] ; _<>_ = _++_ }
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) = 0 ∷ map suc (count n)

product : List Nat β†’ Nat
product [] = 1
product (x ∷ xs) = x * product xs

reverse : List A β†’ List A
reverse = go [] where
  go : List A β†’ List A β†’ List A
  go acc [] = acc
  go acc (x ∷ xs) = go (x ∷ acc) xs

_∷r_ : List A β†’ A β†’ List A
xs ∷r x = xs ++ (x ∷ [])

infixl 20 _∷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 0 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 0       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 0       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)

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._<|>_ = _<>_

PredicatesπŸ”—

We can define a function that determines if a boolean-valued predicate holds on every element of a list.

all-of : βˆ€ {β„“} {A : Type β„“} β†’ (A β†’ Bool) β†’ List A β†’ Bool
all-of f [] = true
all-of f (x ∷ xs) = and (f x) (all-of f xs)

Dually, we can also define a function that determines if a boolean-valued predicate holds on some element of a list.

any-of : βˆ€ {β„“} {A : Type β„“} β†’ (A β†’ Bool) β†’ List A β†’ Bool
any-of f [] = false
any-of f (x ∷ xs) = or (f x) (any-of f xs)
∷-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 (_ ∷ _) = ⊀

instance
  Discrete-List : βˆ€ ⦃ d : Discrete A ⦄ β†’ Discrete (List A)
  Discrete-List {x = []}     {y = []}     = yes refl
  Discrete-List {x = []}     {y = x ∷ y}  = no Ξ» p β†’ βˆ·β‰ [] (sym p)
  Discrete-List {x = x ∷ xs} {y = []}     = no βˆ·β‰ []
  Discrete-List {x = x ∷ xs} {y = y ∷ ys} = case x ≑? y of Ξ» where
    (yes x=y) β†’ case Discrete-List {x = 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) ! fzero  = x
(x ∷ xs) ! fsuc n = xs ! n

tabulate : βˆ€ {n} (f : Fin n β†’ A) β†’ List A
tabulate {n = zero}  f = []
tabulate {n = suc n} f = f fzero ∷ tabulate (f ∘ fsuc)