Mutually Defined Datatypes

MutuallyDefined.agda

{-# OPTIONS --no-termination-check --no-positivity-check #-}

module MutuallyDefined where

open import Data.Nat as ℕ
open import Data.Fin 
open import Function

data Tie {n : ℕ} (F : (Fin n → Set) → Fin n → Set) (k : Fin n) : Set where
  ⟨_⟩ : (v : F (Tie F) k) → Tie F k

_→̇_ : {n : ℕ} (F G : Fin n → Set) → Set
F →̇ G = ∀ {k} → F k → G k

tie : {n : ℕ} {T : Fin n → Set} {R : (Fin n → Set) → Fin n → Set}
      (fmap : ∀ {F G} → F →̇ G → R F →̇ R G) →
      (alg  : R T →̇ T) → {k : Fin n} (v : Tie R k) → T k
tie fmap alg ⟨ v ⟩ = alg $ fmap (tie fmap alg) v


data ForestF (L N : Set) (R : Fin 2 → Set) : Fin 2 → Set where
  Leaf : L                 → ForestF L N R (# 0)
  Node : N → R (# 1)       → ForestF L N R (# 0)
  Nil  :                     ForestF L N R (# 1)
  Cons : R (# 0) → R (# 1) → ForestF L N R (# 1)

Tree : (L N : Set) → Set
Tree L N = Tie (ForestF L N) (# 0)

Forest : (L N : Set) → Set
Forest L N = Tie (ForestF L N) (# 1)

leaf : {L N : Set} → L → Tree L N
leaf l = ⟨ Leaf l ⟩

node : {L N : Set} → N → Forest L N → Tree L N
node n ts = ⟨ Node n ts ⟩

nil : {L N : Set} → Forest L N
nil = ⟨ Nil ⟩

cons : {L N : Set} → Tree L N → Forest L N → Forest L N
cons t ts = ⟨ Cons t ts ⟩

mapForestF : {L N : Set} {F G : Fin 2 → Set} (f : F →̇ G) → ForestF L N F →̇ ForestF L N G
mapForestF f (Leaf l)    = Leaf l
mapForestF f (Node n ts) = Node n $ f ts
mapForestF f Nil         = Nil
mapForestF f (Cons t ts) = Cons (f t) $ f ts

numberLeaves : {L N : Set} → Tree L N → ℕ
numberLeaves {L} {N} = tie {T = const ℕ} mapForestF alg
  where
    alg : ForestF L N (const ℕ) →̇ const ℕ
    alg (Leaf _)    = 1
    alg (Node _ ts) = ts
    alg Nil         = 0
    alg (Cons t ts) = t ℕ.+ ts