I am trying to write a simple program that reads a line from standard input, reverses it, and then prints the reversed 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'))
You can't do that, at least not directly. The problem is that Costring can be infinite in size, while Strings must be finite.
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.
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 ⊥
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
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))
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)
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
And finally, we can write the main function:
main = run (♯ getLine >>= λ c → ♯ putStrLn⊥ (reverse c))
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
Saizan on #agda points out that one could just postulate that getLine : IO String instead of getLine : IO Costring. This works. So you get:
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'))
The downside is that this approach asserts that getLine always returns a finite string, which may not be correct in the case of prog < /dev/zero as @Vitus points out.
But I don't think this matters. If getLine does in fact returns an infinite string then neither this solution nor @Vitus's solution will yield a program that terminates. They have equivalent behavior.
It would be ideal to detect whether the input was infinite and yield an error in that case. But this kind of infinity detection on IO is not possible in general.
