[MLton-user] Fixpoints

[Vesa Karvonen]

Quoting Stephen Weeks <sweeks@sweeks.com>:
> > I'm not sure I like the uncurrying of fix or the new specification
> > of iso, but those are largely stylistic issues.
> 
> Yep.  Those changes both follow two long-standing MLton conventions
> that have proved extremely useful:
> 
>   1. Only use currying if there is actual staging of computation going
>      on.

Ok, I'll bite. :)

I somewhat sympathize with that view (that currying should be reserved for
staging), but I value other aspects more.  Of course, unless we are talking
about a case where staging really is involved, then the difference is
mostly "cosmetic" as one can always convert between the two forms.  However,
I like curried definitions for a number of reasons.

First of all, I'm not at all convinced that such operational concerns as
staging should dictate the choice when there is none (no staging).  I'm
much more interested in the logical properties (types) of combinators than
their operational properties (terms).  Actually, for the most part, I don't
want to pay much attention to operational properties.

IMHO, currying often (significantly) simplifies the types of combinators
making them easier to understand.  For example, compare

  val fix : 'a t * 'a uop -> 'a   (* tupled *)

and

  val fix : 'a t -> 'a fix        (* curried *)

where
  type 'a uop = 'a -> 'a
  type 'a fix = ('a uop) -> 'a

Looking at the curried type, the idea of an injection from tiers to fixpoint
combinators comes immediately to (my) mind.  I find this useful, because when
I'm looking at a fixpoint framework, I'm interested in how one actually
produces a fixpoint combinator.

The type of the tupled version makes it clear that no computation is staged,
but that is hardly useful for understanding the fixpoint framework, IMHO.
If anything, it actually reveals an operational implementation detail that
might change (staging needed).  Also, if some client, for some reason, just
wants to provide a fixpoint combinator and not expose the use of the framework
to the users of the fixpoint combinator, the client has to explicitly curry
fix.

Curried functions are easier to combine (compose and parameterize) to
produce the desired function (in point-free style).  I find this valuable,
because I then don't have to litter the code with plumbing (deconstructing
and constructing tuples) and I find that it helps me to see the code at a
higher-level of abstraction.

> > >     datatype 'a u = U of ('a * ('a -> 'a))
> > >     type 'a t = 'a u thunk
> > 
> > The above definition of u has a problem.  Namely, a user can now
> > instantiate the tier thunk.
> 
> Good point, but the problem is not so much the definition of u, the
> problem is that I exposed too much in the interface.  One can tweak my
> interface so that it only exposes that "t" is an arrow type, and hence
> can be eta-expanded to circumvent the value restriction.

That's a good idea.

> Here is my proposal incorporating the above changes.  Note that the
> "t" type is all that is used in the specifications -- I think that is
> simpler that having a client need to understand both "t" and "t'".
> 
> signature FIX =
>    sig
>       type 'a t1
>       type 'a t2
>       type 'a t = 'a t1 -> 'a t2
> 
>       exception Fix
>       
>       val ^ : 'a t * 'b t -> ('a, 'b) product t
>       val fix: 'a t * ('a -> 'a) -> 'a
>       val iso: 'a t * ('a, 'b) emb -> 'b t
>       val tier: ('a * ('a -> unit)) thunk -> 'a t
>   end

Ok.  This looks very nice, except that I still don't like the tupled
version of fix (and the specification of iso).  Consider the following:

> val isEven & isOdd =
>    Fix.fix
>    (let open Fix Fn in T^T end,
>     fn isEven & isOdd =>
>        (fn 0w0 => true
>          | 0w1 => false
>          | n => isOdd (n-0w1)) &
>        (fn 0w0 => false
>          | 0w1 => true
>          | n => isEven (n-0w1)))
[...]
> val ones =
>     let open Fix Stream
>     in fix (T, fn ones => cons (1, ones))
>     end

Using the curried version of fix one writes:

val isEven & isOdd =
    let open Fix Fn in fix (T^T) end
      (fn isEven & isOdd =>
          (fn 0w0 => true
            | 0w1 => false
            | n => isOdd (n-0w1)) &
          (fn 0w0 => false
            | 0w1 => true
            | n => isEven (n-0w1)))

val ones =
    let open Fix Stream
    in fix T (fn ones => cons (1, ones))
    end

Client code using the curried version is slightly simpler.  Also,
as I said earlier, I find the type of the curried fix (in particular)
much more enlightening.

-Vesa Karvonen