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