Sophie

Sophie

distrib > Fedora > 15 > i386 > by-pkgid > d07d7ab417d79053e7e0155c99e1a1c8 > files > 2240

mlton-20100608-3.fc15.i686.rpm

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
<meta name="robots" content="index,nofollow">



<title>Fixpoints - MLton Standard ML Compiler (SML Compiler)</title>
<link rel="stylesheet" type="text/css" charset="iso-8859-1" media="all" href="common.css">
<link rel="stylesheet" type="text/css" charset="iso-8859-1" media="screen" href="screen.css">
<link rel="stylesheet" type="text/css" charset="iso-8859-1" media="print" href="print.css">


<link rel="Start" href="Home">


</head>

<body lang="en" dir="ltr">

<script src="http://www.google-analytics.com/urchin.js" type="text/javascript">
</script>
<script type="text/javascript">
_uacct = "UA-833377-1";
urchinTracker();
</script>
<table bgcolor = lightblue cellspacing = 0 style = "border: 0px;" width = 100%>
  <tr>
    <td style = "
		border: 0px;
		color: darkblue; 
		font-size: 150%;
		text-align: left;">
      <a class = mltona href="Home">MLton MLTONWIKIVERSION</a>
    <td style = "
		border: 0px;
		font-size: 150%;
		text-align: center;
		width: 50%;">
      Fixpoints
    <td style = "
		border: 0px;
		text-align: right;">
      <table cellspacing = 0 style = "border: 0px">
        <tr style = "vertical-align: middle;">
      </table>
  <tr style = "background-color: white;">
    <td colspan = 3
	style = "
		border: 0px;
		font-size:70%;
		text-align: right;">
      <a href = "Home">Home</a>
      &nbsp;<a href = "TitleIndex">Index</a>
      &nbsp;
</table>
<div id="content" lang="en" dir="ltr">
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 (<a href = "http://mlton.org/cgi-bin/viewsvn.cgi/mltonlib/trunk/com/ssh/extended-basis/unstable/README?view=markup"><img src="moin-www.png" alt="[WWW]" height="11" width="11">README</a>). <p>
First the signature of the framework (<a href = "http://mlton.org/cgi-bin/viewsvn.cgi/mltonlib/trunk/com/ssh/extended-basis/unstable/public/generic/tie.sig?view=markup"><img src="moin-www.png" alt="[WWW]" height="11" width="11">tie.sig</a>): 
</p>
<p>
<pre class=code><I><FONT COLOR="#B22222">(**
 * 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 -&gt; t) -&gt; 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 -&gt; u) -&gt; 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.
 *)</FONT></I>
