Functions from finite sets as a (terminating) alternative to vectors

Fvec.agda

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

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

data Fin : ℕ → Set where
  fzero : ∀{n} → Fin (suc n)
  fsuc  : ∀{n} → Fin n → Fin (suc n)

Fvec : Set → ℕ → Set
Fvec A n = Fin n → A


Vec→Fvec : {n : ℕ} {A : Set} → Vec A n → Fvec A n
Vec→Fvec {zero}    [] ()
Vec→Fvec {(suc n)} (x ∷ xs) fzero = x
Vec→Fvec {(suc n)} (x ∷ xs) (fsuc k) = Vec→Fvec xs k

Fvec→Vec : {n : ℕ} {A : Set} → Fvec A n → Vec A n
Fvec→Vec {zero}    φs = []
Fvec→Vec {(suc n)} φs = φs fzero ∷ Fvec→Vec λ k → φs (fsuc k)


-- Agda sees that recursion over Fvec-based trees terminates
data Tree (A : Set) : Set where
  leaf   : A → Tree A
  branch : ∀{n} → A → Vec (Tree A) n → Tree A

data Ftree (A : Set) : Set where
  leaf   : A → Ftree A
  branch : ∀{n} → A → Fvec (Ftree A) n → Ftree A

map : ∀{n} {A B : Set} → (A → B) → Vec A n → Vec B n
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs


-- Agda will complain if you try this without a pragma, since Agda doesn't
-- understand that map is simply calling (descend f) on subtrees
{-# NON_TERMINATING #-}
descend : ∀{A} → (A → A) → Tree A → Tree A
descend f (leaf x) = leaf (f x)
descend f (branch x ts) = branch (f x) (map (descend f) ts)

-- But this is fine, since Agda sees that (fdescend f) is being called on
-- subtrees
fdescend : ∀{A} → (A → A) → Ftree A → Ftree A
fdescend f (leaf x) = leaf (f x)
fdescend f (branch x ts) = branch (f x) λ k → fdescend f (ts k)