module Revise.IO where

Characters

open import Data.Char using (Char)

The Char type:

Char : Set    -- abstract

Agda has character literals:

char_a : Char
char_a = 'a'

Some operations on characters:

toNat : Char → ℕ   -- unicode code

_==_ : Char → Char → Bool

_≟_ : Decidable {A = Char} _≡_   -- see later

Strings

open import Data.String using (String; Costring; toCostring; _++_)

The String and Costring types:

String : Set     -- abstract

Costring : Set
Costring = Colist Char

Agda has string literals:

string_hello : String
string_hello = "hello"

Some operations:

_++_ : String → String → String

toList : String → List Char

toCostring : String → Costring

toVec : (s : String) → Vec Char (length (toList s))

fromList : List Char → String

Exercise

open import Data.List using (List; _∷_; [])

unlines : List String → String
unlines []       = ""
unlines (x ∷ xs) = x ++ "\n" ++ unlines xs

Equality on strings

_==_ : String → String → Bool

_≟_ : Decidable {A = String} _≡_

The IO type

open import IO.Primitive

IO A denotes a computation which may do I/O operations and at the end delivers a value of type A.

For example, IO ℕ is a computation which delivers a natural number.

IO : Set → Set

The unit type

open import Foreign.Haskell using (Unit; unit)

Unit is isomorphic to ⊤:

data Unit : Set where
  unit : Unit

IO primitives

getContents : IO Costring
putStr      : Costring → IO Unit
putStrLn    : Costring → IO Unit

readFile    : String → IO Costring
writeFile   : String → Costring → IO Unit
appendFile  : String → Costring → IO Unit

The main function

main : IO Unit
main = putStrLn (toCostring "Hello World!")

Compilation

Compilation of the main function: C-c C-x C-c
(or from the Emacs Agda menu)

If you get the error Could not find module IO.FFI, try to do

$ cd <path-to-standard-library>
$ cd ffi
$ cabal install

IO connectives: return

return x do no I/O operations just returns x

return : {A : Set} → A → IO A

This program does nothing:

main′ : IO Unit
main′ = return unit

IO connectives: _>>=_

The computation m >>= f first runs the computation m which delivers a return value a, then runs the computation f a and returns its return value.

_>>=_  : {A B : Set} → IO A → (A → IO B) → IO B

With return, _>>=_ and the privitives we can construct lots of computations already!

Adding a new primitive

This is how to add a new primitive if not present.

postulate
  getLine : IO Costring

{-# COMPILED getLine getLine #-}

The second argument of the COMPILED pragma should be a valid Haskell expression.

Examples

main″ = getLine >>= putStrLn

open import Data.Colist renaming (_++_ to _+++_)

main‴ =
    getLine >>= λ x → 
    putStrLn (toCostring "Hello " +++ x)

Exercise

Write a program which gets a line, and echoes it if the line is not empty.

Infinite computations

open import Data.List renaming (_++_ to _++L_)
open import Coinduction

f : List Char → List Char → Costring → Costring
f acc [] [] = []
f acc [] ('\n' ∷ xs) = '\n' ∷ ♯ ( f [] (reverse acc ++L '\n' ∷ []) (♭ xs))
f acc [] (x ∷ xs) = x ∷ ♯ f (x ∷ acc) [] (♭ xs)
f acc (x ∷ xs) zs = x ∷ ♯ f acc xs zs

trans : Costring → Costring
trans = f [] []

main⁗ = getContents >>= λ x → putStr (trans x)