MutualRecData.agda

{-# OPTIONS --safe --without-K #-}

-- using an inductive datatype (family) instead of El

module MutualRecData where

open import Agda.Primitive

open import Data.Nat.Base
  using (ℕ ; zero ; suc)
open import Data.Bool.Base
  using (Bool ; true ; false ; if_then_else_)
open import Data.List.Base
  using (List ; [] ; _∷_)
open import Data.Vec.Base
  using (Vec ; [] ; _∷_)

open import Data.Unit.Base
  using (⊤ ; tt)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.Sum.Base
  using (_⊎_ ; inj₁ ; inj₂)
open import Data.Product
  using (Σ ; Σ-syntax ; _×_ ; _,_ ; _,′_ ; -,_ ; proj₁ ; proj₂)

open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; subst ; sym ; trans)

syntax σ A (λ a → D) = σ[ a ∈ A ] D
syntax ρ j D = ρ[ j ] D

_⇉_ : ∀ {I : Set} → (I → Set) → (I → Set) → Set
X ⇉ Y = ∀ {i} → X i → Y i

data Desc (I : Set) : Set₁ where
  ι : (j : I) → Desc I
  _⊕_ : Desc I → Desc I → Desc I
  _⊗_ : Desc I → Desc I → Desc I
  σ : (A : Set) → (D : A → Desc I) → Desc I
  ρ : (j : I) → Desc I → Desc I

data Sem {I : Set} (D : Desc I) : (D′ : Desc I) → I → Set₁ where
  S-ι : ∀ {j i} → (eq : i ≡ j) → Sem D (ι j) i
  S-⊕₁ : ∀ {E F i} → Sem D E i → Sem D (E ⊕ F) i
  S-⊕₂ : ∀ {E F i} → Sem D F i → Sem D (E ⊕ F) i
  S-⊗ : ∀ {E F i} → Sem D E i → Sem D F i → Sem D (E ⊗ F) i
  S-σ : ∀ {A E i} → (a : A) → Sem D (E a) i → Sem D (σ A E) i
  S-ρ : ∀ {j E i} → Sem D D j → Sem D E i → Sem D (ρ j E) i

⟦_⟧ : ∀ {I} → Desc I → (I → Set) → (I → Set)
⟦ ι j   ⟧ X i = i ≡ j
⟦ D ⊕ E ⟧ X i = ⟦ D ⟧ X i ⊎ ⟦ E ⟧ X i
⟦ D ⊗ E ⟧ X i = ⟦ D ⟧ X i × ⟦ E ⟧ X i
⟦ σ A D ⟧ X i = Σ A (λ a → ⟦ D a ⟧ X i)
⟦ ρ j D ⟧ X i = X j × ⟦ D ⟧ X i

-- also, cannot use Sem here because that would not pass the positivity checker
data μ {I : Set} (D : Desc I) : I → Set where
  con : ⟦ D ⟧ (μ D) ⇉ μ D

VecBD : Desc ℕ
VecBD = ι 0 ⊕ (σ[ n ∈ ℕ ] σ[ a ∈ Bool ] ρ[ n ] ι(suc n))

VecB : ℕ → Set
VecB n = μ VecBD n

vecb→vec : ∀ {n} → VecB n → Vec Bool n
vecb→vec (con (inj₁ refl))                 = []
vecb→vec (con (inj₂ (n , b , vec , refl))) = b ∷ vecb→vec vec

vec→vecb : ∀ {n} → Vec Bool n → VecB n
vec→vecb {.zero} []       = con (inj₁ refl)
vec→vecb {suc n} (b ∷ bs) = con (inj₂ (n , b , vec→vecb bs , refl))

-- vecb→vec ∘ vec→vecb = id_VecBool
-- vec→vecb ∘ vecb→vec = id_Vecb

VecB′ : ℕ → Set₁
VecB′ n = Sem VecBD VecBD n

vecb′→vec : ∀ {n} → VecB′ n → Vec Bool n
vecb′→vec (S-⊕₁ (S-ι refl)) = []
vecb′→vec (S-⊕₂ (S-σ n (S-σ b (S-ρ r (S-ι refl))))) = b ∷ vecb′→vec r

vec→vecb′ : ∀ {n} → Vec Bool n → VecB′ n
vec→vecb′ {.zero} []       = S-⊕₁ (S-ι refl)
vec→vecb′ {suc n} (b ∷ bs) = S-⊕₂ (S-σ n (S-σ b (S-ρ (vec→vecb′ bs) (S-ι refl))))

