Agda：将一行标准输入读取为String而不是Costring [英] Agda: Reading a line of standard input as a String instead of a Costring

问题描述

我正在尝试编写一个简单的程序，从标准输入读取一行，将其反转，然后打印反转的字符串。

I am trying to write a simple program that reads a line from standard input, reverses it, and then prints the reversed string.

不幸的是本机 getLine 函数读取 Costring ;我只能反转 String s;并且没有函数将 Costring 带到 String 。

Unfortunately the native getLine function reads a Costring; I can only reverse Strings; and there is no function that takes a Costring to a String.

如何修改此程序进行编译？

How can I amend this program to compile?

module EchoInputReverse where

-- Agda standard library 0.7
open import Data.List using (reverse)
open import Data.String
open import Foreign.Haskell using (Unit)
open import IO.Primitive

postulate
  getLine : IO Costring

{-# COMPILED getLine getLine #-}

main : IO Unit
main = 
  getLine >>= (λ s → 
  -- NOTE: Need a (toString : Costring → String) here. Or some other strategy.
  return (toCostring (fromList (reverse (toList (toString s))))) >>= (λ s' → 
  putStrLn s'))

推荐答案

你不能这样做，至少不能直接做到。问题是 Costring 的大小可以是无限的，而 String s必须是有限的。

You can't do that, at least not directly. The problem is that Costring can be infinite in size, while Strings must be finite.

想象一下，将程序作为 prog< / dev / zero ，会发生什么？ 反向函数只能在到达输入列表的末尾后产生第一个元素，并且可能永远不会发生。

Imagine running the program as prog < /dev/zero, what should happen? The reverse function can produce the first element only after reaching the end of the input list and that may never happen.

我们需要表达的事实是将 Costring 转换为 String 可能会失败。一种方法是使用偏好monad。让我们来看看定义：

We need to express the fact that converting a Costring to String can fail. One way to do it is to use the partiality monad. Let's take a look at the definition:

data _⊥ {a} (A : Set a) : Set a where
  now   : (x : A) → A ⊥
  later : (x : ∞ (A ⊥)) → A ⊥

因此，我们可以输入类型 A 右现在的值，或者我们需要等待以后。但请注意∞符号：这意味着我们实际上可以永远等待（因为可以有无限数量的以后构造函数）。

So, we can either have a value of type A right now, or we need to wait for later. But notice the ∞ symbol: that means we can actually wait forever (as in there can be infinite number of later constructors).

我将转换和反转合并为一个函数。首先进口：

I'll merge the conversion and reversing into one function. Imports first:

open import Category.Monad.Partiality
open import Coinduction
open import Data.Char
open import Data.Colist
  using ([]; _∷_)
open import Data.List
  using ([]; _∷_; List)
open import Data.String
open import Data.Unit
open import IO

现在，我们的反向函数的类型应该提到我们将 Costring 作为输入，但也返回字符串可能会失败。然后实现相当简单，它通常与累加器反向：

Now, the type of our reverse function should mention that we take a Costring as an input but also that returning a String may fail. The implementation is then fairly simple, it's the usual reverse with accumulator:

reverse : Costring → String ⊥
reverse = go []
  where
  go : List Char → Costring → String ⊥
  go acc []       = now (fromList acc)
  go acc (x ∷ xs) = later (♯ go (x ∷ acc) (♭ xs))

但是，我们可以打印字符串，但不是字符串⊥！这就是 IO 的帮助：我们可以将以后的构造函数解释为什么都不做，如果我们找到现在构造函数，我们可以 putStrLn 它包含的 String 。

However, we can print a String, but not String ⊥! That's where IO helps: we can interpret the later constructors as "do nothing" and if we find now constructor, we can putStrLn the String it contains.

putStrLn⊥ : String ⊥ → IO ⊤
putStrLn⊥ (now   s) = putStrLn s
putStrLn⊥ (later s) = ♯ return tt >> ♯ putStrLn⊥ (♭ s)

请注意，我使用 IO 来自 IO 模块，而不是来自 IO.Primitive 的模块。这基本上是建立在假设上的一层，所以它更好一些。但如果你想使用 getLine ，你必须写：

Notice that I use the IO from IO module, not the one from IO.Primitive. This is basically a layer built on the postulates, so it's a bit nicer. But if you want to use getLine with this, you have to write:

import IO.Primitive as Prim

postulate
  primGetLine : Prim.IO Costring

{-# COMPILED primGetLine getLine #-}

getLine : IO Costring
getLine = lift primGetLine

最后，我们可以编写 main 功能：

And finally, we can write the main function:

main = run (♯ getLine >>= λ c → ♯ putStrLn⊥ (reverse c))

---

使用 Cc Cx Cc 编译此程序，然后运行它，我们得到预期的结果：

---

Compiling this program using C-c C-x C-c and then running it, we get the expected:

$ cat test
hello world
$ prog < test    
dlrow olleh

这篇关于Agda：将一行标准输入读取为String而不是Costring的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！