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:
_ : [  ,  ,  ] ≡  ∷  ∷  ∷ []
_ = 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  _++_