module Padova2025.ProgrammingBasics.Vectors where

Vectors

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

infixr  _∷_
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.

lengthV : {n : ℕ} {A : Set} → Vector A n → ℕ
lengthV = {!!}

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.

replicateV : {A : Set} → (n : ℕ) → A → Vector A n
replicateV = {!!}

Exercise: Map

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

mapV : {n : ℕ} {A B : Set} → (A → B) → Vector A n → Vector B n
mapV = {!!}

Exercise: zipWith

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

zipWithV : {A B C : Set} {n : ℕ} → (A → B → C) → Vector A n → Vector B n → Vector C n
zipWithV = {!!}

Exercise: drop

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

dropV : {A : Set} {n : ℕ} (k : ℕ) → Vector A (k + n) → Vector A n
dropV = {!!}

Exercise: take

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

takeV : {A : Set} {n : ℕ} (k : ℕ) → Vector A (k + n) → Vector A k
takeV = {!!}

Exercise: Concatenation

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

_++V_ : {A : Set} {n m : ℕ} → Vector A n → Vector A m → Vector A (n + m)
_++V_ = {!!}

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 ∷ [].

snocV : {A : Set} {n : ℕ} → Vector A n → A → Vector A (succ n)
snocV = {!!}

Exercise: Reversal

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

reverseV : {A : Set} {n : ℕ} → Vector A n → Vector A n
reverseV = {!!}

Exercise: Flattening vectors of vectors

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

concatV : {!!}
concatV = {!!}