<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta name="generator" content="Asciidoctor 2.0.26">
<title>Fixpoints</title>
<link rel="stylesheet" href="https://fonts.googleapis.com/css?family=Open+Sans:300,300italic,400,400italic,600,600italic%7CNoto+Serif:400,400italic,700,700italic%7CDroid+Sans+Mono:400,700">
<link rel="stylesheet" href="./asciidoctor.css">
<link rel="stylesheet" href="./mlton.css">

</head>
<body class="article">
<div id="mlton-header">
<div id="mlton-header-text">
<h2>
<a href="./Home">
MLton
20241230+git20251029+dfsg-5
</a>
</h2>
</div>
</div>
<div id="header">
<h1>Fixpoints</h1>
</div>
<div id="content">
<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"><code>README</code></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"><code>tie.sig</code></a>):</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">Unresolved directive in Fixpoints.adoc - include::https://raw.github.com/MLton/mltonlib/master/com/ssh/extended-basis/unstable/public/generic/tie.sig[indent=0,lines=6..-1]</code></pre>
</div>
</div>
<div class="paragraph">
<p><code>fix</code> is a <a href="TypeIndexedValues">type-indexed</a> function.  The type-index
parameter to <code>fix</code> is called a "witness".  To compute fixpoints over
products, one uses the <code>*`</code> 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 <code>pure</code>
combinator is a generalization of <code>tier</code>.  The <code>iso</code> 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"><code>tie.sml</code></a>):</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">Unresolved directive in Fixpoints.adoc - include::https://raw.github.com/MLton/mltonlib/master/com/ssh/extended-basis/unstable/detail/generic/tie.sml[indent=0,lines=6..-1]</code></pre>
</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">
<pre class="rouge highlight"><code data-lang="sml">structure Promise :&gt; sig
   type 'a t
   val lazy : 'a Thunk.t -&gt; 'a t
   val force : 'a t -&gt; 'a
   val Y : 'a t Tie.t
end = struct
   datatype 'a t' =
      EXN of exn
    | THUNK of 'a Thunk.t
    | VALUE of 'a
   type 'a t = 'a t' Ref.t
   fun lazy f = ref (THUNK f)
   fun force t =
      case !t
       of EXN e   =&gt; raise e
        | THUNK f =&gt; (t := VALUE (f ()) handle e =&gt; t := EXN e ; force t)
        | VALUE v =&gt; v
   fun Y ? = Tie.tier (fn () =&gt; let
                             val r = lazy (raising Fix.Fix)
                          in
                             (r, r &lt;\ op := o !)
                          end) ?
end</code></pre>
</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">
<pre class="rouge highlight"><code data-lang="sml">structure Stream :&gt; sig
   type 'a t
   val cons : 'a * 'a t -&gt; 'a t
   val get : 'a t -&gt; ('a * 'a t) Option.t
   val Y : 'a t Tie.t
end = struct
   datatype 'a t = IN of ('a * 'a t) Option.t Promise.t
   fun cons (x, xs) = IN (Promise.lazy (fn () =&gt; SOME (x, xs)))
   fun get (IN p) = Promise.force p
   fun Y ? = Tie.iso Promise.Y (fn IN p =&gt; p, IN) ?
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>Note that above we make use of the <code>iso</code> combinator.  Here is a finite
representation of an infinite stream of ones:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">val ones = let
   open Tie Stream
in
   fix Y (fn ones =&gt; cons (1, ones))
end</code></pre>
</div>
</div>
</div>
</body>
</html>