4 This page discusses a framework that makes it possible to compute
5 fixpoints over arbitrary products of abstract types. The code is from
6 an Extended Basis library
7 (<!ViewGitFile(mltonlib,master,com/ssh/extended-basis/unstable/README)>).
9 First the signature of the framework
10 (<!ViewGitFile(mltonlib,master,com/ssh/extended-basis/unstable/public/generic/tie.sig)>):
13 sys::[./bin/InclGitFile.py mltonlib master com/ssh/extended-basis/unstable/public/generic/tie.sig 6:]
16 `fix` is a <:TypeIndexedValues:type-indexed> function. The type-index
17 parameter to `fix` is called a "witness". To compute fixpoints over
18 products, one uses the +*`+ operator to combine witnesses. To provide
19 a fixpoint combinator for an abstract type, one implements a witness
20 providing a thunk whose instantiation allocates a fresh, mutable proxy
21 and a procedure for updating the proxy with the solution. Naturally
22 this means that not all possible ways of computing a fixpoint of a
23 particular type are possible under the framework. The `pure`
24 combinator is a generalization of `tier`. The `iso` combinator is
25 provided for reusing existing witnesses.
27 Note that instead of using an infix operator, we could alternatively
28 employ an interface using <:Fold:>. Also, witnesses are eta-expanded
29 to work around the <:ValueRestriction:value restriction>, while
30 maintaining abstraction.
32 Here is the implementation
33 (<!ViewGitFile(mltonlib,master,com/ssh/extended-basis/unstable/detail/generic/tie.sml)>):
36 sys::[./bin/InclGitFile.py mltonlib master com/ssh/extended-basis/unstable/detail/generic/tie.sml 6:]
39 Let's then take a look at a couple of additional examples.
41 Here is a naive implementation of lazy promises:
44 structure Promise :> sig
46 val lazy : 'a Thunk.t -> 'a t
47 val force : 'a t -> 'a
54 type 'a t = 'a t' Ref.t
55 fun lazy f = ref (THUNK f)
59 | THUNK f => (t := VALUE (f ()) handle e => t := EXN e ; force t)
61 fun Y ? = Tie.tier (fn () => let
62 val r = lazy (raising Fix.Fix)
69 An example use of our naive lazy promises is to implement equally naive
73 structure Stream :> sig
75 val cons : 'a * 'a t -> 'a t
76 val get : 'a t -> ('a * 'a t) Option.t
79 datatype 'a t = IN of ('a * 'a t) Option.t Promise.t
80 fun cons (x, xs) = IN (Promise.lazy (fn () => SOME (x, xs)))
81 fun get (IN p) = Promise.force p
82 fun Y ? = Tie.iso Promise.Y (fn IN p => p, IN) ?
86 Note that above we make use of the `iso` combinator. Here is a finite
87 representation of an infinite stream of ones:
94 fix Y (fn ones => cons (1, ones))