Rolling mutual data types

ChurchalPolySimple.agda

open import Data.Sum
open import Data.Nat.Base

mutual
  data M (A : Set) : Set where
    r : A -> M A
    n : N -> M A

  data N : Set where
    m : M ℕ -> N

{-# NO_POSITIVITY_CHECK #-}
data Fix {α β} {A : Set α} (B : (A -> Set β) -> A -> Set β) (x : A) : Set β where
  wrap : B (Fix B) x -> Fix B x

M⊎N : ((Set -> Set) -> Set -> Set) -> Set
M⊎N = Fix λ R choose -> choose
  (λ A -> A ⊎ R λ rM rN -> rN)
  (R λ rM rN -> rM ℕ)

M' : Set -> Set
M' A = M⊎N λ rM rN -> rM A

N' : Set
N' = M⊎N λ rM rN -> rN

mutual
  decodeM : ∀ {A} -> M' A -> M A
  decodeM (wrap (inj₁ x)) = r x
  decodeM (wrap (inj₂ y)) = n (decodeN y)

  decodeN : N' -> N
  decodeN (wrap y) = m (decodeM y)

mutual
  encodeM : ∀ {A} -> M A -> M' A
  encodeM (r x) = wrap (inj₁ x)
  encodeM (n y) = wrap (inj₂ (encodeN y))

  encodeN : N -> N'
  encodeN (m y) = wrap (encodeM y)

Churchual.agda

mutual
  data M (A : Set) : Set where
    r : A -> M A
    n : N A -> M A

  data N (A : Set) : Set where
    m : M A -> N A

open import Data.Sum

Bool = Set -> Set -> Set

true : Bool
true A B = A

false : Bool
false A B = B

if_then_else_ : Bool -> Set -> Set -> Set
if_then_else_ b = b

{-# NO_POSITIVITY_CHECK #-}
data Fix {α β} {A : Set α} (B : (A -> Set β) -> A -> Set β) (x : A) : Set β where
  wrap : B (Fix B) x -> Fix B x

-- `M` is `true`, `N` is `false`
M⊎N : Set -> Bool -> Set
M⊎N A = Fix λ R b -> if b then A ⊎ R false else R true

M' : Set -> Set
M' A = M⊎N A true

N' : Set -> Set
N' A = M⊎N A false

module _ {A : Set} where
  mutual
    forthM : M' A -> M A
    forthM (wrap (inj₁ x)) = r x
    forthM (wrap (inj₂ y)) = n (forthN y)

    forthN : N' A -> N A
    forthN (wrap y) = m (forthM y)

  mutual
    backM : M A -> M' A
    backM (r x) = wrap (inj₁ x)
    backM (n y) = wrap (inj₂ (backN y))

    backN : N A -> N' A
    backN (m y) = wrap (backM y)

Churchual.hs

{-# LANGUAGE PolyKinds #-}
data M a
  = R a
  | N (N a)

data N a
  = M (M a)

newtype ChurchTrue  a b = ChurchTrue a
newtype ChurchFalse a b = ChurchFalse b

data Fix (f :: (k -> *) -> k -> *) a
  = Fix (f (Fix f) a)

newtype ChooseMN a r b = ChooseMN (b (Either a (r ChurchFalse)) (r ChurchTrue))

type MN a = Fix (ChooseMN a)
type M' a = MN a ChurchTrue
type N' a = MN a ChurchFalse

forthM :: M' a -> M a
forthM (Fix (ChooseMN (ChurchTrue (Left  x)))) = R x
forthM (Fix (ChooseMN (ChurchTrue (Right y)))) = N (forthN y)

forthN :: N' a -> N a
forthN (Fix (ChooseMN (ChurchFalse y))) = M (forthM y)

backM :: M a -> M' a
backM (R x) = Fix (ChooseMN (ChurchTrue (Left   x       )))
backM (N y) = Fix (ChooseMN (ChurchTrue (Right (backN y))))

backN :: N a -> N' a
backN (M y) = Fix (ChooseMN (ChurchFalse (backM y)))

ChurchualN.agda

mutual
  data M (A : Set) : Set where
    mr : A -> M A
    mn : N A -> M A

  data N (A : Set) : Set where
    nm : M A -> N A
    np : P A -> N A

  data P (A : Set) : Set where
    pn : N A -> P A
    pp : P A -> P A

open import Function
open import Data.Sum

keep : {K : Set₁} -> (Set -> K) -> Set -> Set -> K
keep C A B = C B

skip : {K : Set₁} -> (Set -> K) -> Set -> Set -> K
skip C A B = C A

selector : {Keep Skip : Set₁} -> (Skip -> Keep) -> ((Set -> Set) -> Skip) -> Keep
selector keeps skips = keeps (skips id)

{-# NO_POSITIVITY_CHECK #-}
data Fix {α β} {A : Set α} (B : (A -> Set β) -> A -> Set β) (x : A) : Set β where
  wrap : B (Fix B) x -> Fix B x

M⊎N⊎P : Set -> (Set -> Set -> Set -> Set) -> Set
M⊎N⊎P A = Fix λ R select -> select
  (A ⊎ R (selector keep skip))
  (R (selector id (skip ∘ skip)) ⊎ R (selector (keep ∘ keep) id))
  (R (selector keep skip) ⊎ R (selector (keep ∘ keep) id))

M' : Set -> Set
M' A = M⊎N⊎P A (selector id (skip ∘ skip))

N' : Set -> Set
N' A = M⊎N⊎P A (selector keep skip)

P' : Set -> Set
P' A = M⊎N⊎P A (selector (keep ∘ keep) id)

module _ {A : Set} where
  mutual
    forthM : M' A -> M A
    forthM (wrap (inj₁ x)) = mr x
    forthM (wrap (inj₂ y)) = mn (forthN y)

    forthN : N' A -> N A
    forthN (wrap (inj₁ y)) = nm (forthM y)
    forthN (wrap (inj₂ y)) = np (forthP y)

    forthP : P' A -> P A
    forthP (wrap (inj₁ y)) = pn (forthN y)
    forthP (wrap (inj₂ y)) = pp (forthP y)

  mutual
    backM : M A -> M' A
    backM (mr x) = wrap (inj₁ x)
    backM (mn y) = wrap (inj₂ (backN y))

    backN : N A -> N' A
    backN (nm y) = wrap (inj₁ (backM y))
    backN (np y) = wrap (inj₂ (backP y))

    backP : P A -> P' A
    backP (pn y) = wrap (inj₁ (backN y))
    backP (pp y) = wrap (inj₂ (backP y))

ChurchualPoly.agda

open import Data.Sum
open import Data.List.Base

mutual
  data M (F : Set -> Set) (A : Set) : Set where
    r : F A -> M F A
    n : N A -> M F A

  data N (A : Set) : Set where
    m : M List A -> N A

{-# NO_POSITIVITY_CHECK #-}
data Fix {α β} {A : Set α} (B : (A -> Set β) -> A -> Set β) (x : A) : Set β where
  wrap : B (Fix B) x -> Fix B x

M⊎N : (((Set -> Set) -> Set -> Set) -> (Set -> Set) -> Set) -> Set
M⊎N = Fix λ R choose -> choose
  (λ F A -> F A ⊎ R λ rM rN -> rN A)
  (λ A -> R λ rM rN -> rM List A)

M' : (Set -> Set) -> Set -> Set
M' F A = M⊎N λ rM rN -> rM F A

N' : Set -> Set
N' A = M⊎N λ rM rN -> rN A

mutual
  decodeM : ∀ {F A} -> M' F A -> M F A
  decodeM (wrap (inj₁ x)) = r x
  decodeM (wrap (inj₂ y)) = n (decodeN y)

  decodeN : ∀ {A} -> N' A -> N A
  decodeN (wrap y) = m (decodeM y)

mutual
  encodeM : ∀ {F A} -> M F A -> M' F A
  encodeM (r x) = wrap (inj₁ x)
  encodeM (n y) = wrap (inj₂ (encodeN y))

  encodeN : ∀ {A} -> N A -> N' A
  encodeN (m y) = wrap (encodeM y)

DirectFix0.agda

{-# OPTIONS --type-in-type #-}

{-# NO_POSITIVITY_CHECK #-}
data IFix (A : Set) : ((A -> Set) -> A -> Set) -> A -> Set where
  iwrap : (F : (A -> Set) -> A -> Set) (x : A) -> F (IFix A F) x -> IFix A F x

Fix₀ : (Set -> Set) -> Set
Fix₀ = IFix (Set -> Set) (λ B F -> F (B F))

wrap₀ : (F : Set -> Set) -> F (Fix₀ F) -> Fix₀ F
wrap₀ = iwrap (λ B F -> F (B F))

module Test where
  open import Data.Maybe.Base

  module Nat where
    Nat : Set
    Nat = Fix₀ Maybe

    elimNat
        : {P : Nat -> Set}
        -> P (wrap₀ Maybe nothing)
        -> (∀ n -> P n -> P (wrap₀ Maybe (just n)))
        -> ∀ n
        -> P n
    elimNat z f (iwrap _ _  nothing) = z
    elimNat z f (iwrap _ _ (just n)) = f n (elimNat z f n)

exampleMNP.agda

{-# NO_POSITIVITY_CHECK #-}
data Fix {α β} {A : Set α} (B : (A -> Set β) -> A -> Set β) (x : A) : Set β where
  wrap : B (Fix B) x -> Fix B x

postulate
  M N P : Set -> Set -> Set -> Set

a b c : Set -> Set -> Set -> Set
a = λ x y z -> x
b = λ x y z -> y
c = λ x y z -> z

R : (Set -> Set -> Set -> Set) -> Set
R = Fix λ R select -> select
  (M (R a) (R b) (R c))
  (N (R a) (R b) (R c))
  (P (R a) (R b) (R c))

A = R a
B = R b
C = R c

isoM₁ : M A B C -> A
isoM₁ = wrap

isoM₂ : A -> M A B C
isoM₂ (wrap x) = x

isoN₁ : N A B C -> B
isoN₁ = wrap

isoN₂ : B -> N A B C
isoN₂ (wrap x) = x

isoP₁ : P A B C -> C
isoP₁ = wrap

isoP₂ : C -> P A B C
isoP₂ (wrap x) = x

examplePolyMNP.agda

{-# NO_POSITIVITY_CHECK #-}
data Fix {α β} {A : Set α} (B : (A -> Set β) -> A -> Set β) (x : A) : Set β where
  wrap : B (Fix B) x -> Fix B x

postulate
  M P : Set -> Set -> Set -> Set
  N : Set -> Set -> Set -> Set -> Set

data GX : Set where

R : (Set -> (Set -> Set) -> Set -> Set) -> Set
R = Fix λ R select -> select
  (       M   (R λ x y z -> x) (R λ x y z -> y GX) (R λ x y z -> z))
  (λ X -> N X (R λ x y z -> x) (R λ x y z -> y  X) (R λ x y z -> z))
  (       P   (R λ x y z -> x) (R λ x y z -> y GX) (R λ x y z -> z))

A =        R (λ x y z -> x)
B = λ X -> R (λ x y z -> y X)
C =        R (λ x y z -> z)

isoM₁ : M A (B GX) C -> A
isoM₁ = wrap

isoM₂ : A -> M A (B GX) C
isoM₂ (wrap x) = x

isoN₁ : ∀ {X} -> N X A (B X) C -> B X
isoN₁ = wrap

isoN₂ : ∀ {X} -> B X -> N X A (B X) C
isoN₂ (wrap x) = x

isoP₁ : P A (B GX) C -> C
isoP₁ = wrap

isoP₂ : C -> P A (B GX) C
isoP₂ (wrap x) = x

examplePolySimpleMNP.agda

-- Here we essentially encode the following:

-- open import Data.Product
--
-- postulate
--   Fix : ∀ {α} {A : Set α} -> (A -> A) -> A
--   M : Set -> Set -> Set
--   N : Set -> Set
--
-- M⊎N : (Set -> Set) × Set
-- M⊎N = Fix λ R -> (λ X -> M X (proj₁ R X)) , N (proj₂ R)
--
-- M' : Set -> Set
-- M' X = proj₁ M⊎N X
--
-- N' : Set
-- N' = proj₂ M⊎N

{-# NO_POSITIVITY_CHECK #-}
data Fix {α β} {A : Set α} (B : (A -> Set β) -> A -> Set β) (x : A) : Set β where
  wrap : B (Fix B) x -> Fix B x

postulate
  M : Set -> Set -> Set
  N : Set -> Set

-- Just the Church-encoded version of `M⊎N : (Set -> Set) × Set`.
M⊎N : ((Set -> Set) -> Set -> Set) -> Set
M⊎N = Fix λ R choose -> choose
  (λ X -> M X (R λ m n -> m X))
  (N (R λ m n -> n))

A = λ X -> M⊎N λ m _ -> m X
B = M⊎N λ _ n -> n

isoM₁ : ∀ {X} -> M X (A X) -> A X
isoM₁ = wrap

isoM₂ : ∀ {X} -> A X -> M X (A X)
isoM₂ (wrap x) = x

isoN₁ : N B -> B
isoN₁ = wrap

isoN₂ : B -> N B
isoN₂ (wrap x) = x

IFixN.agda

{-# OPTIONS --type-in-type #-}

{-# NO_POSITIVITY_CHECK #-}
data Fix₁ {A : Set} (F : (A -> Set) -> A -> Set) (x : A) : Set where
  wrap : F (Fix₁ F) x -> Fix₁ F x

module Direct where
  Fix₀ : (Set -> Set) -> Set
  Fix₀ F = Fix₁ (λ B _A -> F (B _A)) Set

  Fix₂ : ∀ {A B} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  Fix₂ F x y = Fix₁ (λ B P -> P (F λ x y -> B λ R -> R x y)) (λ R -> R x y)

  Fix₃ : ∀ {A B C} -> ((A -> B -> C -> Set) -> A -> B -> C -> Set) -> A -> B -> C -> Set
  Fix₃ F x y z = Fix₁ (λ B P -> P (F λ x y z -> B λ R -> R x y z)) (λ R -> R x y z)

module Generic where
  FixBy : ∀ {Rep} -> (((Rep -> Set) -> Set) -> Rep) -> (Rep -> Rep) -> Rep
  FixBy withSpine F = withSpine (Fix₁ λ B P -> P (F (withSpine B)))

  Fix₀ : (Set -> Set) -> Set
  Fix₀ = FixBy λ K -> K λ x -> x

  Fix₂ : ∀ {A B} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  Fix₂ = FixBy λ K x y -> K λ R -> R x y

  Fix₃ : ∀ {A B C} -> ((A -> B -> C -> Set) -> A -> B -> C -> Set) -> A -> B -> C -> Set
  Fix₃ = FixBy λ K x y z -> K λ R -> R x y z

module Test where
  open import Data.Maybe.Base
  open Generic

  module Nat where
    Nat : Set
    Nat = Fix₀ Maybe

    pattern zero  = wrap nothing
    pattern suc n = wrap (just n)

    elimNat
        : {P : Nat -> Set}
        -> P zero
        -> (∀ n -> P n -> P (suc n))
        -> ∀ n
        -> P n
    elimNat z f  zero   = z
    elimNat z f (suc n) = f n (elimNat z f n)

  module List where
    data ListF (R : Set -> Set) A : Set where
      nilF  : ListF R A
      consF : A -> R A -> ListF R A

    List : Set -> Set
    List = Fix₁ ListF

    pattern []       = wrap nilF
    pattern _∷_ x xs = wrap (consF x xs)

    elimList
        : ∀ {A} {P : List A -> Set}
        -> P []
        -> (∀ x xs -> P xs -> P (x ∷ xs))
        -> ∀ xs
        -> P xs
    elimList z f  []      = z
    elimList z f (x ∷ xs) = f x xs (elimList z f xs)

  module InterleavedList where
    open import Data.Unit.Base
    open import Data.Sum.Base
    open import Data.Product

    InterleavedList : Set -> Set -> Set
    InterleavedList = Fix₂ λ R A B -> ⊤ ⊎ A × B × R B A

    pattern []          = wrap (inj₁ tt)
    pattern cons x y ps = wrap (inj₂ (x , y , ps))

    elimInterleavedList
        : ∀ {A B} {P : ∀ {A B} -> InterleavedList A B -> Set}
        -> (∀ {A B} -> P {A} {B} [])
        -> (∀ {A B} x y ps -> P {A} {B} ps -> P (cons x y ps))
        -> ∀ ps
        -> P {A} {B} ps
    elimInterleavedList z f  []           = z
    elimInterleavedList z f (cons x y ps) = f x y ps (elimInterleavedList z f ps)

IFixNat.agda

open import Data.Maybe.Base

{-# NO_POSITIVITY_CHECK #-}
data IFix {α β} {A : Set α} (B : (A -> Set β) -> A -> Set β) (x : A) : Set β where
  wrap : B (IFix B) x -> IFix B x

Fix : ∀ {α} -> (Set α -> Set α) -> Set α
Fix F = IFix (λ B ⊥ -> F (B ⊥)) ((A : Set) -> A)

Nat : Set
Nat = Fix Maybe

pattern zero  = wrap nothing
pattern suc n = wrap (just n)

elimNat : ∀ {π} {P : Nat -> Set π}
        -> P zero
        -> (∀ n -> P n -> P (suc n))
        -> ∀ n
        -> P n
elimNat z f  zero   = z
elimNat z f (suc n) = f n (elimNat z f n)

Mutual.agda

mutual
  data M (A : Set) : Set where
    r : A -> M A
    n : N A -> M A

  data N (A : Set) : Set where
    m : M A -> N A

open import Data.Bool.Base
open import Data.Sum

{-# NO_POSITIVITY_CHECK #-}
data Fix {A : Set} (B : (A -> Set) -> A -> Set) (x : A) : Set where
  wrap : B (Fix B) x -> Fix B x

-- `M` is `true`, `N` is `false`
M⊎N : Set -> Bool -> Set
M⊎N A = Fix λ R b -> if b then A ⊎ R false else R true

M' : Set -> Set
M' A = M⊎N A true

N' : Set -> Set
N' A = M⊎N A false

module _ {A : Set} where
  mutual
    forthM : M' A -> M A
    forthM (wrap (inj₁ x)) = r x
    forthM (wrap (inj₂ y)) = n (forthN y)

    forthN : N' A -> N A
    forthN (wrap y) = m (forthM y)

  mutual
    backM : M A -> M' A
    backM (r x) = wrap (inj₁ x)
    backM (n y) = wrap (inj₂ (backN y))

    backN : N A -> N' A
    backN (m y) = wrap (backM y)

TreeForestPlcStyle.agda

{-# OPTIONS --type-in-type #-}

{-# NO_POSITIVITY_CHECK #-}
data IFix {A : Set} (F : (A -> Set) -> A -> Set) (x : A) : Set where
  wrap : F (IFix F) x -> IFix F x

Fix₂ : ∀ {A B} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
Fix₂ F x y = IFix (λ B P -> P (F λ x y -> B λ R -> R x y)) (λ R -> R x y)

module Direct where
  mutual
    data Tree₀ (A : Set) : Set where
      node₀ : A -> Forest₀ A -> Tree₀ A

    data Forest₀ (A : Set) : Set where
      nil₀  : Forest₀ A
      cons₀ : Tree₀ A -> Forest₀ A -> Forest₀ A
open Direct

module Common where
  treeTag : Set -> Set -> Set
  treeTag T F = T

  forestTag : Set -> Set -> Set
  forestTag T F = F

  AsTree : (Set -> (Set -> Set -> Set) -> Set) -> Set -> Set
  AsTree D A = D A treeTag

  AsForest : (Set -> (Set -> Set -> Set) -> Set) -> Set -> Set
  AsForest D A = D A forestTag
open Common

module Encoded where
  open import Data.Unit.Base
  open import Data.Sum.Base
  open import Data.Product

  TreeForest : Set -> (Set -> Set -> Set) -> Set
  TreeForest =
    Fix₂ λ Rec A tag ->
      tag
        (A × AsForest Rec A)
        (⊤ ⊎ AsTree Rec A × AsForest Rec A)

  Tree : Set -> Set
  Tree = AsTree TreeForest

  Forest : Set -> Set
  Forest = AsForest TreeForest

module ScottEncoded where
  TreeForest : Set -> (Set -> Set -> Set) -> Set
  TreeForest =
    Fix₂ λ Rec A tag ->
      ∀ R -> tag ((A -> AsForest Rec A -> R) -> R) (R -> (AsTree Rec A -> AsForest Rec A -> R) -> R)

  Tree : Set -> Set
  Tree = AsTree TreeForest

  Forest : Set -> Set
  Forest = AsForest TreeForest

  {-# TERMINATING #-}
  mutual
    toTree₀ : ∀ A -> Tree A -> Tree₀ A
    toTree₀ A (wrap match) =
      match (Tree₀ A) λ x forest ->
        node₀ x (toForest₀ A forest)

    toForest₀ : ∀ A -> Forest A -> Forest₀ A
    toForest₀ A (wrap match) =
      match (Forest₀ A) nil₀ λ tree forest ->
        cons₀ (toTree₀ A tree) (toForest₀ A forest)

  mutual
    fromTree₀ : ∀ A -> Tree₀ A -> Tree A
    fromTree₀ A (node₀ x forest) =
      wrap λ R f -> f x (fromForest₀ A forest)

    fromForest₀ : ∀ A -> Forest₀ A -> Forest A
    fromForest₀ A  nil₀               =
      wrap λ R z f -> z
    fromForest₀ A (cons₀ tree forest) =
      wrap λ R z f -> f (fromTree₀ A tree) (fromForest₀ A forest)