[MLton-commit] r6423

[Vesa Karvonen]

Added experimental dependent product combinator for fixed point witnesses.

----------------------------------------------------------------------

U   mltonlib/trunk/com/ssh/extended-basis/unstable/detail/generic/tie.sml
U   mltonlib/trunk/com/ssh/extended-basis/unstable/public/generic/tie.sig

----------------------------------------------------------------------

Modified: mltonlib/trunk/com/ssh/extended-basis/unstable/detail/generic/tie.sml
===================================================================
--- mltonlib/trunk/com/ssh/extended-basis/unstable/detail/generic/tie.sml	2008-02-29 16:55:50 UTC (rev 6422)
+++ mltonlib/trunk/com/ssh/extended-basis/unstable/detail/generic/tie.sml	2008-02-29 17:01:58 UTC (rev 6423)
@@ -18,13 +18,14 @@
    in
       (b2a b, Fn.map iso fB)
    end
-   fun op *` (aT, bT) () () = let
+   fun product (aT, a2bT) () () = let
       val (a, fA) = aT () ()
-      val (b, fB) = bT () ()
+      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))

Modified: mltonlib/trunk/com/ssh/extended-basis/unstable/public/generic/tie.sig
===================================================================
--- mltonlib/trunk/com/ssh/extended-basis/unstable/public/generic/tie.sig	2008-02-29 16:55:50 UTC (rev 6422)
+++ mltonlib/trunk/com/ssh/extended-basis/unstable/public/generic/tie.sig	2008-02-29 17:01:58 UTC (rev 6423)
@@ -66,12 +66,17 @@
     * a witness.
     *)
 
-   val *` : 'a t * 'b t -> ('a, 'b) Product.t t
+   val product : 'a t * ('a -> 'b t) -> ('a, 'b) Product.t t
    (**
-    * Given witnesses for {'a} and {'b} produces a witness for the product
-    * {('a, 'b) Product.t}.  This is used when mutual recursion is needed.
+    * 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