<B><FONT COLOR="#0000FF">signature</FONT></B> TIE = <B><FONT COLOR="#0000FF">sig</FONT></B>
   <B><FONT COLOR="#0000FF">include</FONT></B> ETAEXP'
   <B><FONT COLOR="#A020F0">type</FONT></B><B><FONT COLOR="#228B22"> 'a t </FONT></B>=<B><FONT COLOR="#228B22"> 'a etaexp
   <I><FONT COLOR="#B22222">(** The type of fixpoint witnesses. *)</FONT></I>

   </FONT></B><B><FONT COLOR="#A020F0">val</FONT></B> fix : 'a t -&gt; 'a Fix.t
   <I><FONT COLOR="#B22222">(**
    * Produces a fixpoint combinator from the given witness.  For example,
    * one can make a mutually recursive definition of functions:
    *
    *&gt; val isEven &amp; isOdd =
    *&gt;     let open Tie in fix (function *` function) end
    *&gt;        (fn isEven &amp; isOdd =&gt;
    *&gt;            (fn 0 =&gt; true
    *&gt;              | 1 =&gt; false
    *&gt;              | n =&gt; isOdd (n-1)) &amp;
    *&gt;            (fn 0 =&gt; false
    *&gt;              | 1 =&gt; true
    *&gt;              | n =&gt; isEven (n-1)))
    *)</FONT></I>

   <I><FONT COLOR="#B22222">(** == Making New Witnesses == *)</FONT></I>

   <B><FONT COLOR="#A020F0">val</FONT></B> pure : ('a * 'a UnOp.t) Thunk.t -&gt; 'a t
   <I><FONT COLOR="#B22222">(**
    * {pure} is a more general version of {tier}.  It is mostly useful for
    * computing fixpoints in a non-imperative manner.
    *)</FONT></I>

   <B><FONT COLOR="#A020F0">val</FONT></B> tier : ('a * 'a Effect.t) Thunk.t -&gt; 'a t
   <I><FONT COLOR="#B22222">(**
    * {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.
    *)</FONT></I>

   <B><FONT COLOR="#A020F0">val</FONT></B> id : 'a -&gt; 'a t
   <I><FONT COLOR="#B22222">(** {id x} is equivalent to {pure (const (x, id))}. *)</FONT></I>

   <I><FONT COLOR="#B22222">(** == Combining Existing Witnesses == *)</FONT></I>

   <B><FONT COLOR="#A020F0">val</FONT></B> iso : 'b t -&gt; ('a, 'b) Iso.t -&gt; 'a t
   <I><FONT COLOR="#B22222">(**
    * 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.
    *)</FONT></I>

   <B><FONT COLOR="#A020F0">val</FONT></B> product : 'a t * ('a -&gt; 'b t) -&gt; ('a, 'b) Product.t t
   <I><FONT COLOR="#B22222">(**
    * 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.
    *)</FONT></I>

   <B><FONT COLOR="#A020F0">val</FONT></B> *` : 'a t * 'b t -&gt; ('a, 'b) Product.t t
   <I><FONT COLOR="#B22222">(** {a *` b} is equivalent to {product (a, const b)}. *)</FONT></I>

   <B><FONT COLOR="#A020F0">val</FONT></B> tuple2 : 'a t * 'b t -&gt; ('a * 'b) t
   <I><FONT COLOR="#B22222">(**
    * Given witnesses for {'a} and {'b} produces a witness for the product
    * {'a * 'b}.
    *)</FONT></I>

   <I><FONT COLOR="#B22222">(** == Particular Witnesses == *)</FONT></I>

   <B><FONT COLOR="#A020F0">val</FONT></B> function : ('a -&gt; 'b) t
   <I><FONT COLOR="#B22222">(** Witness for functions. *)</FONT></I>
<B><FONT COLOR="#0000FF">end</FONT></B>
</PRE>
 
</p>
<p>
<tt>fix</tt> is a <a href="TypeIndexedValues">type-indexed</a> function.  The type-index parameter to <tt>fix</tt> is called a "witness".  To compute fixpoints over products, one uses the <tt>*`</tt> 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 <tt>pure</tt> combinator is a generalization of <tt>tier</tt>.  The <tt>iso</tt> combinator is provided for reusing existing witnesses. 
</p>
<p>
Note that instead of using an infix operator, we could alternatively employ an interface using <a href="Fold">Fold</a>.  Also, witnesses are eta-expanded to work around the <a href="ValueRestriction">value restriction</a>, while maintaining abstraction. 
</p>
<p>
Here is the implementation (<a href = "http://mlton.org/cgi-bin/viewsvn.cgi/mltonlib/trunk/com/ssh/extended-basis/unstable/detail/generic/tie.sml?view=markup"><img src="moin-www.png" alt="[WWW]" height="11" width="11">tie.sml</a>): 
</p>
<p>
<pre class=code><B><FONT COLOR="#0000FF">structure</FONT></B> Tie :&gt; TIE = <B><FONT COLOR="#0000FF">struct</FONT></B>
   <B><FONT COLOR="#0000FF">open</FONT></B> Product
   <B><FONT COLOR="#A020F0">infix</FONT></B> &amp;
   <B><FONT COLOR="#A020F0">type</FONT></B><B><FONT COLOR="#228B22"> 'a etaexp_dom </FONT></B>=<B><FONT COLOR="#228B22"> Unit.t
   </FONT></B><B><FONT COLOR="#A020F0">type</FONT></B><B><FONT COLOR="#228B22"> 'a etaexp_cod </FONT></B>=<B><FONT COLOR="#228B22"> ('a * 'a UnOp.t) Thunk.t
   </FONT></B><B><FONT COLOR="#A020F0">type</FONT></B><B><FONT COLOR="#228B22"> 'a etaexp </FONT></B>=<B><FONT COLOR="#228B22"> 'a etaexp_dom -&gt; 'a etaexp_cod
   </FONT></B><B><FONT COLOR="#A020F0">type</FONT></B><B><FONT COLOR="#228B22"> 'a t </FONT></B>=<B><FONT COLOR="#228B22"> 'a etaexp
   </FONT></B><B><FONT COLOR="#A020F0">fun</FONT></B> fix aT f = <B><FONT COLOR="#A020F0">let</FONT></B> <B><FONT COLOR="#A020F0">val</FONT></B> (a, ta) = aT () () <B><FONT COLOR="#A020F0">in</FONT></B> ta (f a) <B><FONT COLOR="#A020F0">end</FONT></B>
   <B><FONT COLOR="#A020F0">val</FONT></B> pure = Thunk.mk
   <B><FONT COLOR="#A020F0">fun</FONT></B> iso bT (iso <B><FONT COLOR="#A020F0">as</FONT></B> (_, b2a)) () () = <B><FONT COLOR="#A020F0">let</FONT></B>
      <B><FONT COLOR="#A020F0">val</FONT></B> (b, fB) = bT () ()
   <B><FONT COLOR="#A020F0">in</FONT></B>
      (b2a b, Fn.map iso fB)
   <B><FONT COLOR="#A020F0">end</FONT></B>
   <B><FONT COLOR="#A020F0">fun</FONT></B> product (aT, a2bT) () () = <B><FONT COLOR="#A020F0">let</FONT></B>
      <B><FONT COLOR="#A020F0">val</FONT></B> (a, fA) = aT () ()
      <B><FONT COLOR="#A020F0">val</FONT></B> (b, fB) = a2bT a () ()
   <B><FONT COLOR="#A020F0">in</FONT></B>
      (a &amp; b, Product.map (fA, fB))
   <B><FONT COLOR="#A020F0">end</FONT></B>
   <I><FONT COLOR="#B22222">(* The rest are not primitive operations. *)</FONT></I>
   <B><FONT COLOR="#A020F0">fun</FONT></B> <B><FONT COLOR="#A020F0">op</FONT></B> *` (aT, bT) = product (aT, Fn.const bT)
   <B><FONT COLOR="#A020F0">fun</FONT></B> tuple2 ab = iso (<B><FONT COLOR="#A020F0">op</FONT></B> *` ab) Product.isoTuple2
   <B><FONT COLOR="#A020F0">fun</FONT></B> tier th = pure ((<B><FONT COLOR="#A020F0">fn</FONT></B> (a, ua) =&gt; (a, Fn.const a o ua)) o th)
   <B><FONT COLOR="#A020F0">fun</FONT></B> id x = pure (Fn.const (x, Fn.id))
   <B><FONT COLOR="#A020F0">fun</FONT></B> function ? =
       pure (<B><FONT COLOR="#A020F0">fn</FONT></B> () =&gt; <B><FONT COLOR="#A020F0">let</FONT></B>
                   <B><FONT COLOR="#A020F0">val</FONT></B> r = ref (Basic.raising Fix.Fix)
                <B><FONT COLOR="#A020F0">in</FONT></B>
                   (<B><FONT COLOR="#A020F0">fn</FONT></B> x =&gt; !r x, <B><FONT COLOR="#A020F0">fn</FONT></B> f =&gt; (r := f ; f))
                <B><FONT COLOR="#A020F0">end</FONT></B>) ?
<B><FONT COLOR="#0000FF">end</FONT></B>
</PRE>
 
</p>
<p>
Let's then take a look at a couple of additional examples. 
</p>
<p>
Here is a naive implementation of lazy promises: 
</p>

<pre class=code>
<B><FONT COLOR="#0000FF">structure</FONT></B> Promise :&gt; <B><FONT COLOR="#0000FF">sig</FONT></B>
   <B><FONT COLOR="#A020F0">type</FONT></B><B><FONT COLOR="#228B22"> 'a t
   </FONT></B><B><FONT COLOR="#A020F0">val</FONT></B> lazy : 'a Thunk.t -&gt; 'a t
   <B><FONT COLOR="#A020F0">val</FONT></B> force : 'a t -&gt; 'a
   <B><FONT COLOR="#A020F0">val</FONT></B> Y : 'a t Tie.t
<B><FONT COLOR="#0000FF">end</FONT></B> = <B><FONT COLOR="#0000FF">struct</FONT></B>
   <B><FONT COLOR="#A020F0">datatype</FONT></B><B><FONT COLOR="#228B22"> 'a t' </FONT></B>=<B><FONT COLOR="#228B22">
      <FONT COLOR="#B8860B">EXN</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> exn
    </FONT></B>|<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">THUNK</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> 'a Thunk.t
    </FONT></B>|<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">VALUE</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> 'a
   </FONT></B><B><FONT COLOR="#A020F0">type</FONT></B><B><FONT COLOR="#228B22"> 'a t </FONT></B>=<B><FONT COLOR="#228B22"> 'a t' Ref.t
   </FONT></B><B><FONT COLOR="#A020F0">fun</FONT></B> lazy f = ref (THUNK f)
   <B><FONT COLOR="#A020F0">fun</FONT></B> force t =
      <B><FONT COLOR="#A020F0">case</FONT></B> !t
       <B><FONT COLOR="#A020F0">of</FONT></B> EXN e   =&gt; <B><FONT COLOR="#A020F0">raise</FONT></B> e
        | THUNK f =&gt; (t := VALUE (f ()) <B><FONT COLOR="#A020F0">handle</FONT></B> e =&gt; t := EXN e ; force t)
        | VALUE v =&gt; v
   <B><FONT COLOR="#A020F0">fun</FONT></B> Y ? = Tie.tier (<B><FONT COLOR="#A020F0">fn</FONT></B> () =&gt; <B><FONT COLOR="#A020F0">let</FONT></B>
                             <B><FONT COLOR="#A020F0">val</FONT></B> r = lazy (raising Fix.Fix)
                          <B><FONT COLOR="#A020F0">in</FONT></B>
                             (r, r &lt;\ <B><FONT COLOR="#A020F0">op</FONT></B> := o !)
                          <B><FONT COLOR="#A020F0">end</FONT></B>) ?
<B><FONT COLOR="#0000FF">end</FONT></B>
</PRE>
<p>
 
</p>
<p>
An example use of our naive lazy promises is to implement equally naive lazy streams: 
</p>

<pre class=code>
<B><FONT COLOR="#0000FF">structure</FONT></B> Stream :&gt; <B><FONT COLOR="#0000FF">sig</FONT></B>
   <B><FONT COLOR="#A020F0">type</FONT></B><B><FONT COLOR="#228B22"> 'a t
   </FONT></B><B><FONT COLOR="#A020F0">val</FONT></B> cons : 'a * 'a t -&gt; 'a t
   <B><FONT COLOR="#A020F0">val</FONT></B> get : 'a t -&gt; ('a * 'a t) Option.t
   <B><FONT COLOR="#A020F0">val</FONT></B> Y : 'a t Tie.t
<B><FONT COLOR="#0000FF">end</FONT></B> = <B><FONT COLOR="#0000FF">struct</FONT></B>
   <B><FONT COLOR="#A020F0">datatype</FONT></B><B><FONT COLOR="#228B22"> 'a t </FONT></B>=<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">IN</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> ('a * 'a t) Option.t Promise.t
   </FONT></B><B><FONT COLOR="#A020F0">fun</FONT></B> cons (x, xs) = IN (Promise.lazy (<B><FONT COLOR="#A020F0">fn</FONT></B> () =&gt; SOME (x, xs)))
   <B><FONT COLOR="#A020F0">fun</FONT></B> get (IN p) = Promise.force p
   <B><FONT COLOR="#A020F0">fun</FONT></B> Y ? = Tie.iso Promise.Y (<B><FONT COLOR="#A020F0">fn</FONT></B> IN p =&gt; p, IN) ?
<B><FONT COLOR="#0000FF">end</FONT></B>
</PRE>
<p>
 
</p>
<p>
Note that above we make use of the <tt>iso</tt> combinator.  Here is a finite representation of an infinite stream of ones: 
</p>

<pre class=code>
<B><FONT COLOR="#A020F0">val</FONT></B> ones = <B><FONT COLOR="#A020F0">let</FONT></B>
   <B><FONT COLOR="#0000FF">open</FONT></B> Tie Stream
<B><FONT COLOR="#A020F0">in</FONT></B>
   fix Y (<B><FONT COLOR="#A020F0">fn</FONT></B> ones =&gt; cons (<B><FONT COLOR="#5F9EA0">1</FONT></B>, ones))
<B><FONT COLOR="#A020F0">end</FONT></B>
</PRE>
<p>
 
</p>
</div>



<p>
<hr>
Last edited on 2007-08-25 21:26:24 by <span title="cs27019070.pp.htv.fi"><a href="VesaKarvonen">VesaKarvonen</a></span>.
</body></html>

Perl :: Catalyst :: PostgreSQL :: RPM Valid HTML 4.01 Transitional