1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Simple examples of programs using IO
------------------------------------------------------------------------
{-# OPTIONS --guardedness #-}
module README.IO where
open import Level
open import Data.Nat.Base
open import Data.Nat.Show using (show)
open import Data.String.Base using (String; _++_; lines)
open import Data.Unit.Polymorphic
open import Function.Base using (_$_)
open import IO
------------------------------------------------------------------------
-- Basic programs
------------------------------------------------------------------------
------------------------------------------------------------------------
-- Hello World!
-- Minimal example of an IO program.
-- * The entrypoint of the executable is given type `Main`
-- * It is implemented using `run`, a function that converts a description
-- of an IO-computation into a computation that actually invokes the magic
-- primitives that will perform the side effects.
helloWorld : Main
helloWorld = run (putStrLn "Hello World!")
------------------------------------------------------------------------
-- Hello {{name}}!
-- We can of course write little auxiliary functions that may be used in
-- larger IO programs. Here we are going to first write a function displaying
-- "Hello {{name}}!" when {{name}} is passed as an argument.
-- `IO` primitives whose sole purpose is generating side effects (e.g.
-- printing a string on the screen) are typically given a level polymorphic
-- type which means we may need to add explicit level annotations.
-- Here we state that the `IO` computation will be at level zero (`0ℓ`).
sayHello : String → IO {0ℓ} ⊤
sayHello name = putStrLn ("Hello " ++ name ++ "!")
-- Functions can be sequenced using monadic combinators or `do` notations.
-- The two following definitions are equivalent. They start by asking the
-- user what their name is, listen for an answer and respond by saying hello
-- using the `sayHello` auxiliary function we just defined.
helloName : Main
helloName = run (putStrLn "What is your name?" >> getLine >>= sayHello)
doHelloName : Main
doHelloName = run do
putStrLn "What is your name?"
name ← getLine
sayHello name
------------------------------------------------------------------------
-- (Co)Recursive programs
------------------------------------------------------------------------
------------------------------------------------------------------------
-- NO GUARDEDNESS
-- If you do not need to rely on guardedness for the function to be seen as
-- terminating (for instance because it is structural in an inductive argument)
-- then you can use `do` notations to write fairly readable programs.
-- Countdown to explosion
countdown : ℕ → IO {0ℓ} _
countdown zero = putStrLn "BOOM!"
countdown m@(suc n) = do
let str = show m
putStrLn str
countdown n
-- cat the content of a finite file
cat : String → IO _
cat fp = do
content ← readFiniteFile fp
let ls = lines content
List.mapM′ putStrLn ls
------------------------------------------------------------------------
-- TOP-LEVEL LOOP
-- If you simply want to repeat the same action over and over again, you
-- can use `forever` e.g. the following defines a REPL that echos whatever
-- the user types
echo : IO ⊤
echo = do
hSetBuffering stdout noBuffering
forever $ do
putStr "echo< "
str ← getLine
putStrLn ("echo> " ++ str)
------------------------------------------------------------------------
-- GUARDEDNESS
-- If you are performing coinduction on a potentially infinite piece of codata
-- then you need to rely on guardedness. That is to say that the coinductive
-- call needs to be obviously under a coinductive constructor and guarded by a
-- sharp (♯_).
-- In this case you cannot use the convenient combinators that make `do`-notations
-- and have to revert back to the underlying coinductive constructors.
open import Codata.Musical.Notation
open import Codata.Musical.Colist using (Colist; []; _∷_)
open import Data.Bool
open import Data.Unit.Polymorphic.Base
-- Whether a colist is finite is semi decidable: just let the user wait until
-- you reach the end!
isFinite : ∀ {a} {A : Set a} → Colist A → IO Bool
isFinite [] = pure true
isFinite (x ∷ xs) = seq (♯ pure tt) (♯ isFinite (♭ xs))
|
