MLton

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 (README).

First the signature of the framework (tie.sig):

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

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

   val pure : ('a * 'a UnOp.t) Thunk.t -> '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 -> '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 -> 'a t
   (** {id x} is equivalent to {pure (const (x, id))}. *)

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

   val iso : 'b t -> ('a, 'b) Iso.t -> '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 -> 'b t) -> ('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 -> ('a, 'b) Product.t t
   (** {a *` b} is equivalent to {product (a, const b)}. *)

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

   (** == Particular Witnesses == *)

   val function : ('a -> 'b) t
   (** Witness for functions. *)
end

fix is a type-indexed function. The type-index parameter to fix is called a "witness". To compute fixpoints over products, one uses the *` 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 pure combinator is a generalization of tier. The iso combinator is provided for reusing existing witnesses.

Note that instead of using an infix operator, we could alternatively employ an interface using Fold. Also, witnesses are eta-expanded to work around the value restriction, while maintaining abstraction.

Here is the implementation (tie.sml):

structure Tie :> TIE = struct
   open Product
   infix &
   type 'a etaexp_dom = Unit.t
   type 'a etaexp_cod = ('a * 'a UnOp.t) Thunk.t
   type 'a etaexp = 'a etaexp_dom -> '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 & 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) => (a, Fn.const a o ua)) o th)
   fun id x = pure (Fn.const (x, Fn.id))
   fun function ? =
       pure (fn () => let
                   val r = ref (Basic.raising Fix.Fix)
                in
                   (fn x => !r x, fn f => (r := f ; f))
                end) ?
end

Let’s then take a look at a couple of additional examples.

Here is a naive implementation of lazy promises:

structure Promise :> sig
   type 'a t
   val lazy : 'a Thunk.t -> 'a t
   val force : 'a t -> '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   => raise e
        | THUNK f => (t := VALUE (f ()) handle e => t := EXN e ; force t)
        | VALUE v => v
   fun Y ? = Tie.tier (fn () => let
                             val r = lazy (raising Fix.Fix)
                          in
                             (r, r <\ op := o !)
                          end) ?
end

An example use of our naive lazy promises is to implement equally naive lazy streams:

structure Stream :> sig
   type 'a t
   val cons : 'a * 'a t -> 'a t
   val get : 'a t -> ('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 () => SOME (x, xs)))
   fun get (IN p) = Promise.force p
   fun Y ? = Tie.iso Promise.Y (fn IN p => p, IN) ?
end

Note that above we make use of the iso combinator. Here is a finite representation of an infinite stream of ones:

val ones = let
   open Tie Stream
in
   fix Y (fn ones => cons (1, ones))
end