让绑定中间产物产生IO单
让绑定中间产物产生IO单
提问于 2016-03-18 08:29:48
鉴于这种情况：
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-binding的中间结果f s。我希望这能奏效：
foo₁ : IO ⊤
foo₁ = ♯ readFiniteFile "input.txt" >>= \s →
let x = f s in
♯ (♯ putStrLn (g₁ x) >>
♯ putStrLn (g₂ x))但这次失败了
未实现:let绑定变量范围内的协归纳构造函数
所以我试着搬出♯
foo₂ : IO ⊤
foo₂ = ♯ readFiniteFile "input.txt" >>= \s →
♯ (let x = f s in
♯ putStrLn (g₁ x) >>
♯ putStrLn (g₂ x))和以前一样的问题。
我成功地解决了这一问题，提出了♯的强化步骤：
_>>′_ : ∀ {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)但是，如果“内联”版本不起作用，为什么这样做呢？
回答 1
Stack Overflow用户
回答已采纳
发布于 2016-11-12 13:07:23
而且，这个问题由来已久，当我今天看它的时候，我注意到它已经修好了就在你问你问题的前几天。修复是当前发布版本(2.5.1.1版)的一部分。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/36079514
复制相关文章
相似问题
腾讯云开发者
