{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProgrammingBasics.Lists where

Lists#

In the Agda community, lists are usually written like a ∷ b ∷ c ∷ [], or more precisely a ∷ (b ∷ (c ∷ [])). The symbol [] denotes the empty list. The operator _∷_ is used for appending (“consing”) a single element in front of an already existing tail of elements. The code to implement this syntax is the following.

infixr 5 _∷_
data List (A : Set) : Set where  -- enter `∷` by `\::`
  []  : List A
  _∷_ : A → List A → List A

The variable A appearing in this datatype definition is a parameter. In effect, for each type A, a new type List A is introduced. If Agda didn’t support parameters, we would be forced to repeat ourselves, for instance with tedious code as the following.

data ListOfBools : Set where
  []  : ListOfBools
  _∷_ : Bool → ListOfBools → ListOfBools

data ListOfNats : Set where
  []  : ListOfNats
  _∷_ : ℕ → ListOfNats → ListOfNats

Exercise: Summing lists#

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic

Define a function which sums the elements of a given list of natural numbers.

sum : List ℕ → ℕ
sum = {!!}

sum : List ℕ → ℕ
sum []       = zero
sum (x ∷ xs) = x + sum xs

Exercise: Length of lists#

Define a function which computes the length of a given list.

length : {A : Set} → List A → ℕ
length = {!!}

length : {A : Set} → List A → ℕ
length []       = zero
length (x ∷ xs) = succ (length xs)

The parameter A is here put in curly brackets so that when calling length, it does not need to be explicitly mentioned: From the explicit argument, a certain list, Agda is able to infer the type of its elements.

Exercise: Replication#

Define a function replicate which reads a number n and an element x as input and outputs a list containing n copies of x.

replicate : {A : Set} → ℕ → A → List A
replicate = {!!}

replicate : {A : Set} → ℕ → A → List A
replicate zero     x = []
replicate (succ n) x = x ∷ replicate n x

Exercise: Concatenation#

Define a binary operator which concatenates two lists. For instance, (a ∷ b ∷ []) ++ (c ∷ d ∷ []) should reduce to a ∷ b ∷ c ∷ d ∷ [].

infixr 5 _++_
_++_ : {A : Set} → List A → List A → List A
_++_ = {!!}

infixr 5 _++_
_++_ : {A : Set} → List A → List A → List A
_++_ []       ys = ys
_++_ (x ∷ xs) ys = x ∷ (xs ++ ys)

Exercise: Flattening#

Define a function which flattens a list of lists into a single list:

concat : {A : Set} → List (List A) → List A
concat = {!!}

concat : {A : Set} → List (List A) → List A
concat []         = []
concat (xs ∷ xss) = xs ++ concat xss

Exercise: Dropping initial elements#

For instance, drop one (a ∷ b ∷ c ∷ []) should evaluate to b ∷ c ∷ [].

drop : {A : Set} (k : ℕ) → List A → List A
drop = {!!}

drop : {A : Set} (k : ℕ) → List A → List A
drop zero     xs       = xs
drop (succ k) []       = []
drop (succ k) (x ∷ xs) = drop k xs

Exercise: Mapping over lists#

Define the map function, which should apply the supplied function f to each element in the input list.

For instance, map f (x ∷ y ∷ z ∷ []) should reduce to f x ∷ f y ∷ f z ∷ [].

map : {A B : Set} → (A → B) → List A → List B
map = {!!}

map : {A B : Set} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

Exercise: Snocking#

For instance, (a ∷ b ∷ c ∷ []) ∷ʳ z should reduce to a ∷ b ∷ c ∷ z ∷ [].

_∷ʳ_ : {A : Set} → List A → A → List A
_∷ʳ_ = {!!}

_∷ʳ_ : {A : Set} → List A → A → List A
_∷ʳ_ []       y = y ∷ []
_∷ʳ_ (x ∷ xs) y = x ∷ (xs ∷ʳ y)

Exercise: Reversal#

Write a function which reverses the elements of a list. For instance, reverse (a ∷ b ∷ c ∷ []) should reduce to c ∷ b ∷ a ∷ [].

reverse : {A : Set} → List A → List A
reverse = {!!}

reverse : {A : Set} → List A → List A
reverse []       = []
reverse (x ∷ xs) = reverse xs ∷ʳ x

-- Alternatively, in tail-recursive form thanks to an accumulator:
-- reverse = reverseAcc []
--   where
--   reverseAcc : {A : Set} → List A → List A → List A
--   reverseAcc acc []       = acc
--   reverseAcc acc (x ∷ xs) = reverseAcc (x ∷ acc) xs

Exercise: Countdown#

Implement a function downFrom which reads a number n as input and outputs the length-n list of numbers from n (exclusively) to 0 (inclusively). For instance, downFrom three should reduce to two ∷ one ∷ zero ∷ [].

downFrom : ℕ → List ℕ
downFrom = {!!}

downFrom : ℕ → List ℕ
downFrom zero     = []
downFrom (succ n) = n ∷ downFrom n

Similarly, implement a function upTo : ℕ → List ℕ such that for instance upTo three reduces to zero ∷ one ∷ two ∷ [].

upTo : ℕ → List ℕ
upTo = {!!}

upTo : ℕ → List ℕ
upTo zero     = []
upTo (succ n) = zero ∷ map succ (upTo n)

Exercise: A higher-kinded function#

The Agda expressions List ℕ, List Bool and so on denote certain types, i.e. elements of Set. Is the bare expression List, without any argument, also meaningful? What is its type?

List' : {!!}
List' = List

List' : Set → Set
List' = List