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