File: Fixpoints

package info (click to toggle)
mlton 20130715-3
  • links: PTS
  • area: main
  • in suites: stretch
  • size: 60,900 kB
  • ctags: 69,386
  • sloc: xml: 34,418; ansic: 17,399; lisp: 2,879; makefile: 1,605; sh: 1,254; pascal: 256; python: 143; asm: 97
file content (235 lines) | stat: -rw-r--r-- 41,584 bytes parent folder | download 
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
 
<!DOCTYPE html>
<html lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="generator" content="AsciiDoc 8.6.8">
<title>Fixpoints</title>
<link rel="stylesheet" href="./asciidoc.css" type="text/css">
<link rel="stylesheet" href="./pygments.css" type="text/css">


<script type="text/javascript" src="./asciidoc.js"></script>
<script type="text/javascript">
/*<![CDATA[*/
asciidoc.install();
/*]]>*/
</script>
<link rel="stylesheet" href="./mlton.css" type="text/css"/>
</head>
<body class="article">
<div id="banner">
<div id="banner-home">
<a href="./Home">MLton 20130715</a>
</div>
</div>
<div id="header">
<h1>Fixpoints</h1>
</div>
<div id="content">
<div id="preamble">
<div class="sectionbody">
<div class="paragraph"><p>This page discusses a framework that makes it possible to compute
fixpoints over arbitrary products of abstract types.  The code is from
an Extended Basis library
(<a href="https://github.com/MLton/mltonlib/blob/master/com/ssh/extended-basis/unstable/README"><span class="monospaced">README</span></a>).</p></div>
<div class="paragraph"><p>First the signature of the framework
(<a href="https://github.com/MLton/mltonlib/blob/master/com/ssh/extended-basis/unstable/public/generic/tie.sig"><span class="monospaced">tie.sig</span></a>):</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="cm">(**</span>
<span class="cm"> * A framework for computing fixpoints.</span>
<span class="cm"> *</span>
<span class="cm"> * In a strict language you sometimes want to provide a fixpoint</span>
<span class="cm"> * combinator for an abstract type {t} to make it possible to write</span>
<span class="cm"> * recursive definitions.  Unfortunately, a single combinator {fix} of the</span>
<span class="cm"> * type {(t -&gt; t) -&gt; t} does not support mutual recursion.  To support</span>
<span class="cm"> * mutual recursion, you would need to provide a family of fixpoint</span>
<span class="cm"> * combinators having types of the form {(u -&gt; u) -&gt; u} where {u} is a</span>
<span class="cm"> * type of the form {t * ... * t}.  Unfortunately, even such a family of</span>
<span class="cm"> * fixpoint combinators does not support mutual recursion over different</span>
<span class="cm"> * abstract types.</span>
<span class="cm"> *)</span><span class="w"></span>
<span class="k">signature</span><span class="w"> </span><span class="n">TIE</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="k">sig</span><span class="w"></span>
<span class="w">   </span><span class="k">include</span><span class="w"> </span><span class="n">ETAEXP&#39;</span><span class="w"></span>
<span class="w">   </span><span class="k">type</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">etaexp</span><span class="w"></span>
<span class="w">   </span><span class="cm">(** The type of fixpoint witnesses. *)</span><span class="w"></span>

