Well typed primitive recursive functions in Agda

PRF.agda

module PRF where

open import Data.Nat
open import Data.Vec
open import Data.Fin using (Fin; #_)

data PRF : ℕ → Set where
  z : PRF 0
  s : PRF 1
  p : {n : ℕ} (i : Fin n) → PRF n
  comp : {m n : ℕ} (g : PRF m) → (fs : Vec (PRF n) m) → PRF n
  rec : {n : ℕ} (g : PRF n) → (h : PRF (2 + n)) → PRF (1 + n)

mutual
  [[_]]_ : {n : ℕ} (f : PRF n) → Vec ℕ n → ℕ
  [[ z ]] _ = 0
  [[ s ]] (x ∷ []) = 1 + x
  [[ p i ]] xs = lookup i xs
  [[ comp g fs ]] xs = [[ g ]] ([[ fs ]]* xs)
  [[ rec g h ]] (zero ∷ xs) = [[ g ]] xs
  [[ rec g h ]] ((suc y) ∷ xs) = [[ h ]] (y ∷ [[ rec g h ]] (y ∷ xs) ∷ xs)

  [[_]]*_ : {n m : ℕ} (fs : Vec (PRF n) m) → Vec ℕ n → Vec ℕ m
  [[ [] ]]* t = []
  [[ f ∷ fs ]]* t = ([[ f ]] t) ∷ [[ fs ]]* t


-- Programs

add : PRF 2
add = rec (p (# 0)) (comp s [ p (# 1) ])

pre : PRF 1
pre = rec z (p (# 1))

mul : PRF 2
mul = rec (comp z []) (comp add (p (# 1) ∷ p (# 2) ∷ []))

fact : PRF 1
fact = rec (comp s [ z ])
           (comp mul (comp s [ p (# 0) ] ∷ p (# 1) ∷ []))