时间戳

首页 > 解决方案 > 如何在 Agda 中创建一个“do”块

agda - 如何在 Agda 中创建一个“do”块

问题描述

我有一些在 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 ）

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

open import Common.IO

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

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

...我如何让我的代码在 Agda 中工作？

标签： agda

解决方案

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

open import IO
open import Codata.Musical.Notation

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

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

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

推荐阅读