Re: variables in 'let rec'

From: Max Skaller (maxs@in.ot.com.au)
Date: Thu Mar 23 2000 - 02:37:20 MET

  • Next message: Max Skaller: "Re: Unsigned integers?"

    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
    



    This archive was generated by hypermail 2b29 : Thu Mar 23 2000 - 13:50:44 MET