variables in 'let rec'

David Chemouil
 Max Skaller
 Xavier Leroy
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20000323 (12:46) 
From:  Max Skaller <maxs@i...> 
Subject:  Re: variables in 'let rec' 
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 righthand 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 nongeneric 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