Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Mutually Defined Datatypes
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment