6

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

不幸的是，本机getLine函数读取的是Costring; 我只能反转Strings；并且没有将 aCostring带到 a 的函数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'))
4

2 回答 2

12
于 2014-02-16T13:11:11.490 回答
7

#agda 上的 Saizan 指出，人们可以假设getLine : IO String而不是getLine : IO Costring. 这行得通。所以你得到：

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 String

{-# COMPILED getLine getLine #-}

main : IO Unit
main = 
  getLine >>= (λ s → 
  return (toCostring (fromList (reverse (toList s)))) >>= (λ s' → 
  putStrLn s'))

缺点是这种方法断言getLine总是返回一个有限prog < /dev/zero的字符串，这在@Vitus 指出的情况下可能不正确。

但我不认为这很重要。如果getLine确实返回了一个无限字符串，那么这个解决方案和@Vitus 的解决方案都不会产生终止的程序。它们具有相同的行为。

检测输入是否无限并在这种情况下产生错误将是理想的。但是这种对 IO 的无穷大检测一般是不可能的。

于 2014-02-16T18:39:09.267 回答