David Chemouil wrote:

> I'm currently writing a program where I need to create both variables
> and functions in a 'let rec'. The problem is that it is not allowed to
> define a simple variable (i.e not a variant) in a 'let rec', because it
> would be able to write things such as:
> 
> # let rec x = x+1;;
> This kind of expression is not allowed as right-hand side of `let rec'
> 
> This error message seems okay to me.
> 
> However, the error message also occurs in situations where there is no
> problem:

This difficulty is more general: it applies to types, functions,
modules and classes mixed together as well.

I can't comment on the general undecidability issues here.
However, mixing classes and types together appears to be
decidable.  Here's a demonstration: given a mixed
definition:

	let rec class A1' .. and class An '
  	and type t1 ... and type tm

we can mechanically split the definition to:

	(* generic classes *)
	let class ['t1, 't2, .. 'tn] A1' ... 
	and class ['t1, 't2, .. 'tn] A2' ..
	..
 	and class ['t1, 't2, .. 'tn] An' ..
	
	(* algebraic types  using generic classes
	 instantiated on themselves *)
	let t1 ..  [t1, t2, .. tn] A1' ....[.. ] A2' ..
	and t2 ..  [t2, t3, ... tn] A1' .. [.. ] A2' ...


	(* rename generic classes as non-generic ones *)
	class A1 = [t1, t2 .. tn] A1'
	class A2 = [ ... ] A2'


This transformation can be done mechanically, and produces
the desired result, so allowing mixed type/class definition
recursions is purely a matter of syntactic sugar (although
my 'demonstration' is certainly not a proof).

It seems clear to me that this kind of result must extend
to _constants_ as well, since classes and functions
are just constants. It isn't clear that it extends to
variables... that is, mutable record components...

Cases like:

  let rec x = x+1

must be decidable, by the above decision algorithm,
assuming the existing type system is (which it isn't, I'm told?)
Or at least, no worse than an existing problem.
That's because one can always replace a constant value with
a function:

	let rec x' () = (x' ()) + 1
	let x = x' ()

is perfectly legal now and equivalent. What hapens is
that you get an infinite loop calling x = x'(). The type system
has failed to detect this. So allowing

	let rec x = x + 1

is no worse, indeed, it may be better, because there is some
chance of improving the typing algorithm to detect some such
cases.

Alternatively, you can just use

	let rec x' () = ...
	and ...
	let x = x() 

in lieu of what you really wanted: (that is,
there is a workaround).

Unfortunately, I do _not_ know of a workaround
for modules. (ie a functor where the argument
depends on one of the types defined, and the
type depends on that module instance).

This case may be genuinely undecidable, precisely because
I can't think of a workaround.

-- 
John (Max) Skaller at OTT [Open Telecommications Ltd]
mailto:maxs@in.ot.com.au      -- at work
mailto:skaller@maxtal.com.au  -- at home