<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">fix</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">Fix</span><span class="p">.</span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="cm">(**</span>
<span class="cm">    * Produces a fixpoint combinator from the given witness.  For example,</span>
<span class="cm">    * one can make a mutually recursive definition of functions:</span>
<span class="cm">    *</span>
<span class="cm">    *&gt; val isEven &amp; isOdd =</span>
<span class="cm">    *&gt;     let open Tie in fix (function *` function) end</span>
<span class="cm">    *&gt;        (fn isEven &amp; isOdd =&gt;</span>
<span class="cm">    *&gt;            (fn 0 =&gt; true</span>
<span class="cm">    *&gt;              | 1 =&gt; false</span>
<span class="cm">    *&gt;              | n =&gt; isOdd (n-1)) &amp;</span>
<span class="cm">    *&gt;            (fn 0 =&gt; false</span>
<span class="cm">    *&gt;              | 1 =&gt; true</span>
<span class="cm">    *&gt;              | n =&gt; isEven (n-1)))</span>
<span class="cm">    *)</span><span class="w"></span>

<span class="w">   </span><span class="cm">(** == Making New Witnesses == *)</span><span class="w"></span>

<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">pure</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">UnOp</span><span class="p">.</span><span class="n">t</span><span class="p">)</span><span class="w"> </span><span class="n">Thunk</span><span class="p">.</span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="cm">(**</span>
<span class="cm">    * {pure} is a more general version of {tier}.  It is mostly useful for</span>
<span class="cm">    * computing fixpoints in a non-imperative manner.</span>
<span class="cm">    *)</span><span class="w"></span>

<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">tier</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">Effect</span><span class="p">.</span><span class="n">t</span><span class="p">)</span><span class="w"> </span><span class="n">Thunk</span><span class="p">.</span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="cm">(**</span>
<span class="cm">    * {tier} is used to define fixpoint witnesses for new abstract types</span>
<span class="cm">    * by providing a thunk whose instantiation allocates a mutable proxy</span>
<span class="cm">    * and a procedure for updating it with the result.</span>
<span class="cm">    *)</span><span class="w"></span>

<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">id</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="cm">(** {id x} is equivalent to {pure (const (x, id))}. *)</span><span class="w"></span>

<span class="w">   </span><span class="cm">(** == Combining Existing Witnesses == *)</span><span class="w"></span>

<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">iso</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;b</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="p">,</span><span class="w"> </span><span class="n">&#39;b</span><span class="p">)</span><span class="w"> </span><span class="n">Iso</span><span class="p">.</span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="cm">(**</span>
<span class="cm">    * Given an isomorphism between {&#39;a} and {&#39;b} and a witness for {&#39;b},</span>
<span class="cm">    * produces a witness for {&#39;a}.  This is useful when you have a new</span>
<span class="cm">    * type that is isomorphic to some old type for which you already have</span>
<span class="cm">    * a witness.</span>
<span class="cm">    *)</span><span class="w"></span>

<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">product</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;b</span><span class="w"> </span><span class="n">t</span><span class="p">)</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="p">,</span><span class="w"> </span><span class="n">&#39;b</span><span class="p">)</span><span class="w"> </span><span class="n">Product</span><span class="p">.</span><span class="n">t</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="cm">(**</span>
<span class="cm">    * Dependent product combinator.  Given a witness for {&#39;a} and a</span>
<span class="cm">    * constructor from a {&#39;a} to witness for {&#39;b}, produces a witness for</span>
<span class="cm">    * the product {(&#39;a, &#39;b) Product.t}.  The constructor for {&#39;b} should</span>
<span class="cm">    * not access the (proxy) value {&#39;a} before it has been fixed.</span>
<span class="cm">    *)</span><span class="w"></span>

<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">*`</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">&#39;b</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="p">,</span><span class="w"> </span><span class="n">&#39;b</span><span class="p">)</span><span class="w"> </span><span class="n">Product</span><span class="p">.</span><span class="n">t</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="cm">(** {a *` b} is equivalent to {product (a, const b)}. *)</span><span class="w"></span>

<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">tuple2</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">&#39;b</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">&#39;b</span><span class="p">)</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="cm">(**</span>
<span class="cm">    * Given witnesses for {&#39;a} and {&#39;b} produces a witness for the product</span>
<span class="cm">    * {&#39;a * &#39;b}.</span>
<span class="cm">    *)</span><span class="w"></span>

<span class="w">   </span><span class="cm">(** == Particular Witnesses == *)</span><span class="w"></span>

<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">function</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;b</span><span class="p">)</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="cm">(** Witness for functions. *)</span><span class="w"></span>
<span class="k">end</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p><span class="monospaced">fix</span> is a <a href="TypeIndexedValues">type-indexed</a> function.  The type-index
parameter to <span class="monospaced">fix</span> is called a "witness".  To compute fixpoints over
products, one uses the <span class="monospaced">*&grave;</span> operator to combine witnesses.  To provide
a fixpoint combinator for an abstract type, one implements a witness
providing a thunk whose instantiation allocates a fresh, mutable proxy
and a procedure for updating the proxy with the solution.  Naturally
this means that not all possible ways of computing a fixpoint of a
particular type are possible under the framework.  The <span class="monospaced">pure</span>
combinator is a generalization of <span class="monospaced">tier</span>.  The <span class="monospaced">iso</span> combinator is
provided for reusing existing witnesses.</p></div>
<div class="paragraph"><p>Note that instead of using an infix operator, we could alternatively
employ an interface using <a href="Fold">Fold</a>.  Also, witnesses are eta-expanded
to work around the <a href="ValueRestriction">value restriction</a>, while
maintaining abstraction.</p></div>
<div class="paragraph"><p>Here is the implementation
(<a href="https://github.com/MLton/mltonlib/blob/master/com/ssh/extended-basis/unstable/detail/generic/tie.sml"><span class="monospaced">tie.sml</span></a>):</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">structure</span><span class="w"> </span><span class="n">Tie</span><span class="w"> </span><span class="p">:&gt;</span><span class="w"> </span><span class="n">TIE</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="k">struct</span><span class="w"></span>
<span class="w">   </span><span class="k">open</span><span class="w"> </span><span class="n">Product</span><span class="w"></span>
<span class="w">   </span><span class="k">infix</span><span class="w"> </span><span class="n">&amp;</span><span class="w"></span>
<span class="w">   </span><span class="k">type</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">etaexp_dom</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">Unit</span><span class="p">.</span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="k">type</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">etaexp_cod</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">UnOp</span><span class="p">.</span><span class="n">t</span><span class="p">)</span><span class="w"> </span><span class="n">Thunk</span><span class="p">.</span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="k">type</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">etaexp</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">etaexp_dom</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">etaexp_cod</span><span class="w"></span>
<span class="w">   </span><span class="k">type</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">etaexp</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">fix</span><span class="w"> </span><span class="n">aT</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="k">let</span><span class="w"> </span><span class="k">val</span><span class="w"> </span><span class="p">(</span><span class="n">a</span><span class="p">,</span><span class="w"> </span><span class="n">ta</span><span class="p">)</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">aT</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">ta</span><span class="w"> </span><span class="p">(</span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="k">end</span><span class="w"></span>
<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">pure</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">Thunk</span><span class="p">.</span><span class="n">mk</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">iso</span><span class="w"> </span><span class="n">bT</span><span class="w"> </span><span class="p">(</span><span class="n">iso</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="p">(_,</span><span class="w"> </span><span class="n">b2a</span><span class="p">))</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="k">let</span><span class="w"></span>
<span class="w">      </span><span class="k">val</span><span class="w"> </span><span class="p">(</span><span class="n">b</span><span class="p">,</span><span class="w"> </span><span class="n">fB</span><span class="p">)</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">bT</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">()</span><span class="w"></span>
<span class="w">   </span><span class="k">in</span><span class="w"></span>
<span class="w">      </span><span class="p">(</span><span class="n">b2a</span><span class="w"> </span><span class="n">b</span><span class="p">,</span><span class="w"> </span><span class="n">Fn</span><span class="p">.</span><span class="n">map</span><span class="w"> </span><span class="n">iso</span><span class="w"> </span><span class="n">fB</span><span class="p">)</span><span class="w"></span>
<span class="w">   </span><span class="k">end</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">product</span><span class="w"> </span><span class="p">(</span><span class="n">aT</span><span class="p">,</span><span class="w"> </span><span class="n">a2bT</span><span class="p">)</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="k">let</span><span class="w"></span>
<span class="w">      </span><span class="k">val</span><span class="w"> </span><span class="p">(</span><span class="n">a</span><span class="p">,</span><span class="w"> </span><span class="n">fA</span><span class="p">)</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">aT</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">()</span><span class="w"></span>
<span class="w">      </span><span class="k">val</span><span class="w"> </span><span class="p">(</span><span class="n">b</span><span class="p">,</span><span class="w"> </span><span class="n">fB</span><span class="p">)</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">a2bT</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">()</span><span class="w"></span>
<span class="w">   </span><span class="k">in</span><span class="w"></span>
<span class="w">      </span><span class="p">(</span><span class="n">a</span><span class="w"> </span><span class="n">&amp;</span><span class="w"> </span><span class="n">b</span><span class="p">,</span><span class="w"> </span><span class="n">Product</span><span class="p">.</span><span class="n">map</span><span class="w"> </span><span class="p">(</span><span class="n">fA</span><span class="p">,</span><span class="w"> </span><span class="n">fB</span><span class="p">))</span><span class="w"></span>
<span class="w">   </span><span class="k">end</span><span class="w"></span>
<span class="w">   </span><span class="cm">(* The rest are not primitive operations. *)</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="k">op</span><span class="w"> </span><span class="n">*`</span><span class="w"> </span><span class="p">(</span><span class="n">aT</span><span class="p">,</span><span class="w"> </span><span class="n">bT</span><span class="p">)</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">product</span><span class="w"> </span><span class="p">(</span><span class="n">aT</span><span class="p">,</span><span class="w"> </span><span class="n">Fn</span><span class="p">.</span><span class="n">const</span><span class="w"> </span><span class="n">bT</span><span class="p">)</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">tuple2</span><span class="w"> </span><span class="n">ab</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">iso</span><span class="w"> </span><span class="p">(</span><span class="k">op</span><span class="w"> </span><span class="n">*`</span><span class="w"> </span><span class="n">ab</span><span class="p">)</span><span class="w"> </span><span class="n">Product</span><span class="p">.</span><span class="n">isoTuple2</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">tier</span><span class="w"> </span><span class="n">th</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">pure</span><span class="w"> </span><span class="p">((</span><span class="k">fn</span><span class="w"> </span><span class="p">(</span><span class="n">a</span><span class="p">,</span><span class="w"> </span><span class="n">ua</span><span class="p">)</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="p">(</span><span class="n">a</span><span class="p">,</span><span class="w"> </span><span class="n">Fn</span><span class="p">.</span><span class="n">const</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">o</span><span class="w"> </span><span class="n">ua</span><span class="p">))</span><span class="w"> </span><span class="n">o</span><span class="w"> </span><span class="n">th</span><span class="p">)</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">id</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">pure</span><span class="w"> </span><span class="p">(</span><span class="n">Fn</span><span class="p">.</span><span class="n">const</span><span class="w"> </span><span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="n">Fn</span><span class="p">.</span><span class="n">id</span><span class="p">))</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">function</span><span class="w"> </span><span class="n">?</span><span class="w"> </span><span class="p">=</span><span class="w"></span>
<span class="w">       </span><span class="n">pure</span><span class="w"> </span><span class="p">(</span><span class="k">fn</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="k">let</span><span class="w"></span>
<span class="w">                   </span><span class="k">val</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">ref</span><span class="w"> </span><span class="p">(</span><span class="n">Basic</span><span class="p">.</span><span class="n">raising</span><span class="w"> </span><span class="n">Fix</span><span class="p">.</span><span class="n">Fix</span><span class="p">)</span><span class="w"></span>
<span class="w">                </span><span class="k">in</span><span class="w"></span>
<span class="w">                   </span><span class="p">(</span><span class="k">fn</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="n">!r</span><span class="w"> </span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="k">fn</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="p">(</span><span class="n">r</span><span class="w"> </span><span class="n">:=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="p">;</span><span class="w"> </span><span class="n">f</span><span class="p">))</span><span class="w"></span>
<span class="w">                </span><span class="k">end</span><span class="p">)</span><span class="w"> </span><span class="n">?</span><span class="w"></span>
<span class="k">end</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>Let&#8217;s then take a look at a couple of additional examples.</p></div>
<div class="paragraph"><p>Here is a naive implementation of lazy promises:</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">structure</span><span class="w"> </span><span class="n">Promise</span><span class="w"> </span><span class="p">:&gt;</span><span class="w"> </span><span class="k">sig</span><span class="w"></span>
<span class="w">   </span><span class="k">type</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">lazy</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">Thunk</span><span class="p">.</span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">force</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"></span>
<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">Y</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="n">Tie</span><span class="p">.</span><span class="n">t</span><span class="w"></span>
<span class="k">end</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="k">struct</span><span class="w"></span>
<span class="w">   </span><span class="k">datatype</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t&#39;</span><span class="w"> </span><span class="p">=</span><span class="w"></span>
<span class="w">      </span><span class="n">EXN</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">exn</span><span class="w"></span>
<span class="w">    </span><span class="p">|</span><span class="w"> </span><span class="n">THUNK</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">Thunk</span><span class="p">.</span><span class="n">t</span><span class="w"></span>
<span class="w">    </span><span class="p">|</span><span class="w"> </span><span class="n">VALUE</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"></span>
<span class="w">   </span><span class="k">type</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t&#39;</span><span class="w"> </span><span class="n">Ref</span><span class="p">.</span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">lazy</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">ref</span><span class="w"> </span><span class="p">(</span><span class="n">THUNK</span><span class="w"> </span><span class="n">f</span><span class="p">)</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">force</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"></span>
<span class="w">      </span><span class="k">case</span><span class="w"> </span><span class="n">!t</span><span class="w"></span>
<span class="w">       </span><span class="k">of</span><span class="w"> </span><span class="n">EXN</span><span class="w"> </span><span class="n">e</span><span class="w">   </span><span class="p">=&gt;</span><span class="w"> </span><span class="k">raise</span><span class="w"> </span><span class="n">e</span><span class="w"></span>
<span class="w">        </span><span class="p">|</span><span class="w"> </span><span class="n">THUNK</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="p">(</span><span class="n">t</span><span class="w"> </span><span class="n">:=</span><span class="w"> </span><span class="n">VALUE</span><span class="w"> </span><span class="p">(</span><span class="n">f</span><span class="w"> </span><span class="p">())</span><span class="w"> </span><span class="k">handle</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="n">:=</span><span class="w"> </span><span class="n">EXN</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="p">;</span><span class="w"> </span><span class="n">force</span><span class="w"> </span><span class="n">t</span><span class="p">)</span><span class="w"></span>
<span class="w">        </span><span class="p">|</span><span class="w"> </span><span class="n">VALUE</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="n">v</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">Y</span><span class="w"> </span><span class="n">?</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">Tie</span><span class="p">.</span><span class="n">tier</span><span class="w"> </span><span class="p">(</span><span class="k">fn</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="k">let</span><span class="w"></span>
<span class="w">                             </span><span class="k">val</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">lazy</span><span class="w"> </span><span class="p">(</span><span class="n">raising</span><span class="w"> </span><span class="n">Fix</span><span class="p">.</span><span class="n">Fix</span><span class="p">)</span><span class="w"></span>
<span class="w">                          </span><span class="k">in</span><span class="w"></span>
<span class="w">                             </span><span class="p">(</span><span class="n">r</span><span class="p">,</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="n">&lt;\</span><span class="w"> </span><span class="k">op</span><span class="w"> </span><span class="n">:=</span><span class="w"> </span><span class="n">o</span><span class="w"> </span><span class="n">!</span><span class="p">)</span><span class="w"></span>
<span class="w">                          </span><span class="k">end</span><span class="p">)</span><span class="w"> </span><span class="n">?</span><span class="w"></span>
<span class="k">end</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>An example use of our naive lazy promises is to implement equally naive
lazy streams:</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">structure</span><span class="w"> </span><span class="n">Stream</span><span class="w"> </span><span class="p">:&gt;</span><span class="w"> </span><span class="k">sig</span><span class="w"></span>
<span class="w">   </span><span class="k">type</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">cons</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">get</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="p">)</span><span class="w"> </span><span class="n">Option</span><span class="p">.</span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="k">val</span><span class="w"> </span><span class="n">Y</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="n">Tie</span><span class="p">.</span><span class="n">t</span><span class="w"></span>
<span class="k">end</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="k">struct</span><span class="w"></span>
<span class="w">   </span><span class="k">datatype</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">IN</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">&#39;a</span><span class="w"> </span><span class="n">t</span><span class="p">)</span><span class="w"> </span><span class="n">Option</span><span class="p">.</span><span class="n">t</span><span class="w"> </span><span class="n">Promise</span><span class="p">.</span><span class="n">t</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">cons</span><span class="w"> </span><span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="n">xs</span><span class="p">)</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">IN</span><span class="w"> </span><span class="p">(</span><span class="n">Promise</span><span class="p">.</span><span class="n">lazy</span><span class="w"> </span><span class="p">(</span><span class="k">fn</span><span class="w"> </span><span class="p">()</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="n">SOME</span><span class="w"> </span><span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="n">xs</span><span class="p">)))</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">get</span><span class="w"> </span><span class="p">(</span><span class="n">IN</span><span class="w"> </span><span class="n">p</span><span class="p">)</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">Promise</span><span class="p">.</span><span class="n">force</span><span class="w"> </span><span class="n">p</span><span class="w"></span>
<span class="w">   </span><span class="k">fun</span><span class="w"> </span><span class="n">Y</span><span class="w"> </span><span class="n">?</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">Tie</span><span class="p">.</span><span class="n">iso</span><span class="w"> </span><span class="n">Promise</span><span class="p">.</span><span class="n">Y</span><span class="w"> </span><span class="p">(</span><span class="k">fn</span><span class="w"> </span><span class="n">IN</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="n">p</span><span class="p">,</span><span class="w"> </span><span class="n">IN</span><span class="p">)</span><span class="w"> </span><span class="n">?</span><span class="w"></span>
<span class="k">end</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>Note that above we make use of the <span class="monospaced">iso</span> combinator.  Here is a finite
representation of an infinite stream of ones:</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">val</span><span class="w"> </span><span class="n">ones</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="k">let</span><span class="w"></span>
<span class="w">   </span><span class="k">open</span><span class="w"> </span><span class="n">Tie</span><span class="w"> </span><span class="n">Stream</span><span class="w"></span>
<span class="k">in</span><span class="w"></span>
<span class="w">   </span><span class="n">fix</span><span class="w"> </span><span class="n">Y</span><span class="w"> </span><span class="p">(</span><span class="k">fn</span><span class="w"> </span><span class="n">ones</span><span class="w"> </span><span class="p">=&gt;</span><span class="w"> </span><span class="n">cons</span><span class="w"> </span><span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="w"> </span><span class="n">ones</span><span class="p">))</span><span class="w"></span>
<span class="k">end</span><span class="w"></span>
</pre></div></div></div>
</div>
</div>
</div>
<div id="footnotes"><hr></div>
<div id="footer">
<div id="footer-text">
</div>
<div id="footer-badges">
</div>
</div>
</body>
</html>