io - Agda:将一行标准输入作为字符串而不是 Costring 读取

Question

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

不幸的是本地人getLine函数读取 Costring ;我只能反转String小号；并且没有采用 Costring 的函数到 String .

我怎样才能修改这个程序来编译？

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'))

Answer 1

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

想象一下以 prog < /dev/zero 运行程序，应该怎么办？ reverse函数只有在到达输入列表的末尾后才能产生第一个元素，这可能永远不会发生。

我们需要表达一个事实，即转换 Costring至String可能会失败。一种方法是使用偏心单子(monad)。让我们看一下定义:

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

所以，我们可以有一个 A 类型的值。对 now , 或者我们需要等待 later .但请注意 ∞符号:这意味着我们实际上可以永远等待(因为可以有无限数量的 later 构造函数)。

我将转换和反转合并到一个函数中。先导入:

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

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

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))

但是，我们可以打印 String ，但不是 String ⊥ !这就是 IO帮助:我们可以解释 later构造函数为“什么都不做”，如果我们找到 now构造函数，我们可以 putStrLn String它包含。

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

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

import IO.Primitive as Prim

postulate
  primGetLine : Prim.IO Costring

{-# COMPILED primGetLine getLine #-}

getLine : IO Costring
getLine = lift primGetLine

最后，我们可以写 main功能:

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

使用 C-c C-x C-c 编译此程序然后运行它，我们得到了预期:

$ cat test
hello world
$ prog < test    
dlrow olleh