agda/agda-stdlib — pull request #24 by jepugs (2014-06-25 17:59:08+00:00)
Title: Added to IO.agda

I added a few more IO functions (namely `putChar`, `readChar`, and `readLine`) to `IO.Primitive` and `IO`. These are pretty self-explanatory.

I also added the utility functions `_>>♯_` and `_>>=♯_` to `IO`. These allow ∞ IO objects to be "chained" together. Basically, they are like `_>>_` and `_>>=_` respectively, but they evaluate to values of type `∀ {a} {A : set a} -> ∞ (IO A)`.

Together, these additions allow one to write the program:

open import Coinduction
open import Data.Char
open import Data.String
open import Data.Unit
open import IO

agdaMain : ∞ (IO ⊤)
agdaMain =
♯ putStrLn "Enter a string..." >>♯
♯ getLine >>=♯ λ str →
♯ putStrLn ("You entered " ++ str) >>♯
♯ putStrLn "Enter a character..." >>♯
♯ getChar >>=♯ λ c →
♯ putStr "You entered " >>♯
♯ putChar c >>♯
♯ putChar '\n'

main = run (♭ agdaMain)

All without having to go through IO.Primitive or the ffi.