Why rec only works with function values in SML/NJ?
Mark-Jason Dominus
I have a type `Stream' of lazy streams:
datatype 'a Stream =
Empty
| Cons of 'a * ( unit -> 'a Stream )
;
A stream has a head element, and a tail, which is a promise to compute
more elements if (and only if) necessary. A promise has type (unit ->
'a Stream). We collect on a promise by calling `force', which accepts a
promise and yields the promised stream.
fun force v = (v()) : 'a Stream;
So for example:
fun Hd (Cons(a,_)) = a; (* val Hd = fn : 'a Stream -> 'a *)
fun Tl (Cons(_,d)) = force d; (* val Tl = fn : 'a Stream -> 'a Stream *)
Here's a function that scales a stream of ints by a constant value:
fun scale (c:int) Empty = Empty
| scale c (Cons(h,p)) = Cons(c*h, fn () => scale c (force p))
(* val scale = fn : int -> int Stream -> int Stream *)
Let's make pow2, a stream of powers of 2. I want to say that its
first element is 1, and the rest of the stream is just pow2 itself
scaled by 2.
The first cut is
val pow2 = Cons(1, fn()=> scale 2 pow2);
This doesn't work, because pow2 isn't bound in the top-level
environment until after the definition is finished, and we want to use
it before that:
Error: unbound variable or constructor: pow2
One normally has the same problem defining recursive functions,
because the recursive function isn't bound at the time it's defined, and
so for example:
val factorial = fn 0 => 1 | n => n*(factorial (n-1));
fails:
Error: unbound variable or constructor: factorial
ML has a simple way around this: The keyword `rec' means to include
the new `factorial' in the environment before constructing the
definition, so that the `factorial' in the definition refers to the
object being defined.
val rec factorial = fn 0 => 1 | n => n*(factorial (n-1));
works as expected, and in fact the normal syntax
fun factorial 0 = | factorial n => n*(factorial (n-1));
is just sugar for this.
So I'd like to use this feature to define pow2:
val rec pow2 = Cons(1, fn()=> scale 2 pow2);
Error: syntax error found at ID
SML/NJ is finding fault with `Cons', apparently because it was
hoping to see `fn'.
I can fudge around it this way:
local
val rec pow2_promise =
fn () => Cons(1, fn()=>(scale 2 (force pow2_promise)))
in
val pow2 = force pow2_promise
end
This works fine. It is identical to the other definition, except I get
SML/NJ to swallow the `rec', by the legerdemain of embedding it in a
bogus definition which happens to declare and object of function type.
Why can't I use `rec' unless my variable is going to have function type?
Design flaw or feature?
--
--
If you never did, / you should. / These things are fun / and fun is good.
Mark-Jason Dominus m...@central.cis.upenn.edu
Xavier Leroy
> Why can't I use `rec' unless my variable is going to have function type?
Standard ML is even more restrictive than that: in a "val rec"
declaration, not only the variable must have a functional type, but
the right-hand side must be a function expression (fn pat => expr).
So,
fun K x y = x;
val rec f = K (fn x => x+1) f;
is rejected even though f has type int->int.
> Design flaw or feature?
The short answer is: SML's restrictions on recursive definitions are
indeed very strong and could be relaxed, but some restrictions must be
imposed anyway, because SML has call-by-value semantics.
Arbitrary recursive definitions cause no difficulties in a lazy
language, because it's always possible to unwind the definition on
demand and either reach the fixpoint if it exists or diverge
otherwise. This is not so in a call-by-value language: the evaluation
of the "val rec" definition must build a value that satisfies the
fixpoint equation, which is in general impossible. Consider for
instance
val rec X = some integer polynomial P in X
Evaluating this definition amounts to Hilbert's tenth problem (find an
integer root for an arbitrary integer polynomial, P-X).
Now, it is true that the class of recursive definitions that can
easily be handled in a call-by-value language is larger than just
function definitions. For instance, the Caml Light compiler handles
all recursive definitions "val rec x = E" where E contains only
constants, variables, constructor applications and function
definitions.
For this class of expressions, the actual value of x is not needed to
evaluate E: a pointer to x suffices. Evaluation proceeds by binding x
to a dummy object, then evaluating E, then overwriting x with the
value of E. (A formal proof of why this works involves infinite
terms, a metric on the value space, and Banach's fixed-point theorem;
we'll stick with the intuitive description if you don't mind.)
For instance,
val rec x = 1::2::x
is accepted and binds x to the cyclic list 1::2::1::2::..., which is
the solution of this equation: x is bound to a dummy cons cell, then
1::2::x is evaluated, and the car of x is overwritten with 1 and the
cdr with 2::x, which "loops" the list as expected.
Your definition
val rec pow2 = Cons(1, fn()=> scale 2 pow2);
also works as expected. But notice that if you had defined "scale"
with an extra () parameter:
fun scale (c:int) Empty = fn () => Empty
| scale c (Cons(h,p)) = fn () => Cons(c*h, scale c (force p))
then the definition
val rec pow2 = Cons(1, scale 2 pow2)
would be rejected, since there are no guarantees that the application
(scale 2 pow2) does not actually need to inspect the value of pow2.
This extension of "val rec" definitions beyond functions has proved
very useful when programming with streams or doubly-linked data
structures, among others, and is fairly easy to implement.
However, it brings considerable complexity to the formal semantics of
the language, which is probably why it was left out of Standard ML.
(The Definition of Standard ML is painful enough to read as it is.)
- Xavier Leroy
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Caml Light - "Taste ML in a whole new light" - caml...@margaux.inria.fr %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%