List

definition example program

The list type $L_a$ (list of $a$) is defined by two introduction rules

$$\mathsf{Nil}:1\to L_a,\mathsf{Cons}:a\times L_a\to L_a,$$

(“a list is either empty or a thing followed by a list of things”) and the elimination rule: given $init:1\to c$ and $step:a\times c\to c$ there is a unique $h:L_a\to c$ with $h\circ \mathsf{Nil}=init$ and $h\circ \mathsf{Cons}=step\circ ({\mathrm{id}}_a\times h)$. Such an $h$ is a fold (list catamorphism); in Haskell foldr step init, with [a], [] and (:) as built-in syntax.

Sources: DaoFP §7.2 (“Lists”, “Elimination Rule”), §7.3 (“Functoriality”: map, badMap), §12.4 (“Lists as initial algebras”), §15.3 (“Free monoid and the list monad”), Exercises 7.2.1–7.2.3; Kittenlab Lecture 5 (ConcatMonoid); 7 Sketches §5.2.4 (free monoid); CTfS Definition 3.1.1.10, Example 3.1.1.11

• Lists as functions (CTfS Definition 3.1.1.10): a list in $X$ is a pair $(n,f)$ with $n\in \mathbb{N}$ its length and $f:\underline{n}\to X$ its entries; concatenation $(n,f)++(n^{\prime },f^{\prime })=(n+n^{\prime },f++f^{\prime })$ uses $f$ on $\mathrm{1..}n$ and $f^{\prime }(i-n)$ after — so $[a,b,c]++[p,a,a,a,p]=[a,b,c,p,a,a,a,p]$ and $[]$ is the unit.
• Functoriality (§7.3): for $f:a\to b$, map f is the fold with $init={\mathsf{Nil}}_b$ and $step={\mathsf{Cons}}_b\circ (f\times \mathrm{id})$. The alternative $step=\mathsf{snd}$ (badMap, which drops all elements) type-checks but fails the functor law map id = id — see Functor.
• $L_a$ is the Free Monoid on $a$ and the Initial Algebra of $F(x)=1+a\times x$; foldr is the catamorphism. $L_1\cong N$ (Natural Numbers Object, DaoFP Exercise 7.2.1).
• Not every mapping out of a list is a fold, but every Haskell function [a] -> c written by pattern matching on [] and (:) is (DaoFP Exercise 7.2.2, DaoFP Exercise 7.2.3).
• sum = foldr plus Z on lists of naturals; the List Monad uses concatenation as join.

JuliaLeanHaskell

Docs: Kittenlab Lecture 5

# foldr as the list recursor
recList(init, step) = as -> isempty(as) ? init : step(as[1], recList(init, step)(as[2:end]))
recList(0, +)([1, 2, 3])                      # 6
mapList(f) = recList(Any[], (a, bs) -> [f(a); bs])
mapList(x -> x^2)([1, 2, 3])                  # [1, 4, 9]
third(as) = length(as) >= 3 ? Some(as[3]) : nothing

import Mathlib
#check @List.rec                -- the eliminator
#check @List.foldr              -- (α → β → β) → β → List α → β
#check @List.map
#check @List.map_id             -- the functor law badMap violates
#check @List.get?               -- l.get? 2 : Option α, the "third element" of Exercise 7.2.3

data List a where
  Nil  :: List a
  Cons :: (a, List a) -> List a
 
recList :: c -> ((a, c) -> c) -> (List a -> c)       -- the list recursor
recList init step = \as -> case as of
  Nil          -> init
  Cons (a, as) -> step (a, recList init step as)
 
foldr' :: (a -> c -> c) -> c -> [a] -> c              -- built-in lists
foldr' step init = \as -> case as of
  []     -> init
  a : as -> step a (foldr' step init as)
 
mapList :: (a -> b) -> List a -> List b
mapList f = recList Nil (\(a, bs) -> Cons (f a, bs))