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:
_ : [ 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)

foldr : (A β†’ B β†’ B) β†’ B β†’ List A β†’ B
foldr f x = List-elim _ x (Ξ» x _ β†’ f x)

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.

map : (A β†’ B) β†’ List A β†’ List B
map f []       = []
map f (x ∷ xs) = f x ∷ map 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 5 _++_

mapUp : (Nat β†’ A β†’ B) β†’ Nat β†’ List A β†’ List B
mapUp f _ [] = []
mapUp f n (x ∷ xs) = f n x ∷ mapUp f (suc n) xs

length : List A β†’ Nat
length [] = zero
length (x ∷ x₁) = suc (length x₁)

concat : List (List A) β†’ List A
concat [] = []
concat (x ∷ xs) = x ++ concat 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 ∷ [])

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