在Agda-stdlib的IO中使用`do`符号的正确方式是什么？

Question

我尝试将do-notation与agda-stdlib的IO一起使用，但奇怪的是，_>>_的类型使用∞：{B : Set a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A。正因为如此，我需要在应用程序之间交替使用♯，但这使得使用起来很笨拙。例如，♯是构建打印一行的程序所必需的：

main : IO ⊤
main = do
  ♯ (putStrLn "hi")
  ♯ (return tt)

此外，用更多的行扩展它不能进行检查。我不得不放弃do-notation，就像这样：

main : IO ⊤
main = 
  ♯ (♯ putStrLn "hi" >> 
    ♯ putStrLn "ho") >>
    ♯ return tt

这看起来很可怕。我可以重新定义_>>_和_>>=_

_>>_ : {A : Set} {B : Set} (m₁ : (IO B)) (m₂ : (IO A)) → IO A
_>>_ a b = (♯ a) IO.>> (♯ b)

但我想这不是我该做的。我是不是漏掉了什么？使用它的正确方式是什么？

Answer 1

IO在标准库中的实现早于do-notation在Agda中的添加，因此它在编写时并没有考虑到do-notation。Ulf的Agda prelude有一个更新的IO实现，它支持do-notation。