```
{-# 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.

```code
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: Flattening

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

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


## 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
```

::: Aside :::
In Haskell's two-level type system with types governing values and "kinds"
governing types, `List` would be called a "type constructor" of kind `* → *`.
:::