Multiple parameters as vectors

mparam.agda

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat renaming (Nat to ℕ)

data False : Set where
record True : Set where

isTrue : Bool → Set
isTrue false = False
isTrue true  = True

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : ∀{n} → A → Vec A n → Vec A (suc n)
infixr 5 _∷_


--------------------------------------------------------------------------------
-- Naive approach: access the elements

-- For fun
_^_⇒_ : Set → ℕ → Set → Set
A ^ n ⇒ B = (Vec A n) → B

_!_ : ∀{n} → {A : Set} → Vec A n → (k : ℕ) → {_ : isTrue (k < n)} → A
([] ! k) {()}
(x ∷ xs) ! zero = x
((x ∷ xs) ! suc k) {pf} = (xs ! k) {pf}


badder : ℕ ^ 2 ⇒ ℕ
badder pair = (pair ! 0) + (pair ! 1)


--------------------------------------------------------------------------------
-- Better: Agda knows that two elements are passed

-- More fun
ℕ² = Vec ℕ 2

adder : ℕ² → ℕ
adder (x ∷ y ∷ []) = x + y