如何在 Agda 中创建“do”块

Question

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

\n\n

这是哈斯克尔代码

\n\n

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

\n\n

输出是

\n\n

A string\nsecond string\n

\n\n

我尝试将其转换为 Agda

\n\n

open import Common.IO\n\nmain = do\n  putStrLn "A string"\n  putStrLn "second string"\n

\n\n

但我刚刚收到错误消息

\n\n

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

\n\n

（完整错误的屏幕截图：https ://i.stack.imgur.com/pS3Ty.jpg ）

\n\n

编辑：这是我最好的猜测，它显然行不通，但我是 Agda 的新手......有什么想法吗？

\n\n

open import Common.IO\n\n_>>_ : ? \xe2\x86\x92 ? \xe2\x86\x92 ?\n??? = ???\n??? = ???\n\nmain = do\n  putStrLn "A string"\n  putStrLn "second string"\n

\n\n

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

\n

Answer 1

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

\n\n

open import IO\nopen import Codata.Musical.Notation\n\nmain = run do\n  \xe2\x99\xaf putStrLn "A string"\n  \xe2\x99\xaf putStrLn "second string"\n

\n\n

有趣\xe2\x99\xaf_的是我们所说的乐谱：IO导致潜在的无限计算，所以我们必须使用共归纳类型。

\n\n

但请注意，标准库中的 IO 是在 do 表示法添加到 Agda 之前创建的，因此如果它们在某种程度上兼容，那只是偶然的。最好坚持>>=（并尝试尽快编写纯代码，仅在边界处使用 IO）。

\n