πŸ“₯ Download raw
{-# 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 = {!!}

Exercise: Length of lists

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

length : {A : Set} β†’ List A β†’ β„•
length = {!!}

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 = {!!}

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
_++_ = {!!}

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 = {!!}

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 = {!!}

Exercise: Snocking

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

_∷ʳ_ : {A : Set} β†’ List A β†’ A β†’ List A
_∷ʳ_ = {!!}

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 = {!!}

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 = {!!}

Similarly, implement a function upTo : β„• β†’ List β„• such that for instance upTo three reduces to zero ∷ one ∷ two ∷ [].

upTo : β„• β†’ List β„•
upTo = {!!}

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

In Haskell’s two-level type system with types governing values and β€œkinds” governing types, List would be called a β€œtype constructor” of kind * β†’ *.