let rec for non-function values

let rec for non-function values

[Joshua D. Guttman]

I don't understand when OCaml will allow me to define non-functional
values via let rec.  

Here's a puzzling example.  It arose in the course of implementing
some algorithms manipulating non-deterministic finite automata.

type 'a t = Node of bool *		(* Accepting state? *)
      ('a * 'a t) list *		(* Next states for different events *)
      'a t list 			(* Next states after tau (silent event) *)

Then the following is accepted by ocaml v. 3:

let star_sketch (Node(b, i_0, t_0))	= 
  let rec n = 
    let rec
	traverse_initial (e,n_1)	= e, traverse n_1
    and traverse			= function 
	Node (true,i,t)			->
	  Node (true, 
		List.map traverse_initial i,
		(n :: (List.map traverse t)))
      |	Node (false,i,t)		->
	  Node (false, 
		List.map traverse_initial i,
		List.map traverse t)
    in Node (b,
	     List.map traverse_initial i_0,
	     List.map traverse t_0)
  in n

#                                 val star_sketch : 'a t -> 'a t = <fun>

I know it's not a good definition of Kleene star, because it will loop
if the argument already has cycles.  But it's syntactically OK.

By contrast: 

let rec star_sketch_2 (Node(b, i_0, t_0))	= 
  let rec n = Node (b,
		    List.map traverse_initial i_0,
		    List.map traverse t_0)

  and traverse_initial (e,n_1)	= e, traverse n_1
  and traverse			= function 
      Node (true,i,t)			->
	Node (true, 
	      List.map traverse_initial i,
	      (n :: (List.map traverse t)))
    |	Node (false,i,t)		->
	Node (false, 
	      List.map traverse_initial i,
	      List.map traverse t)
  in n

is syntactically not OK:

Characters 59-133:
This kind of expression is not allowed as right-hand side of `let rec' 

And yet star_sketch_2 seems to be derived from star_sketch by a sound
transformation for unnesting let recs.

The manual is not terribly informative:  

    The current implementation also supports a certain
    class of recursive definitions of non-functional values, such as 
              let rec name_1 = 1 :: name_2 and name_2 = 2 :: name_1 in expr 
       which binds name_1 to the cyclic list  1::2::1::2::..., and name_2 to the
    cyclic list  2::1::2::1::... Informally, the class of accepted definitions
    consists of those definitions where the defined names occur only inside
    function bodies or as argument to a data constructor.

I ask this question because using let rec to define immutable cyclic
data is pretty attractive, but clearly one can't write a program in
that style if such small differences break things.  Many variants were
either accepted or rejected in patterns that I found inscrutable.  

Thanks --

        Joshua 


-- 
	Joshua D. Guttman		<guttman@mitre.org> 
	MITRE, Mail Stop A150 
	202 Burlington Rd.		Tel:	+1 781 271 2654
	Bedford, MA 01730-1420 USA	Fax:	+1 781 271 3816