remove-index : ∀ {I} → Desc I → Desc ⊤
remove-index (ι i)   = ι tt
remove-index (D ⊕ E) = remove-index D ⊕ remove-index E
remove-index (D ⊗ E) = remove-index D ⊗ remove-index E
remove-index (σ A D) = σ A (λ a → remove-index (D a))
remove-index (ρ i D) = ρ tt (remove-index D)

ListBND : Desc ⊤
ListBND = ι tt ⊕ (σ[ n ∈ ℕ ] σ[ a ∈ Bool ] ρ[ tt ] ι(tt))

ListBND-eq : remove-index VecBD ≡ ListBND
ListBND-eq = refl

mutual
  {-
  -- can't pass the termination checker under --without-K
  fold : ∀ {I X} → {D : Desc I} → ⟦ D ⟧ X ⇉ X → μ D ⇉ X
  fold {D = D} alg (con d) = alg (mapFold D alg d)

  mapFold : ∀ {I X D} → (D′ : Desc I) → ⟦ D ⟧ X ⇉ X → ⟦ D′ ⟧ (μ D) ⇉ ⟦ D′ ⟧ X
  mapFold (ι i) alg refl = refl
  mapFold (D ⊕ E) alg (inj₁ d) = inj₁ (mapFold D alg d)
  mapFold (D ⊕ E) alg (inj₂ e) = inj₂ (mapFold E alg e)
  mapFold (D ⊗ E) alg (d , e) = mapFold D alg d , mapFold E alg e
  mapFold (σ A D)  alg (a , d) = a , mapFold (D a) alg d
  mapFold (ρ i D)  alg (r , d) = fold alg r ,′ mapFold D alg d
  -}

  fold′ : ∀ {I X} → {D : Desc I} → ⟦ D ⟧ X ⇉ X → ∀ {i} → Sem D D i → X i
  fold′ alg sem = alg (mapFold′ alg sem)

  mapFold′ : ∀ {I} {X : I → Set} {D D′ : Desc I} → ∀ {i} → ⟦ D ⟧ X ⇉ X → Sem D D′ i → ⟦ D′ ⟧ X i
  mapFold′ alg (S-ι refl)     = refl
  mapFold′ alg (S-⊕₁ sem)     = inj₁ (mapFold′ alg sem)
  mapFold′ alg (S-⊕₂ sem)     = inj₂ (mapFold′ alg sem)
  mapFold′ alg (S-⊗ sem₁ sem₂) = mapFold′ alg sem₁ ,′ mapFold′ alg sem₂
  mapFold′ alg (S-σ a sem)    = a , mapFold′ alg sem
  mapFold′ alg (S-ρ semᵣ sem) = fold′ alg semᵣ ,′ mapFold′ alg sem

{-
mutual
  erase-idx-top : ∀ {I} → (D : Desc I) →
    ∀ {i} → μ D i → μ (remove-index D) tt
  erase-idx-top = {!!}

  erase-idx : ∀ {I} → (D′ : Desc I) → ∀ {i} → Sem D′ i → Sem (remove-index D′) tt
  erase-idx = {!!}
-}

MutualRecNonterm.agda

{-# OPTIONS --safe #-}

-- ordinary datatype-generic programming, require K for termination checking

module MutualRecNonterm where

open import Data.Nat.Base
  using (ℕ ; zero ; suc)
open import Data.Bool.Base
  using (Bool ; true ; false ; if_then_else_)
open import Data.List.Base
  using (List ; [] ; _∷_)
open import Data.Vec.Base
  using (Vec ; [] ; _∷_)

open import Data.Unit.Base
  using (⊤ ; tt)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.Sum.Base
  using (_⊎_ ; inj₁ ; inj₂)
open import Data.Product
  using (Σ ; Σ-syntax ; _×_ ; _,_ ; _,′_ ; -,_ ; proj₁ ; proj₂)

open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; subst ; sym ; trans)

syntax σ A (λ a → D) = σ[ a ∈ A ] D
syntax ρ j D = ρ[ j ] D

_⇉_ : ∀ {I : Set} → (I → Set) → (I → Set) → Set
X ⇉ Y = ∀ {i} → X i → Y i

