1557 ML{*signature UNIVERSAL_TYPE =

  1558 sig

  1559   type t

  1560 

  1561   val embed: unit -> ('a -> t) * (t -> 'a option)

  1562 end*}

  1563 

  1564 ML{*structure U:> UNIVERSAL_TYPE =

  1565    struct

  1566       type t = exn

  1567 

  1568       fun 'a embed () =

  1569          let

  1570             exception E of 'a

  1571             fun project (e: t): 'a option =

  1572                case e of

  1573                   E a => SOME a

  1574                 | _ => NONE

  1575          in

  1576             (E, project)

  1577          end

  1578    end*}

  1579 

  1580 text {*

  1581   The idea is that type t is the universal type and that each call to embed

  1582   returns a new pair of functions (inject, project), where inject embeds a

  1583   value into the universal type and project extracts the value from the

  1584   universal type. A pair (inject, project) returned by embed works together in

  1585   that project u will return SOME v if and only if u was created by inject

  1586   v. If u was created by a different function inject', then project returns

  1587   NONE.

  1588 

  1589   in library.ML

  1590 *}

  1591 

  1592 ML_val{*structure Object = struct type T = exn end; *}

  1593 

  1594 ML{*functor Test (U: UNIVERSAL_TYPE): sig end =

  1595    struct

  1596       val (intIn: int -> U.t, intOut) = U.embed ()

  1597       val r: U.t ref = ref (intIn 13)

  1598       val s1 =

  1599          case intOut (!r) of

  1600             NONE => "NONE"

  1601           | SOME i => Int.toString i

  1602       val (realIn: real -> U.t, realOut) = U.embed ()

  1603       val () = r := realIn 13.0

  1604       val s2 =

  1605          case intOut (!r) of

  1606             NONE => "NONE"

  1607           | SOME i => Int.toString i

  1608       val s3 =

  1609          case realOut (!r) of

  1610             NONE => "NONE"

  1611           | SOME x => Real.toString x

  1612       val () = warning (concat [s1, " ", s2, " ", s3, "\n"])

  1613    end*}

  1614 

  1615 ML_val{*structure t = Test(U) *} 

  1616 

  1617 ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}

  1618