免费的Monad Transformer-如何实施绑定？

Question

我正在尝试实现与Haskell的“ Free”软件包中的freet类似的免费单本变压器，但我不知道如何编写bind，以便终止检查器不使用' t抱怨。在我看来，递归调用的参数p i应该小于初始参数，但是我不确定这是否真的正确。是否可以使用 - 安全 agda实现bint？

{-# 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

问题是bind的实现正在混合迭代
在同构集合之间来回移动的结构和来回移动（复合容器的扩展与容器扩展的组成）。推理模型ISO掩盖了终止论点。

您可以通过分开两者来绕过它。我实现了加入，因为
更方便。大多数代码是您的，唯一的见解是
使用data.w.foldr将迭代分配给库函数。

    join : ∀{A} → C (C A) → C A
    join = Data.W.foldr $ λ ca → sup $ c[c]⇒[c∘c]
         $ M.join $ M._<
gt;_ [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