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