data Desc (I : Set) : Set₁ where
  ι : (j : I) → Desc I
  _⊕_ : Desc I → Desc I → Desc I
  _⊗_ : Desc I → Desc I → Desc I
  σ : (A : Set) → (D : A → Desc I) → Desc I
  ρ : (j : I) → Desc I → Desc I

⟦_⟧ : ∀ {I} → Desc I → (I → Set) → (I → Set)
⟦ ι j   ⟧ X i = i ≡ j
⟦ D ⊕ E ⟧ X i = ⟦ D ⟧ X i ⊎ ⟦ E ⟧ X i
⟦ D ⊗ E ⟧ X i = ⟦ D ⟧ X i × ⟦ E ⟧ X i
⟦ σ A D ⟧ X i = Σ A (λ a → ⟦ D a ⟧ X i)
⟦ ρ j D ⟧ X i = X j × ⟦ D ⟧ X i

data μ {I : Set} (D : Desc I) : I → Set where
  con : ⟦ D ⟧ (μ D) ⇉ μ D

VecBD : Desc ℕ
VecBD = ι 0 ⊕ (σ[ n ∈ ℕ ] σ[ a ∈ Bool ] ρ[ n ] ι(suc n))

VecB : ℕ → Set
VecB n = μ VecBD n

vecb→vec : ∀ {n} → VecB n → Vec Bool n
vecb→vec (con (inj₁ refl))                 = []
vecb→vec (con (inj₂ (n , a , vec , refl))) = a ∷ vecb→vec vec

vec→vecb : ∀ {n} → Vec Bool n → VecB n
vec→vecb {.zero} []       = con (inj₁ refl)
vec→vecb {suc n} (a ∷ as) = con (inj₂ (n , a , vec→vecb as , refl))

-- vecb→vec ∘ vec→vecb = id_VecBool
-- vec→vecb ∘ vecb→vec = id_Vecb

remove-index : ∀ {I} → Desc I → Desc ⊤
remove-index (ι i)   = ι tt
remove-index (D ⊕ E) = remove-index D ⊕ remove-index E
remove-index (D ⊗ E) = remove-index D ⊗ remove-index E
remove-index (σ A D) = σ A (λ a → remove-index (D a))
remove-index (ρ i D) = ρ tt (remove-index D)

ListBND : Desc ⊤
ListBND = ι tt ⊕ (σ[ n ∈ ℕ ] σ[ a ∈ Bool ] ρ[ tt ] ι(tt))

ListBND-eq : remove-index VecBD ≡ ListBND
ListBND-eq = refl

mutual
  -- this definition (map and mapFold) requires K for the purpose of termination checking
  fold : ∀ {I X} → {D : Desc I} → ⟦ D ⟧ X ⇉ X → μ D ⇉ X
  fold {D = D} alg (con d) = alg (mapFold D alg d)

  mapFold : ∀ {I X D} → (D′ : Desc I) → ⟦ D ⟧ X ⇉ X → ⟦ D′ ⟧ (μ D) ⇉ ⟦ D′ ⟧ X
  mapFold (ι i) alg refl = refl
  mapFold (D ⊕ E) alg (inj₁ d) = inj₁ (mapFold D alg d)
  mapFold (D ⊕ E) alg (inj₂ e) = inj₂ (mapFold E alg e)
  mapFold (D ⊗ E) alg (d , e) = mapFold D alg d , mapFold E alg e
  mapFold (σ A D) alg (a , d) = a , mapFold (D a) alg d
  mapFold (ρ i D) alg (r , d) = fold alg r ,′ mapFold D alg d

mutual
  erase-idx-top : ∀ {I} → (D : Desc I) →
    ∀ {i} → μ D i → μ (remove-index D) tt
  erase-idx-top D (con d) = con (erase-idx D d)

  erase-idx : ∀ {I D} → (D′ : Desc I) → ∀ {i} → ⟦ D′ ⟧ (μ D) i → ⟦ remove-index D′ ⟧ (μ (remove-index D)) tt
  erase-idx (ι i)   refl     = refl
  erase-idx (D ⊕ E) (inj₁ d) = inj₁ (erase-idx D d) 
  erase-idx (D ⊕ E) (inj₂ e) = inj₂ (erase-idx E e)
  erase-idx (D ⊗ E) (d , e)  = erase-idx D d ,′ erase-idx E e
  erase-idx (σ A D) (a , d)  = a , erase-idx (D a) d
  erase-idx (ρ i D) (r , d)  = erase-idx-top _ r ,′ erase-idx D d