> A possible approach for Caml would be to have a link-time analysis
> that detects cross-module value recursions that involve only function
> definitions, and allow these (because they are safe -- like in C!).
> Fabrice Le Fessant posted a patch to OCaml a while ago that does
> pretty much this.  I'm still hoping more general, principled solutions
> exist, but they sure are hard to design!


Isn't it feasible to annotate elements of signatures with something that
indicates that an identifier really is bound to a value, rather than a
module??  i.e.

foo.mli:

    value f : int -> int  (* must be bound to a lambda expression or an
identifier in foo.ml *)
    value x : int list (* must be bound to a cons-cell or an identifier
in foo.ml *)
    expr g : int -> int (* may be a computation *)

(The current "val" would be interpreted as "expr". "value" could also be
replaced by "const" or "val rec" or "rec" or whatever)  

I know this is revealing part of how foo.mli is implemented, but that is
really the point: allow the programmer to reveal more when necessary to
prove that things are safe.  I guess you'd have to generalize this to
functors, etc., (the subsumption relation between signatures would allow
"values" to be used as "expressions", but not vice-versa).   

Hasn't there been some work done one such "phase distinction" rules?
Was that by Harper et al.? 

However, this would not solve the problem:

    A.mli    val x : int                B.mli    val y : int
    A.ml     let x = B.y                B.ml     let y = A.x

Perhaps disallowing identifiers on the r.h.s. (as in "let rec") is the
right thing to do, even if a bit of pain when just rebinding function
values.

Cheers,
Don
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr