<!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.20">
<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-ok1
</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">(**
 * A framework for computing fixpoints.
 *
 * In a strict language you sometimes want to provide a fixpoint
 * combinator for an abstract type {t} to make it possible to write
 * recursive definitions.  Unfortunately, a single combinator {fix} of the
 * type {(t -&gt; t) -&gt; t} does not support mutual recursion.  To support
 * mutual recursion, you would need to provide a family of fixpoint
 * combinators having types of the form {(u -&gt; u) -&gt; u} where {u} is a
 * type of the form {t * ... * t}.  Unfortunately, even such a family of
 * fixpoint combinators does not support mutual recursion over different
 * abstract types.
 *)
signature TIE = sig
   include ETAEXP'
   type 'a t = 'a etaexp
   (** The type of fixpoint witnesses. *)

   val fix : 'a t -&gt; 'a Fix.t
   (**
    * Produces a fixpoint combinator from the given witness.  For example,
    * one can make a mutually recursive definition of functions:
    *
    *&gt; val isEven &amp; isOdd =
    *&gt;     let open Tie in fix (function *` function) end
    *&gt;        (fn isEven &amp; isOdd =&gt;
    *&gt;            (fn 0 =&gt; true
    *&gt;              | 1 =&gt; false
    *&gt;              | n =&gt; isOdd (n-1)) &amp;
    *&gt;            (fn 0 =&gt; false
    *&gt;              | 1 =&gt; true
    *&gt;              | n =&gt; isEven (n-1)))
    *)

   (** == Making New Witnesses == *)

   val pure : ('a * 'a UnOp.t) Thunk.t -&gt; 'a t
   (**
    * {pure} is a more general version of {tier}.  It is mostly useful for
    * computing fixpoints in a non-imperative manner.
    *)

   val tier : ('a * 'a Effect.t) Thunk.t -&gt; 'a t
   (**
    * {tier} is used to define fixpoint witnesses for new abstract types
    * by providing a thunk whose instantiation allocates a mutable proxy
    * and a procedure for updating it with the result.
    *)

   val id : 'a -&gt; 'a t
   (** {id x} is equivalent to {pure (const (x, id))}. *)

   (** == Combining Existing Witnesses == *)

   val iso : 'b t -&gt; ('a, 'b) Iso.t -&gt; 'a t
   (**
    * Given an isomorphism between {'a} and {'b} and a witness for {'b},
    * produces a witness for {'a}.  This is useful when you have a new
    * type that is isomorphic to some old type for which you already have
    * a witness.
    *)

   val product : 'a t * ('a -&gt; 'b t) -&gt; ('a, 'b) Product.t t
   (**
    * Dependent product combinator.  Given a witness for {'a} and a
    * constructor from a {'a} to witness for {'b}, produces a witness for
    * the product {('a, 'b) Product.t}.  The constructor for {'b} should
    * not access the (proxy) value {'a} before it has been fixed.
    *)

   val *` : 'a t * 'b t -&gt; ('a, 'b) Product.t t
   (** {a *` b} is equivalent to {product (a, const b)}. *)

   val tuple2 : 'a t * 'b t -&gt; ('a * 'b) t
   (**
    * Given witnesses for {'a} and {'b} produces a witness for the product
    * {'a * 'b}.
    *)

   (** == Particular Witnesses == *)

   val function : ('a -&gt; 'b) t
   (** Witness for functions. *)
end</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">structure Tie :&gt; TIE = struct
   open Product
   infix &amp;
   type 'a etaexp_dom = Unit.t
   type 'a etaexp_cod = ('a * 'a UnOp.t) Thunk.t
   type 'a etaexp = 'a etaexp_dom -&gt; 'a etaexp_cod
   type 'a t = 'a etaexp
   fun fix aT f = let val (a, ta) = aT () () in ta (f a) end
   val pure = Thunk.mk
   fun iso bT (iso as (_, b2a)) () () = let
      val (b, fB) = bT () ()
   in
      (b2a b, Fn.map iso fB)
   end
   fun product (aT, a2bT) () () = let
      val (a, fA) = aT () ()
      val (b, fB) = a2bT a () ()
   in
      (a &amp; b, Product.map (fA, fB))
   end
   (* The rest are not primitive operations. *)
   fun op *` (aT, bT) = product (aT, Fn.const bT)
   fun tuple2 ab = iso (op *` ab) Product.isoTuple2
   fun tier th = pure ((fn (a, ua) =&gt; (a, Fn.const a o ua)) o th)
   fun id x = pure (Fn.const (x, Fn.id))
   fun function ? =
       pure (fn () =&gt; let
                   val r = ref (Basic.raising Fix.Fix)
                in
                   (fn x =&gt; !r x, fn f =&gt; (r := f ; f))
                end) ?
end</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>