Mutual term-level recursion

MutualFix.agda

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

fstFun : ∀ {A B} -> A -> B -> A
fstFun x _ = x

sndFun : ∀ {A B} -> A -> B -> B
sndFun _ y = y

uncurryFun : ∀ {A B C} -> (A -> B -> C) -> (∀ {R} -> (A -> B -> R) -> R) -> C
uncurryFun f k = f (k fstFun) (k sndFun)

{-# TERMINATING #-}
fix2 : ∀ {A B R} -> (A -> B -> A) -> (A -> B -> B) -> (A -> B -> R) -> R
fix2 f g k = k (uncurryFun f (fix2 f g)) (uncurryFun g (fix2 f g))

open import Data.Bool.Base
open import Data.Nat.Base

evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
evenAndOdd = fix2
  (λ even odd -> λ { 0 -> true  ; (suc n) -> odd  n })
  (λ even odd -> λ { 0 -> false ; (suc n) -> even n })

even = evenAndOdd fstFun
odd  = evenAndOdd sndFun

open import Relation.Binary.PropositionalEquality
open import Data.List.Base

testEven : map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
         ≡ (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ [])
testEven = refl

testOdd : map odd (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
        ≡ (false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ [])
testOdd = refl

MutualFixGeneric.agda

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

open import Function

{-# TERMINATING #-}
fixN : ∀ {F : Set -> Set} {R}
     -> (∀ {R} -> (∀ {Q} -> F Q -> Q) -> F R -> R)
     -> (∀ {Q} -> F Q -> F Q) -> F R -> R
fixN {F} selfCotraverse h = loop where
  loop : ∀ {R} -> F R -> R
  loop = selfCotraverse (loop ∘ h)

{-# TERMINATING #-}
fix2 : ∀ {A B R} -> (∀ {Q} -> (A -> B -> Q) -> A -> B -> Q) -> (A -> B -> R) -> R
fix2 = fixN λ k f -> f (k λ x y -> x) (k λ x y -> y)

{-# TERMINATING #-}
fix3 : ∀ {A B C R} -> (∀ {Q} -> (A -> B -> C -> Q) -> A -> B -> C -> Q) -> (A -> B -> C -> R) -> R
fix3 = fixN λ k f -> f (k λ x y z -> x) (k λ x y z -> y) (k λ x y z -> z)

open import Data.Bool.Base
open import Data.Nat.Base

evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
evenAndOdd = fix2 λ choose even odd -> choose
  (λ { 0 -> true  ; (suc n) -> odd  n })
  (λ { 0 -> false ; (suc n) -> even n })

even = evenAndOdd λ x y -> x
odd  = evenAndOdd λ x y -> y

open import Relation.Binary.PropositionalEquality
open import Data.List.Base

testEven : map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
         ≡ (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ [])
testEven = refl

testOdd : map odd (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
        ≡ (false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ [])
testOdd = refl

MutualFixGenericCompute.agda

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

open import Function
open import Data.Nat.Base

RecPattern : (Set -> Set) -> Set
RecPattern F = ∀ {R} -> (∀ {Q} -> F Q -> Q) -> F R -> R

FixPattern : (Set -> Set) -> Set
FixPattern F = ∀ {R} -> (∀ {Q} -> F Q -> F Q) -> F R -> R

{-# TERMINATING #-}
fixRec : ∀ {F} -> RecPattern F -> FixPattern F
fixRec rec h = rec (fixRec rec h ∘ h)

FixOver : ((Set -> Set) -> Set) -> ℕ -> Set
FixOver K  0      = K id
FixOver K (suc n) = ∀ {A} -> FixOver (λ F -> K λ X -> A -> F X) n

hoistFixOver : ∀ {K L} n -> (∀ {F} -> K F -> L F) -> FixOver K n -> FixOver L n
hoistFixOver  0      h f = h f
hoistFixOver (suc n) h f = hoistFixOver n h f

FixN : ℕ -> Set
FixN = FixOver FixPattern

RecN : ℕ -> Set
RecN = FixOver RecPattern

bump : ∀ {F A}
     -> (∀ {Q} -> F Q -> F (A -> Q))
     -> (∀ {R} -> F (A -> R) -> A -> F R)
     -> F (A -> A)
     -> RecPattern F
     -> RecPattern λ X -> F (A -> X)
bump skip keep last r k f = r (k ∘ skip) (keep f $ k last)

fixOverBump : ∀ {K} n
            -> (bump : ∀ {F A}
                     -> (∀ {Q} -> F Q -> F (A -> Q))
                     -> (∀ {R} -> F (A -> R) -> A -> F R)
                     -> F (A -> A)
                     -> K F
                     -> K λ X -> F (A -> X))
            -> K id
            -> FixOver K n
fixOverBump  0      bump z = z
fixOverBump (suc n) bump z = fixOverBump n
  (λ skip keep last -> bump (λ g y -> skip (g y)) (λ g x y -> keep (g y) x) (λ _ -> last))
  (bump {id} const _$_ id z)

recN : ∀ n -> RecN n
recN n = fixOverBump n bump (λ _ f -> f)

fixN : ∀ n -> FixN n
fixN n = hoistFixOver n fixRec (recN n)







fix2 : FixN 2
fix2 = fixN 2

fix3 : FixN 3
fix3 = fixN 3

-- `fix3` is the same as
fix3′ : ∀ {A B C R} -> (∀ {Q} -> (A -> B -> C -> Q) -> A -> B -> C -> Q) -> (A -> B -> C -> R) -> R
fix3′ = fixRec λ k f -> f (k λ x y z -> x) (k λ x y z -> y) (k λ x y z -> z)

open import Data.Bool.Base
open import Data.Nat.Base

evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
evenAndOdd = fix2 λ choose even odd -> choose
  (λ { 0 -> true  ; (suc n) -> odd  n })
  (λ { 0 -> false ; (suc n) -> even n })

even = evenAndOdd λ x y -> x
odd  = evenAndOdd λ x y -> y

open import Relation.Binary.PropositionalEquality
open import Data.List.Base

testEven : map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
         ≡ (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ [])
testEven = refl

testOdd : map odd (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
        ≡ (false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ [])
testOdd = refl

MutualFixGenericComputeNonDep.agda

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

open import Function

NAT : Set
NAT = ((((Set -> Set) -> Set) -> Set) -> ((Set -> Set) -> Set) -> Set)
   -> (((Set -> Set) -> Set) -> Set)
   -> ((Set -> Set) -> Set)
   -> Set

Zero : NAT
Zero = λ F Z -> Z

Suc : NAT -> NAT
Suc N = λ F Z -> F (N F Z)

SNat : NAT -> Set
SNat N = (P : NAT -> Set) -> (∀ {M} -> P M -> P (Suc M)) -> P Zero -> P N

szero : SNat Zero
szero = λ P f z -> z

ssuc : ∀ {N} -> SNat N -> SNat (Suc N)
ssuc sn = λ P f z -> f (sn P f z)

RecPattern : (Set -> Set) -> Set
RecPattern F = ∀ {R} -> (∀ {Q} -> F Q -> Q) -> F R -> R

FixPattern : (Set -> Set) -> Set
FixPattern F = ∀ {R} -> (∀ {Q} -> F Q -> F Q) -> F R -> R

{-# TERMINATING #-}
fixRec : ∀ {F} -> RecPattern F -> FixPattern F
fixRec rec h = rec (fixRec rec h ∘ h)

FixOver : ((Set -> Set) -> Set) -> NAT -> Set
FixOver F N = N (λ r K -> ∀ {A} -> r (λ F -> K λ X -> A -> F X)) (λ K -> K id) F

hoistFixOver : ∀ {N} -> SNat N -> ∀ {K L} -> (∀ {F} -> K F -> L F) -> FixOver K N -> FixOver L N
hoistFixOver sn = sn
  (λ N -> ∀ {K L} -> (∀ {F} -> K F -> L F) -> FixOver K N -> FixOver L N)
  (λ r h f -> r h f)
  (λ h f -> h f)

FixN : NAT -> Set
FixN = FixOver FixPattern

RecN : NAT -> Set
RecN = FixOver RecPattern

Bump : ((Set -> Set) -> Set) -> Set
Bump K = ∀ {F A}
       -> (∀ {Q} -> F Q -> F (A -> Q))
       -> (∀ {R} -> F (A -> R) -> A -> F R)
       -> F (A -> A)
       -> K F
       -> K λ X -> F (A -> X)

bump : Bump RecPattern
bump skip keep last r k f = r (k ∘ skip) (keep f $ k last)

fixOverBump : ∀ {N} -> SNat N -> ∀ {K} -> Bump K -> K id -> FixOver K N
fixOverBump {K} sn = sn
  (λ N -> ∀ {K} -> Bump K -> K id -> FixOver K N)
  (λ r bump z -> r
    (λ skip keep last -> bump (λ g y -> skip (g y)) (λ g x y -> keep (g y) x) (λ _ -> last))
    (bump {id} const _$_ id z))
  (λ _ z -> z)

recN : ∀ {N} -> SNat N -> RecN N
recN sn = fixOverBump sn bump (λ _ f -> f)

fixN : ∀ {N} -> SNat N -> FixN N
fixN sn = hoistFixOver sn fixRec (recN sn)

fix2 : FixN (Suc (Suc Zero))
fix2 = fixN (ssuc (ssuc szero))

fix3 : FixN (Suc (Suc (Suc Zero)))
fix3 = fixN (ssuc (ssuc (ssuc szero)))

-- `fix3` is the same as
fix3′ : ∀ {A B C R} -> (∀ {Q} -> (A -> B -> C -> Q) -> A -> B -> C -> Q) -> (A -> B -> C -> R) -> R
fix3′ = fixRec λ k f -> f (k λ x y z -> x) (k λ x y z -> y) (k λ x y z -> z)

open import Data.Bool.Base
open import Data.Nat.Base

evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
evenAndOdd = fix2 λ choose even odd -> choose
  (λ { 0 -> true  ; (suc n) -> odd  n })
  (λ { 0 -> false ; (suc n) -> even n })

even = evenAndOdd λ x y -> x
odd  = evenAndOdd λ x y -> y

open import Relation.Binary.PropositionalEquality
open import Data.List.Base

testEven : map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
         ≡ (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ [])
testEven = refl

testOdd : map odd (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
        ≡ (false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ [])
testOdd = refl

MutualFixGenericHigherElaborated.agda

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

open import Function

{-# TERMINATING #-}
hfix : ∀ (F G : Set -> Set) S -> (∀ R -> (∀ Q -> F Q -> G Q) -> F R -> G R) -> F S -> G S
hfix F G S f = f S (λ Q -> hfix F G Q f)

fixBy : ∀ F R -> (∀ S -> (∀ Q -> F Q -> Q) -> F S -> S) -> (∀ Q -> F Q -> F Q) -> F R -> R
fixBy F R by h = hfix F id R (λ T rec t -> by T (λ Q q -> rec Q (h Q q)) t)

fix2 : ∀ A B R -> (∀ Q -> (A -> B -> Q) -> A -> B -> Q) -> (A -> B -> R) -> R
fix2 A B R = fixBy (λ X -> A -> B -> X) R (λ S k f -> f (k A (λ x y -> x)) (k B (λ x y -> y)))



open import Data.Bool.Base
open import Data.Nat.Base

evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
evenAndOdd = fix2 _ _ _ λ _ choose even odd -> choose
  (λ { 0 -> true  ; (suc n) -> odd  n })
  (λ { 0 -> false ; (suc n) -> even n })

even = evenAndOdd λ x y -> x
odd  = evenAndOdd λ x y -> y

open import Relation.Binary.PropositionalEquality
open import Data.List.Base

testEven : map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
         ≡ (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ [])
testEven = refl

testOdd : map odd (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
        ≡ (false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ [])
testOdd = refl

MutualFixUniform.agda

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

fstFun : ∀ {A B} -> A -> B -> A
fstFun x _ = x

sndFun : ∀ {A B} -> A -> B -> B
sndFun _ y = y

uncurryFun : ∀ {A B C} -> (A -> B -> C) -> (∀ {R} -> (A -> B -> R) -> R) -> C
uncurryFun f k = f (k fstFun) (k sndFun)

{-# TERMINATING #-}
fix2 : ∀ {A B R} -> (∀ {Q} -> (A -> B -> Q) -> A -> B -> Q) -> (A -> B -> R) -> R
fix2 h k = k (uncurryFun (h fstFun) (fix2 h)) (uncurryFun (h sndFun) (fix2 h))

-- fixN : ∀ {F : Set -> Set} {R} -> (∀ {Q} -> F Q -> F Q) -> F R -> R

open import Data.Bool.Base
open import Data.Nat.Base

evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
evenAndOdd = fix2 λ choose even odd -> choose
  (λ { 0 -> true  ; (suc n) -> odd  n })
  (λ { 0 -> false ; (suc n) -> even n })

even = evenAndOdd fstFun
odd  = evenAndOdd sndFun

open import Relation.Binary.PropositionalEquality
open import Data.List.Base

testEven : map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
         ≡ (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ [])
testEven = refl

testOdd : map odd (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
        ≡ (false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ [])
testOdd = refl

MutualStrictFix.hs

apply :: (a -> b) -> a -> b
apply = ($!)

fstFun :: a -> b -> a
fstFun x _ = x

sndFun :: a -> b -> b
sndFun _ y = y

fix2
    :: ((a1 -> b1) -> (a2 -> b2) -> a1 -> b1)
    -> ((a1 -> b1) -> (a2 -> b2) -> a2 -> b2)
    -> ((a1 -> b1) -> (a2 -> b2) -> r) -> r
fix2 f g k = k
    (\x1 -> f `apply` fix2 f g fstFun `apply` fix2 f g sndFun `apply` x1)
    (\x2 -> g `apply` fix2 f g fstFun `apply` fix2 f g sndFun `apply` x2)

evenAndOdd' :: ((Int -> Bool) -> (Int -> Bool) -> r) -> r
evenAndOdd' = fix2 (\even odd n -> n == 0 || odd  (n - 1))
                   (\even odd n -> n /= 0 && even (n - 1))

even' = evenAndOdd' fstFun
odd'  = evenAndOdd' sndFun

main = print $
       map even' [0..5] == [True , False, True , False, True , False]
    && map odd'  [0..5] == [False, True , False, True , False, True]

MutualStrictFixByFix.hs

{-# LANGUAGE RankNTypes #-}

apply :: (a -> b) -> a -> b
apply = ($!)

fstFun :: a -> b -> a
fstFun x _ = x

sndFun :: a -> b -> b
sndFun _ y = y

fix :: ((a -> b) -> a -> b) -> a -> b
fix f = f (\x -> fix f $! x)

newtype With2 a b = With2
    { unWith2 :: forall r. (a -> b -> r) -> r
    }

fix2
    :: ((a1 -> b1) -> (a2 -> b2) -> a1 -> b1)
    -> ((a1 -> b1) -> (a2 -> b2) -> a2 -> b2)
    -> ((a1 -> b1) -> (a2 -> b2) -> r) -> r
fix2 f0 g0 = unWith2 $ fix
    (\r f g -> With2 $ \k -> k
        (\x -> f `apply` unWith2 (r f g) fstFun `apply` unWith2 (r f g) sndFun `apply` x)
        (\y -> g `apply` unWith2 (r f g) fstFun `apply` unWith2 (r f g) sndFun `apply` y))
    f0
    g0

evenAndOdd' :: ((Int -> Bool) -> (Int -> Bool) -> r) -> r
evenAndOdd' = fix2 (\even odd n -> n == 0 || odd  (n - 1))
                   (\even odd n -> n /= 0 && even (n - 1))

even' = evenAndOdd' fstFun
odd'  = evenAndOdd' sndFun

main = print $
       map even' [0..5] == [True , False, True , False, True , False]
    && map odd'  [0..5] == [False, True , False, True , False, True]

MutualStrictFixGenericElaborated.agda

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

{-# TERMINATING #-}
fix : ∀ {A B} -> ((A -> B) -> A -> B) -> A -> B
fix f = f (λ x -> f (fix f) x)

fixBy =
  λ {F : Set -> Set} ->
  λ (by : ({Q : Set} -> F Q -> Q) -> {S : Set} -> F S -> S) ->
    fix {∀ {Q : Set} -> F Q -> F Q} {∀ {R : Set} -> F R -> R}
      (λ (rec : ({Q : Set} -> F Q -> F Q) -> {R : Set} -> F R -> R) ->
       λ (h   : {Q : Set} -> F Q -> F Q) ->
       λ {R : Set} ->
       λ (r : F R) ->
         by
           (λ {Q : Set} -> λ (q : F Q) -> rec h {Q} (h {Q} q))
           {R}
           r)

fix2 =
  λ {A₁ B₁ A₂ B₂ : Set} ->
    fixBy {λ (X : Set) -> (A₁ -> B₁) -> (A₂ -> B₂) -> X}
      (λ (k : {Q : Set} -> ((A₁ -> B₁) -> (A₂ -> B₂) -> Q) -> Q) ->
       λ {S} ->
       λ (h : (A₁ -> B₁) -> (A₂ -> B₂) -> S) ->
         h
           (λ (x₁ : A₁) -> k {B₁} (λ (f₁ : A₁ -> B₁) (f₂ : A₂ -> B₂) -> f₁ x₁))
           (λ (x₂ : A₂) -> k {B₂} (λ (f₁ : A₁ -> B₁) (f₂ : A₂ -> B₂) -> f₂ x₂)))



open import Data.Bool.Base
open import Data.Nat.Base

evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
evenAndOdd = fix2 {ℕ} {Bool} {ℕ} {Bool} λ choose even odd -> choose
  (λ { 0 -> true  ; (suc n) -> odd  n })
  (λ { 0 -> false ; (suc n) -> even n })

even = evenAndOdd λ x y -> x
odd  = evenAndOdd λ x y -> y

open import Relation.Binary.PropositionalEquality
open import Data.List.Base

testEven : map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
         ≡ (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ [])
testEven = refl

testOdd : map odd (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
        ≡ (false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ [])
testOdd = refl

MutualStrictFixGenericHigherElaborated.agda

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

open import Function

{-# TERMINATING #-}
hfix : ∀ (F G : Set -> Set) S -> (∀ R -> (∀ Q -> F Q -> G Q) -> F R -> G R) -> F S -> G S
hfix F G S f = f S (λ Q q -> hfix F G Q f q)

fixBy : ∀ F R -> (∀ S -> (∀ Q -> F Q -> Q) -> F S -> S) -> (∀ Q -> F Q -> F Q) -> F R -> R
fixBy F R by h = hfix F id R (λ T rec t -> by T (λ Q q -> rec Q (h Q q)) t)

fix2 : ∀ A₁ B₁ A₂ B₂ R
     -> (∀ Q -> ((A₁ -> B₁) -> (A₂ -> B₂) -> Q) -> (A₁ -> B₁) -> (A₂ -> B₂) -> Q)
     -> ((A₁ -> B₁) -> (A₂ -> B₂) -> R)
     -> R
fix2 A₁ B₁ A₂ B₂ R = fixBy
  (λ X -> (A₁ -> B₁) -> (A₂ -> B₂) -> X)
  R
  (λ S k h -> h (λ x₁ -> k B₁ (λ f₁ f₂ -> f₁ $! x₁)) (λ x₂ -> k B₂ (λ f₁ f₂ -> f₂ $! x₂)))



open import Data.Bool.Base
open import Data.Nat.Base

evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
evenAndOdd {R} = fix2 ℕ Bool ℕ Bool R λ _ choose even odd -> choose
  (λ { 0 -> true  ; (suc n) -> odd  n })
  (λ { 0 -> false ; (suc n) -> even n })

even = evenAndOdd λ x y -> x
odd  = evenAndOdd λ x y -> y

open import Relation.Binary.PropositionalEquality
open import Data.List.Base

testEven : map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
         ≡ (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ [])
testEven = refl

testOdd : map odd (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
        ≡ (false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ [])
testOdd = refl

MutualStrictFixGenericHigherElaboratedSelf.agda

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

open import Function

{-# NO_POSITIVITY_CHECK #-}
data Fix (F : Set -> Set) : Set where
  Wrap : F (Fix F) -> Fix F

-- The same trickery that the usual `fix` uses.
data SelfF A R : Set where
  selfF : (R -> A) -> SelfF A R

Self : Set -> Set
Self A = Fix (SelfF A)

pattern self f = Wrap (selfF f)

unfold : ∀ A -> Self A -> Self A -> A
unfold A (self f) = f

unroll : ∀ A -> Self A -> A
unroll A s = unfold A s s

{-# TERMINATING #-}
hfix : ∀ (F G : Set -> Set) S -> (∀ R -> (∀ Q -> F Q -> G Q) -> F R -> G R) -> F S -> G S
hfix F G S f =
  unroll (∀ Q -> F Q -> G Q) (self (λ knot Q q -> (f Q $! unroll (∀ Q -> F Q -> G Q) knot) $! q)) S

fixBy : ∀ F R -> (∀ S -> (∀ Q -> F Q -> Q) -> F S -> S) -> (∀ Q -> F Q -> F Q) -> F R -> R
fixBy F R by h = hfix F (λ X -> X) R (λ T rec t -> by T (λ Q q -> rec Q $! h Q q) $! t)

fix2 : ∀ A₁ B₁ A₂ B₂ R
     -> (∀ Q -> ((A₁ -> B₁) -> (A₂ -> B₂) -> Q) -> (A₁ -> B₁) -> (A₂ -> B₂) -> Q)
     -> ((A₁ -> B₁) -> (A₂ -> B₂) -> R)
     -> R
fix2 A₁ B₁ A₂ B₂ R = fixBy
  (λ X -> (A₁ -> B₁) -> (A₂ -> B₂) -> X)
  R
  (λ S k h -> h (λ x₁ -> k B₁ (λ f₁ f₂ -> f₁ $! x₁)) (λ x₂ -> k B₂ (λ f₁ f₂ -> f₂ $! x₂)))



open import Data.Bool.Base
open import Data.Nat.Base

evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
evenAndOdd {R} = fix2 ℕ Bool ℕ Bool R λ _ choose even odd -> choose
  (λ { 0 -> true  ; (suc n) -> odd  n })
  (λ { 0 -> false ; (suc n) -> even n })

even = evenAndOdd λ x y -> x
odd  = evenAndOdd λ x y -> y

open import Relation.Binary.PropositionalEquality
open import Data.List.Base

testEven : map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
         ≡ (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ [])
testEven = refl

testOdd : map odd (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
        ≡ (false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ [])
testOdd = refl

MutualStrictFixGenericHigherElaboratedSelfImplicits.agda

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

open import Function

{-# NO_POSITIVITY_CHECK #-}
data Fix (F : Set -> Set) : Set where
  Wrap : F (Fix F) -> Fix F

-- The same trickery that the usual `fix` uses.
data SelfF A R : Set where
  selfF : (R -> A) -> SelfF A R

Self : Set -> Set
Self A = Fix (SelfF A)

pattern self f = Wrap (selfF f)

unfold : ∀ {A} -> Self A -> Self A -> A
unfold (self f) = f

unroll : ∀ {A} -> Self A -> A
unroll s = unfold s s

hfix =
  λ {F G : Set -> Set} {S : Set} ->
    λ (f : {R : Set} -> ({Q : Set} -> F Q -> G Q) -> F R -> G R) ->
      unroll {∀ {Q : Set} -> F Q -> G Q}
        (self (λ (knot : Self ({Q : Set} -> F Q -> G Q)) -> λ {Q : Set} -> λ (q : F Q) ->
          (f {Q} (unroll {∀ {Q : Set} -> F Q -> G Q} knot) q)))
        {S}

fixBy =
  λ {F : Set -> Set} {R : Set} ->
    λ (by : ({S : Set} -> ({Q : Set} -> F Q -> Q) -> F S -> S)) (h : ({Q : Set} -> F Q -> F Q)) ->
      hfix {F} {λ (X : Set) -> X} {R}
        (λ {T : Set} -> λ (rec : {Q : Set} -> F Q -> Q) (t : F T) ->
           by {T} (λ {Q : Set} -> λ (q : F Q) -> rec {Q} (h {Q} q)) t)

fix2 =
  λ {A₁ B₁ A₂ B₂ R : Set} ->
    fixBy {λ (X : Set) -> (A₁ -> B₁) -> (A₂ -> B₂) -> X} {R}
      (λ {S : Set} ->
        λ (k : {Q : Set} -> ((A₁ -> B₁) -> (A₂ -> B₂) -> Q) -> Q) (h : (A₁ -> B₁) -> (A₂ -> B₂) -> S) ->
          h
            (λ (x₁ : A₁) -> k {B₁} (λ (f₁ : A₁ -> B₁) (f₂ : A₂ -> B₂) -> f₁ x₁))
            (λ (x₂ : A₂) -> k {B₂} (λ (f₁ : A₁ -> B₁) (f₂ : A₂ -> B₂) -> f₂ x₂)))



open import Data.Bool.Base
open import Data.Nat.Base

evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
evenAndOdd {R} = fix2 {ℕ} {Bool} {ℕ} {Bool} {R} λ choose even odd -> choose
  (λ { 0 -> true  ; (suc n) -> odd  n })
  (λ { 0 -> false ; (suc n) -> even n })

even = evenAndOdd λ x y -> x
odd  = evenAndOdd λ x y -> y

open import Relation.Binary.PropositionalEquality
open import Data.List.Base

testEven : map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
         ≡ (true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ [])
testEven = refl

testOdd : map odd (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
        ≡ (false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ [])
testOdd = refl