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
```