如何在Agda中创建“do”块

Question

我有一些代码在Haskell中工作，我想将其转换为Agda。

这是Haskell代码

main = do
  putStrLn "A string"
  putStrLn "second string"

而输出是

A string
second string

我试过把它转换成Agda

open import Common.IO

main = do
  putStrLn "A string"
  putStrLn "second string"

但我只是得到错误信息

'_>>_ needs to be in scope to desugar 'do' block'

（完整错误的屏幕截图：https://imgur.com/a/3lxdwR7）

编辑：这是我最好的猜测，它显然不起作用，但我是阿格达的新手...任何想法？

open import Common.IO

_>>_ : ? → ? → ?
??? = ???
??? = ???

main = do
  putStrLn "A string"
  putStrLn "second string"

...如何让我的代码在Agda中运行？

Answer 1

我不知道Common.IO是什么。使用标准库，您可以编写：

open import IO
open import Codata.Musical.Notation

main = run do
  ♯ putStrLn "A string"
  ♯ putStrLn "second string"

有趣的♯_就是我们所说的乐谱：IO导致潜在的无限计算，所以我们必须使用共同类型。

但请注意，标准库中的IO是在将符号添加到Agda之前创建的，因此如果它们是兼容的，那么它只是偶然的。坚持>> =（并尝试尽快编写纯代码，只在边界使用IO）可能更好。