open import 1Lab.Type.Sigma
open import 1Lab.Path
open import 1Lab.Type

open import Data.Product.NAry
open import Data.Maybe.Base
open import Data.Dec.Base
open import Data.Fin.Base
open import Data.Bool

open import Meta.Traversable
open import Meta.Foldable
open import Meta.Append
open import Meta.Idiom
open import Meta.Bind
open import Meta.Alt

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.

private variable
  β„“ : Level
  A B : Type β„“

infixr 20 _∷_

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)

instance
  Foldable-List : Foldable (eff List)
  Foldable-List .foldr f x = List-elim _ x (Ξ» x _ β†’ f x)

  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 ⦈

foldl : (B β†’ A β†’ B) β†’ B β†’ List A β†’ B
foldl f x []       = x
foldl f x (a ∷ as) = foldl f (f x a) as

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)

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

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) ! 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)