Let's play Agda 
{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProgrammingBasics.Vectors where

Vectors#

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
infixr 5 _∷_
data Vector (A : Set) : β„• β†’ Set where
  []  : Vector A zero
  _∷_ : {n : β„•} β†’ A β†’ Vector A n β†’ Vector A (succ n)

Exercise: Length#

Define a function which computes the length of a given vector. There are two possible implementations, one which runs in constant time and one which runs in linear time.

Exercise 1lengthV
lengthV : {n : β„•} {A : Set} β†’ Vector A n β†’ β„•
lengthV = {!!}
Reference solution
lengthV : {n : β„•} {A : Set} β†’ Vector A n β†’ β„•
lengthV {n} xs = n

-- This is the O(1) implementation. A slower O(n) implementation
-- reconstructs the size from the vector itself, disregarding
-- the type information:
-- lengthV' []       = zero
-- lengthV' (x ∷ xs) = succ (lengthV xs)

Exercise: Replication#

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

Exercise 2replicateV
replicateV : {A : Set} β†’ (n : β„•) β†’ A β†’ Vector A n
replicateV = {!!}
The reference solution uses: zero [] succ _∷_
Reference solution
replicateV : {A : Set} β†’ (n : β„•) β†’ A β†’ Vector A n
replicateV zero     x = []
replicateV (succ n) x = x ∷ replicateV n x

Exercise: Map#

Define the map function for vectors. For instance, map f (x ∷ y ∷ z ∷ []) should reduce to f x ∷ f y ∷ f z ∷ [].

Exercise 3mapV
mapV : {n : β„•} {A B : Set} β†’ (A β†’ B) β†’ Vector A n β†’ Vector B n
mapV = {!!}
The reference solution uses: [] _∷_
Reference solution
mapV : {n : β„•} {A B : Set} β†’ (A β†’ B) β†’ Vector A n β†’ Vector B n
mapV f []       = []
mapV f (x ∷ xs) = f x ∷ mapV f xs

Exercise: zipWith#

For instance, zipWithV f (x ∷ y ∷ []) (a ∷ b ∷ []) should evaluate to f x a ∷ f y b ∷ [].

Exercise 4zipWithV
zipWithV : {A B C : Set} {n : β„•} β†’ (A β†’ B β†’ C) β†’ Vector A n β†’ Vector B n β†’ Vector C n
zipWithV = {!!}
The reference solution uses: [] _∷_
Reference solution
zipWithV : {A B C : Set} {n : β„•} β†’ (A β†’ B β†’ C) β†’ Vector A n β†’ Vector B n β†’ Vector C n
zipWithV f []       []       = []
zipWithV f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWithV f xs ys

Exercise: drop#

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

Exercise 5dropV
dropV : {A : Set} {n : β„•} (k : β„•) β†’ Vector A (k + n) β†’ Vector A n
dropV = {!!}
The reference solution uses: zero succ _∷_
Reference solution
dropV : {A : Set} {n : β„•} (k : β„•) β†’ Vector A (k + n) β†’ Vector A n
dropV zero     xs       = xs
dropV (succ n) (x ∷ xs) = dropV n xs

Exercise: take#

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

Exercise 6takeV
takeV : {A : Set} {n : β„•} (k : β„•) β†’ Vector A (k + n) β†’ Vector A k
takeV = {!!}
The reference solution uses: zero [] succ _∷_
Reference solution
takeV : {A : Set} {n : β„•} (k : β„•) β†’ Vector A (k + n) β†’ Vector A k
takeV zero     xs       = []
takeV (succ n) (x ∷ xs) = x ∷ takeV n xs

Exercise: Concatenation#

For instance, (a ∷ b ∷ []) ++V (c ∷ d ∷ []) should evaluate to a ∷ b ∷ c ∷ d ∷ [].

Exercise 7_++V_
_++V_ : {A : Set} {n m : β„•} β†’ Vector A n β†’ Vector A m β†’ Vector A (n + m)
_++V_ = {!!}
The reference solution uses: [] _∷_
Reference solution
_++V_ : {A : Set} {n m : β„•} β†’ Vector A n β†’ Vector A m β†’ Vector A (n + m)
_++V_ []       ys = ys
_++V_ (x ∷ xs) ys = x ∷ (xs ++V ys)

Exercise: Snocking#

Write a function which appends a new element at the end. For instance, snocV (a ∷ b ∷ []) c should evaluate to a ∷ b ∷ c ∷ [].

Exercise 8snocV
snocV : {A : Set} {n : β„•} β†’ Vector A n β†’ A β†’ Vector A (succ n)
snocV = {!!}
The reference solution uses: [] _∷_
Reference solution
snocV : {A : Set} {n : β„•} β†’ Vector A n β†’ A β†’ Vector A (succ n)
snocV []       y = y ∷ []
snocV (x ∷ xs) y = x ∷ snocV xs y

Exercise: Reversal#

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

Exercise 9reverseV
reverseV : {A : Set} {n : β„•} β†’ Vector A n β†’ Vector A n
reverseV = {!!}
The reference solution uses: [] _∷_ snocV
Reference solution
reverseV : {A : Set} {n : β„•} β†’ Vector A n β†’ Vector A n
reverseV []       = []
reverseV (x ∷ xs) = snocV (reverseV xs) x

Exercise: Flattening vectors of vectors#

For instance, concatV ((a ∷ b ∷ []) ∷ (c ∷ d ∷ []) ∷ []) should evaluate to a ∷ b ∷ c ∷ d ∷ [].

Exercise 10concatV
concatV : {!!}
concatV = {!!}
The reference solution uses: β„• Vector _Β·_ [] _∷_ _++V_
Reference solution
concatV : {A : Set} {n m : β„•} β†’ Vector (Vector A n) m β†’ Vector A (m Β· n)
concatV []         = []
concatV (xs ∷ xss) = xs ++V concatV xss

Note that this exercise nontrivially depends on the somewhat arbitrary choices in implementing addition and multiplication of natural numbers: Should the case split be on the first or on the second argument? Should succ a Β· b be defined as b + a Β· b or as a Β· b + b? Et cetera. This state of affairs is unsatisfying and there are a couple of proposals attacking this problem. One of these is objective type theory by Benno van den Bergh and Martijn den Besten.