让 IO monad 中的绑定中间结果

Question

鉴于此背景：

open import IO
open import Data.String
open import Data.Unit
open import Coinduction

postulate
  A : Set
  f : String → A
  g₁ g₂ : A → String

假设我想实现类似

的东西

foo : IO ⊤
foo = ♯ readFiniteFile "input.txt" >>= \s →
      ♯ (♯ putStrLn (g₁ (f s)) >>
      ♯ putStrLn (g₂ (f s)))

通过let绑定中间结果f s。我希望这会起作用：

foo₁ : IO ⊤
foo₁ = ♯ readFiniteFile "input.txt" >>= \s →
       let x = f s in
       ♯ (♯ putStrLn (g₁ x) >>
       ♯ putStrLn (g₂ x))

但这失败了

Not implemented: coinductive constructor in the scope of a let-bound variable

所以我试着搬出 ♯:

foo₂ : IO ⊤
foo₂ = ♯ readFiniteFile "input.txt" >>= \s →
       ♯ (let x = f s in
       ♯ putStrLn (g₁ x) >>
       ♯ putStrLn (g₂ x))

和以前一样的问题。

我通过取消 ♯ening 步骤成功解决了这个问题：

_>>′_ : ∀ {a} {A B : Set a} → IO A → IO B → IO B
m >>′ m′ = ♯ m >> ♯ m′

foo₂ : IO ⊤
foo₂ = ♯ readFiniteFile "input.txt" >>= \s →
       ♯ let x = f s in
       putStrLn (g₁ x) >>′ putStrLn (g₂ x)

但是为什么 "inlined" 版本不起作用？

Answer 1

仅供参考，这个问题是一个长期存在的问题，当我今天查看它时，我注意到 it had been fixed 就在您提出问题的前几天。该修复是当前发布版本（版本 2.5.1.1）的一部分。

让 IO monad 中的绑定中间结果

Let-binding intermediate results in IO monad

agda

coinduction