[MLton-commit] r5801
Vesa Karvonen
vesak at mlton.org
Fri Jul 27 19:57:18 PDT 2007
No need to pass around monomorphic isomorphism.
----------------------------------------------------------------------
U mltonlib/trunk/org/mlton/vesak/tech/generics/lgd.sml
----------------------------------------------------------------------
Modified: mltonlib/trunk/org/mlton/vesak/tech/generics/lgd.sml
===================================================================
--- mltonlib/trunk/org/mlton/vesak/tech/generics/lgd.sml 2007-07-28 00:47:08 UTC (rev 5800)
+++ mltonlib/trunk/org/mlton/vesak/tech/generics/lgd.sml 2007-07-28 02:57:17 UTC (rev 5801)
@@ -31,7 +31,8 @@
*)
-(* The following code uses the Extended Basis Library. To try the code
+(*
+ The following code uses the Extended Basis Library. To try the code
with SML/NJ, run the following prefix before evaluating the rest:
val mltonLib = "../../../../.." ;
@@ -62,7 +63,8 @@
val Y : 'a t Tie.t
end
-(* The type variables in {CASES} are going to be mostly phantoms. The
+(*
+ * The type variables in {CASES} are going to be mostly phantoms. The
* structural cases of a generic are actually used by the framework at
* specific monomorphic types. The upshot of defining the structural
* cases as polymorphic functions in a structure is that they will be
@@ -74,51 +76,36 @@
structure Type = struct
datatype t =
- UNIT of Unit.t e
- | INT of Int.t e
- | SUM of t Sq.t * (u, u) Sum.t Thunk.t e
- | PROD of t Sq.t * (u, u) Product.t Thunk.t e
+ UNIT
+ | INT
+ | SUM of t Sq.t
+ | PROD of t Sq.t
| FIX of t Ref.t * t
| VAR of t Ref.t
fun Y ? =
Tie.pure
(fn () => let
- val r = ref (UNIT (undefined, undefined))
+ val r = ref UNIT
in
(VAR r, fn t => let val t = FIX (r, t) in r := t ; t end)
end) ?
end
-(* The universal type {u} and isomorphism {e} above implement the "poor
- * man's existentials" mentioned at the beginning. See [1] for the
- * Haskell version using existentials.
- *
- * Note the thunks in {SUM} and {PROD}. The idea is to perform coercions
- * lazily. For example, if you evaluate
- *
- *> equal (list int) ([], veryLongList)
- *
- * then only the first sum of the {veryLongList} should be coerced.
- *
- * Note also that the thunks do not appear in the {CASES}. The framework
- * handles data coercions automatically behind the scenes. This is
- * different from both Cheney & Hinze's and Weeks' approaches and leads to
- * comparatively concise definitions of generics (see {Eq} and {Ord} at
- * the end).
- *
- * Finally, note the {FIX} and {VAR} constructors. They are used to
- * encode recursive types. The point here is to make it possible to
- * implement a fixed point witness, using the {Tie} module from the
- * Extended Basis Library, for the type constructor of an arbitrary
- * generic (structural cases). IOW, we do not only compute a fixed point
- * of the type representation, but we also want to make it possible to
- * compute a fixed point of a given generic for the recursive type at
- * hand. In order to do this, we are very explicit about recursion.
+(*
+ * Note the {FIX} and {VAR} constructors. They are used to encode
+ * recursive types. The point here is to make it possible to implement a
+ * fixed point witness, using the {Tie} module from the Extended Basis
+ * Library, for the type constructor of an arbitrary generic (structural
+ * cases). IOW, we do not only compute a fixed point of the type
+ * representation, but we also want to make it possible to compute a fixed
+ * point of a given generic for the recursive type at hand. In order to
+ * do this, we are very explicit about recursion.
*)
-(* Type representation cases.
+(*
+ * Type representation cases.
*
* Somewhat tricky, but luckily this is a one time cost.
*)
@@ -126,39 +113,53 @@
structure Type (* : CASES -- Sealed later! *) = struct
open Type
datatype 'a t = T of Type.t * 'a e
- local
- val unit = Univ.newIso ()
- val int = Univ.newIso ()
- val sum = Univ.newIso ()
- val prod = Univ.newIso ()
+
+ val isoUnit : Unit.t e = Univ.newIso ()
+ val isoInt : Int.t e = Univ.newIso ()
+ val isoSum : (u, u) Sum.t Thunk.t e = Univ.newIso ()
+ val isoProd : (u, u) Product.t Thunk.t e = Univ.newIso ()
+
+ val unit = T (UNIT, isoUnit)
+ val int = T (INT, isoInt)
+ fun iso (T (bU, bIu)) aIb = T (bU, bIu <--> aIb)
+ fun op +` (T (lU, (l2u, u2l)), T (rU, (r2u, u2r))) = let
+ val isoPoly = (fn INL l => (fn () => INL (l2u l))
+ | INR r => (fn () => INR (r2u r)),
+ Sum.map (u2l, u2r) o pass ())
in
- val unit = T (UNIT unit, unit)
- val int = T (INT int, int)
- fun iso (T (bU, bIu)) aIb = T (bU, bIu <--> aIb)
- fun op +` (T (lU, (l2u, u2l)), T (rU, (r2u, u2r))) = let
- val pIu = (fn INL l => (fn () => INL (l2u l))
- | INR r => (fn () => INR (r2u r)),
- Sum.map (u2l, u2r) o pass ())
- in
- T (SUM ((lU, rU), sum), sum <--> pIu)
- end
- fun op *` (T (lU, (l2u, u2l)), T (rU, (r2u, u2r))) = let
- val pIu = (fn l & r => (fn () => l2u l & r2u r),
- Product.map (u2l, u2r) o pass ())
- in
- T (PROD ((lU, rU), prod), prod <--> pIu)
- end
- fun Y ? = let
- open Tie
- in
- iso (tuple2 (Type.Y, tuple2 (function, function)))
- (fn T ? => ?, T)
- end ?
+ T (SUM (lU, rU), isoSum <--> isoPoly)
end
+ fun op *` (T (lU, (l2u, u2l)), T (rU, (r2u, u2r))) = let
+ val isoPoly = (fn l & r => (fn () => l2u l & r2u r),
+ Product.map (u2l, u2r) o pass ())
+ in
+ T (PROD (lU, rU), isoProd <--> isoPoly)
+ end
+ fun Y ? = let
+ open Tie
+ in
+ iso (tuple2 (Type.Y, tuple2 (function, function)))
+ (fn T ? => ?, T)
+ end ?
end
-(* Note the use of a second, type-parameterized, isomorphism. The earlier
- * type representation datatype was non-parameterized.
+(*
+ * The universal type {u} and isomorphism {e} above implement the "poor
+ * man's existentials" mentioned at the beginning. See [1] for the
+ * (trivial) Haskell version using existentials.
+ *
+ * Note the thunks in the sum and product cases. The idea is to perform
+ * coercions lazily. For example, if you evaluate
+ *
+ *> equal (list int) ([], veryLongList)
+ *
+ * then only the first sum of the {veryLongList} should be coerced.
+ *
+ * Note also that the thunks do not appear in the {CASES}. The framework
+ * handles data coercions automatically behind the scenes. This is
+ * different from both Cheney & Hinze's and Weeks' approaches and leads to
+ * comparatively concise definitions of generics (see {Eq} and {Ord} at
+ * the end).
*)
@@ -170,7 +171,11 @@
end
-(* Functor to build a generic given the structural cases. *)
+(*
+ * Functor to build a generic given the structural cases.
+ *
+ * What this does is to morph the structural cases to work
+ *)
functor Generic (C : CASES) : GENERIC = struct
open Type C
@@ -178,40 +183,46 @@
fun lookup r = Option.map Pair.snd o List.find (eq r o Pair.fst) o !
fun insert (r, g) p = if isSome (lookup r p) then () else List.push p (r, g)
- fun osi ? = iso ? o Iso.swap
+ val unit = iso unit (Iso.swap isoUnit)
+ val int = iso int (Iso.swap isoInt)
+ val isoSum = Iso.swap (isoSum <--> Thunk.iso)
+ val isoProd = Iso.swap (isoProd <--> Thunk.iso)
+
fun mk (p, t) =
case t
- of UNIT e => osi unit e
- | INT e => osi int e
- | SUM ((l, r), e) => osi (mk (p, l) +` mk (p, r)) (e <--> Thunk.iso)
- | PROD ((l, r), e) => osi (mk (p, l) *` mk (p, r)) (e <--> Thunk.iso)
- | FIX (rT, t) => (case lookup rT p of
- SOME r => r
- | NONE =>
- Tie.fix Y (fn g => (insert (rT, g) p
- ; mk (p, t))))
- | VAR rT => (case lookup rT p of
- SOME r => r
- | NONE => mk (p, !rT))
- fun apply (Type.T (tU, e)) =
- iso (mk (ref [], tU)) e
+ of UNIT => unit
+ | INT => int
+ | SUM (l, r) => iso (mk (p, l) +` mk (p, r)) isoSum
+ | PROD (l, r) => iso (mk (p, l) *` mk (p, r)) isoProd
+ | VAR r => mk (p, !r)
+ | FIX (r, t) => case lookup r p
+ of SOME g => g
+ | NONE =>
+ Tie.fix Y (fn g => (insert (r, g) p ; mk (p, t)))
+
+ fun apply (T (tU, e)) = iso (mk (ref [], tU)) e
end
-(* Note the treatment of recursive types. To compute fixed points of the
+(*
+ * Note the treatment of recursive types. To compute fixed points of the
* generics (structural cases) we keep a (mutable) map of computed fixed
* points. Note that it is possible to get to a {VAR} without going
* through a corresponding {FIX}, which is why the above calls {mk} in the
- * {VAR} case (the reference {rT} points to the corresponding {FIX}).
+ * {VAR} case (the reference {r} points to the corresponding {FIX}).
*)
+
(* Finally we seal the type representation. *)
+
structure Type : CASES = Type
+
(* Note that (all of) the above is part of the framework (one time cost). *)
(* Then we add a couple of type representation constructors. *)
+
structure Type = struct
open Type
@@ -251,9 +262,12 @@
(fn USELESS ? => ?, USELESS))
end
-(* Below are implementations of generic equality and ordering relations.
+
+(*
+ * Below are implementations of generic equality and ordering relations.
* The type constraints are for just for clarity.
*)
+
structure Eq = Generic
(open BinPr
fun iso b (a2b, _) = map a2b b
@@ -278,8 +292,9 @@
val compare : 'a Type.t -> 'a Cmp.t =
Ord.apply
-(* The above certainly works and the approach could be extended somewhat
- * further. Try the equal and compare functions in a REPL!
+(*
+ * The above certainly works and the approach could be extended somewhat
+ * further. Try the {equal} and {compare} functions in a REPL!
*
* A problem with this approach is mutable types. They can not be
* supported through (the ideal) structural cases with specs of the
@@ -292,7 +307,7 @@
* universal type are likely to have a significant cost. This problem is
* mostly due to lack of true existentials.
*
- * Even with true existentials, this approach would suffer from the
+ * Even with existentials, this approach would suffer from the
* inflexibility that the user can not specify ad hoc cases [2] for
* specific datatypes. For example, picklers based on this approach need
* to encode lists with a spine---unless the list type constructor is
More information about the MLton-commit
mailing list