Free monad transformer - how to implement bind?

Question

I am trying to implement free monad transformer similar to the FreeT from haskell's "free" package, but I don't know how to write bind so that the termination checker doesn't complain. It seems to me that the recursive call's parameter p i should be smaller than the initial parameter, but I'm not sure if that's really true. Is it possible to implement bind with --safe agda?

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

module Test where

import Data.Container.Combinator            as Cc
import Data.Container.Combinator.Properties as Ccp
import Function.Equality                    as Fun
import Function.Inverse                     as Fun
open import Data.Container.Core             as C        using (Container; ⟦_⟧)
open import Data.Container.Relation.Unary.Any           using (any)
open import Data.Product                                using (_,_)
open import Data.Sum.Base                               using (inj₁; inj₂)
open import Data.W                                      using (W; sup)
open import Effect.Monad                                using (RawMonad)
open import Function.Base                               using (_$_)
open import Level

module _ (M F : Container 0ℓ 0ℓ) ⦃ M-monad : RawMonad {f = 0ℓ} ⟦ M ⟧ ⦄ where
    module M = RawMonad M-monad
    
    module _ {A X : Set} where
        private
            ∘-correct = Ccp.Composition.correct M (F Cc.⊎ Cc.const A) {X = X}
        
        open Fun.Π (Fun.Inverse.to ∘-correct) public
            using () renaming (_⟨$⟩_ to [c∘c]⇒c[c])

        open Fun.Π (Fun.Inverse.from ∘-correct) public
            using () renaming (_⟨$⟩_ to c[c]⇒[c∘c])

    C : Set → Set
    C A = W $ M Cc.∘ (F Cc.⊎ Cc.const A)

    pure : ∀{A} → A → C A
    pure x = sup $ c[c]⇒[c∘c] $ M.pure $ inj₂ x , λ ()

    unsup : ∀{A} → C A → ⟦ M Cc.∘ (F Cc.⊎ Cc.const A) ⟧ (C A)
    unsup (sup x) = x

    bind : ∀{A B} → C A → (A → C B) → C B
    bind {A}{B} (sup ca) f = sup $ c[c]⇒[c∘c] $ M.join $
        M._<$>_ [c∘c]⇒c[c] $ [c∘c]⇒c[c] ca M.>>= λ where
            (inj₁ a , p) → M.pure $ c[c]⇒[c∘c] $ M.pure $ inj₁ a , λ i → bind (p i) f
            (inj₂ x , _) → M.pure $ unsup $ f x

Answer 1

The issue is that the implementation of bind is mixing iterating over the structure and moving back and forth between isomorphic sets (the extension of the composite container vs. the composition of the containers' extensions). That reasoning modulo isos obscures the termination argument.

You can bypass that by separating the two. I implemented join because it's more convenient. Most of the code is yours, the only insight is the use of Data.W.foldr to fork off the iteration to a library function.

    join : ∀{A} → C (C A) → C A
    join = Data.W.foldr $ λ ca → sup $ c[c]⇒[c∘c]
         $ M.join $ M._<$>_ [c∘c]⇒c[c] $ [c∘c]⇒c[c] ca M.>>= λ where
           (inj₁ a , p) → M.pure $ c[c]⇒[c∘c] $ M.pure $ inj₁ a , p
           (inj₂ ca , p) → M.pure $ unsup ca