免费单体变压器 - 如何实现绑定?

Question

我正在尝试实现类似于 Haskell "free"包中的FreeT的自由 monad 转换器，但我不知道如何编写bind以便终止检查器不会抱怨。在我看来，递归调用的参数p i应该小于初始参数，但我不确定这是否真的如此。是否可以使用--safeagda 实施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