-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex.html
248 lines (204 loc) · 7.03 KB
/
index.html
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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta name="generator" content=
"HTML Tidy for Mac OS X (vers 31 October 2006 - Apple Inc. build 13), see www.w3.org">
<style type="text/css" title="currentStyle">
/* text margins and font */
body, td
{
font:12px verdana, sans-serif;
color: #191919;
margin: 2ex 12.5% 2ex 12.5%;
padding-bottom: 2ex;
line-height: 140%;
}
.ralign
{
margin: 0ex 0em 0ex 2em;
}
/* Header with border */
h1
{
border-bottom-style: solid;
border-color: #404040;
border-width: 1px;
padding-bottom: 0.25ex;
}
/* Headers colour */
h1,h2,h3,h4
{
color:#000080
}
/* link colouring */
a:link
{
color: #0000FF;
text-decoration: none;
}
/* visited link coloring */
a:visited
{
color: #880000;
text-decoration: none;
}
pre
{
border: 2px solid gray;
padding: 1px;
padding-left: 5px;
margin-left: 10px;
background-color: #eee;
}
pre.define
{
background-color: #ffb;
border-color: #cc0;
}
/* footer style */
p.footer
{
border-top-style: solid;
border-top-width: 1px;
border-color: #404040;
padding-top:1ex;
color: #878787;
font-family: Helvetica;
font-size: 75%;
text-align: right;
}
</style>
<title>IOSpec</title>
</head>
<body>
<h1>IOSpec: a pure specification of the IO monad</h1>
<table>
<tr>
<td>
<p>IOSpec is a library containing a pure specification of
several functions in the IO monad. You can use these
specifications to test, debug, and reason about impure
code.</p>
<h2>Introduction</h2>
<p>To get a taste of what you can do, consider an
implementation of an 'imperative' queue that uses pointers
to build a linked list:</p>
<pre>
import Test.IOSpec
data Queue = Queue {front :: IORef Cell, back :: IORef Cell}
data Cell = Cell Int (IORef Cell) | NULL
emptyQueue :: IOSpec IORefS Queue
enqueue :: Queue -> Int -> IOSpec IORefS () ()
dequeue :: Queue -> IOSpec IORefS (Maybe Int)
</pre>
</td>
<td><img class="ralign" src="www/unsafe.jpg" alt=
"unsafePerformIO"></td>
</tr>
</table>
<p>Values of type <code>IOSpec IORefS a</code> correspond to
computations that use IORefs, but no other parts of the IO monad,
and return a value of type <code>a</code>. By convention, a
trailing 'S' is used to denote a specification. For example,
values of type <code>IOSpec MVarS a</code> correspond to IO
computations using just MVars.</p>
<p>These specifications are pure functions, running on a pure
<a href=
"http://www.cs.nott.ac.uk/~wss/repos/IOSpec/dist/doc/html/IOSpec/Test-IOSpec-VirtualMachine.html">
Virtual Machine</a>, that behave the same as their IO
counterparts. Using tools such as <a href=
"http://www.cs.chalmers.se/~rjmh/QuickCheck/">QuickCheck</a> and
the <a href=
"http://www.haskell.org/ghc/docs/latest/html/users_guide/ghci-debugger.html">
GHCi debugger</a> we can test and debug our implementation of
queues <em>as if it was pure</em>. For example, we may want to
check that the following property holds:</p>
<pre>
fifoProp :: [Int] -> Bool
fifoProp xs = evalIOSpec enqDeq singleThreaded == Done xs
where
enqDeq :: IOSpec IORefS [Int]
enqDeq = do
q <- emptyQueue
forM_ xs (enqueue q)
unfoldM dequeue q
</pre>That is, starting from an empty queue, enqueuing and
subsequently dequeuing any list of integers should return the
original list. Note that this property does <em>not</em> require
<code>unsafePerformIO</code> or any such hacks: the
<code>evalIOSpec</code> function is entirely pure. It is
parameterized by the scheduler, allowing you to test your code with
different scheduling algorithms to maximize code coverage. Once we
are satisfied with our implementation, we can import <a href=
"http://haskell.cs.yale.edu/ghc/docs/latest/html/libraries/base/Data-IORef.html">
Data.IORef</a> and use real IORefs, instead of the pure
specification provided by IOSpec.
<p>The IOSpec library is not restricted to IORefs. There are also
pure specifications of concurrency, STM, and teletype primitives.
These specifications can be combined as you see fit: you can
define your own <code>IOSpec</code> monad <em>à la
carte</em>. For example, when writing concurrent code you may
want use just MVars and <code>forkIO</code>:</p>
<pre>
type Concurrent a = IOSpec (MVarS :+: ForkS) a
</pre>Functions of type <code>Concurrent a</code> may use IO
functions such as <code>newEmptyMVar</code> or <code>forkIO</code>.
But using <code>putStr</code> in the <code>Concurrent</code> monad,
for example, will cause a type error. You may want to <a href=
"http://www.cs.nott.ac.uk/~wss/repos/IOSpec/dist/doc/html/IOSpec/">
browse the API</a> to get a better idea of how the library is
organized.
<p>Haskell's careful treatment of IO shows how being <em>precise
about effects</em> can help you write <em>more reliable
code</em>. I'd like to think that the IOSpec library takes some
of these ideas one step further.</p>
<h2>Download</h2>
<p>A <a href="dist/IOSpec-0.2.tar.gz">tarball containing the
sources</a> is available.</p>
<p>Alternatively, you may want to check out the following darcs
repository:</p>
<pre>
darcs get http://www.cs.nott.ac.uk/~wss/repos/IOSpec
</pre>
<h2>Installation</h2>You need to install IOSpec using <a href=
"http://www.haskell.org/cabal/">Cabal</a>. Essentially, you need
to download the sources and issue the following commands:
<pre>
runhaskell Setup.lhs configure
runhaskell Setup.lhs build
runhaskell Setup.lhs install
</pre>If you want to customize the installation process, you may
want to read more about <a href=
"http://www.haskell.org/ghc/docs/latest/html/Cabal/builders.html">
installing packages using Cabal</a>.
<h2>Documentation</h2>
<p>Browse the <strong><a href=
"http://www.cs.nott.ac.uk/~wss/repos/IOSpec/dist/doc/html/IOSpec/">
Haddock-ed source code</a></strong>.</p>
<p>The examples directory that comes with the sources contains
several well-documented examples.</p>
<p>The ideas underlying the implementation are described in the
following papers:</p>
<ul>
<li><a href=
"http://www.cs.nott.ac.uk/~wss/Publications/BeautyInTheBeast.pdf">
Beauty in the Beast: A Functional Semantics for the Awkward
Squad</a>. Haskell Workshop 2007.</li>
<li><a href=
"http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf">
Data types à la carte</a>. Accepted for publication in
JFP.</li>
</ul>
<h2>Feedback</h2><img style="float: right" width="102" height=
"35" src="www/cabal.png" alt="Cabal">
<p>If you have any comments or suggestions, please don't hesitate
to get in touch!</p><a href=
"http://www.cs.nott.ac.uk/~wss">Wouter Swierstra</a><br>
<script src="http://www.google-analytics.com/urchin.js" type=
"text/javascript">
</script><script type="text/javascript">
_uacct
= "UA-1372453-2"; urchinTracker();
</script>
</body>
</html>