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

open import Data.Product.NAry

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 _++_