免费的 monad 转换器 - 如何实现绑定？

Question

我正在尝试实现类似于 haskell 的“免费”包中的 FreeT 的免费 monad 转换器，但我不知道如何编写 bind 以便终止检查器不会抱怨。在我看来，递归调用的参数 p i 应该小于初始参数，但我不确定这是不是真的。是否可以用 --safe agda 实现 bind？

{-# 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 的实现正在混合迭代结构和在同构集合之间来回移动（复合容器的扩展与容器扩展的组合）。该推理模 isos 掩盖了终止参数。

您可以通过将两者分开来绕过它。我实现了 join 因为它更方便。大多数代码是你的，唯一的见解是使用 Data.W.foldr 将迭代分支到库函数。

    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

免费的 monad 转换器 - 如何实现绑定？

Free monad transformer - how to implement bind?

agda

monad-transformers

termination