英文:
Reading a string from the command line in Agda 2
问题
如何在Agda 2.6+中读取字符串输入？
我一直在努力编写一个程序，只需读取一行输入并立即将其返回。无论我尝试什么，似乎总是会出现问题。尽管我进行了搜索，但我找不到一个简单的示例。"Hello World"示例只能输出。如果我尝试输入然后输出，那么我需要某种单子。我尝试了Haskell风格，但显然行不通。我尝试使用音乐符号，但仍然不起作用。我正在寻找最简单的示例，类似于以下内容：
main = do
s <- getLine
putStrLn s
我尝试了太多变种，但似乎都会遇到某些问题。即使在我似乎弄清楚单子的情况下，它也会抱怨尝试统一不同的IO定义。ChatGPT变得有些不耐烦，告诉我如果我想编写实际执行操作的依赖代码，可以尝试使用Idris。
英文:
How do you read string input into Agda in 2.6+?
I have been fighting to just write a program that reads a line of input and immediately spits it back. There seems to always be an issue, no matter what I try. Despite searching, I cannot find a simple example. The hello world only outputs. If I try to input and then output, then I need some kind of monad. I've tried haskell style, but that obviously won't work. I've tried using musical notation, but still doesn't do it. I'm looking for the simplest example, something with
main = do
s <- getLine
putStrLn s
I've tried too many variations to list, but all seem to fall prey to some issue. Even when I seem to get the monad right, it complains of trying to unify different definitions of IO. ChatGPT got all snippy and told me to try Idris if I want to write dependent code that actually does something.
答案1
得分: 2
你已经走在正确的道路上：你只缺少一个导入（Agda默认不加载任何内容）和一个类型注解（Agda要求顶层注解）。
[文档](https://agda.readthedocs.io/en/v2.6.3/getting-started/a-taste-of-agda.html#building-an-executable-agda-program)中有一个示例，可以扩展到你的程序中：
```agda
{-# OPTIONS --guardedness #-}
open import IO
main : Main
main = run do
s <- getLine
putStrLn s
请注意，这需要安装标准库。
<details>
<summary>英文:</summary>
You're on the right track: you're only missing an import
(Agda does not load anything by default) and a type annotation
(Agda requires top-level annotations).
[The docs](https://agda.readthedocs.io/en/v2.6.3/getting-started/a-taste-of-agda.html#building-an-executable-agda-program) have an example that can be extended to your program:
{-# OPTIONS --guardedness #-}
open import IO
main : Main
main = run do
s <- getLine
putStrLn s
Note that this requires [the standard library being installed](https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md).
</details>
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论