variables in 'let rec'

variables in 'let rec'

[David Chemouil]

hi


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:

# let rec x = fact 5    (* using usual fact *)
              ^^^^^^
  and even = function
  | 0 -> true
  | n -> odd (n-1)
  and odd = function
  | 1 -> true
  | n -> even (n-1);;
This kind of expression is not allowed as right-hand side of `let rec'

What is "funny" is that it is possible to write 'Some (fact 5)'...

I wonder, then, if it would be possible to be a little less strict in
the typing policy. I believe however that it must be hard to perform
this, because it believe it is undecidable in the general case. But
isn't it possible to find a less strict policy which remains decidable?
For example, what if, in the typer, the 'let rec ... and ...' definition
was split in two parts: 
- the first part would be typed first: it would contain the variable
definitions which would be typed as a normal 'let ... and ...'.
- the second part would be typed as the current 'let rec ... and ...',
but the environment would contain the variables typed in the first part.

This system would enable to create variables in a 'let rec', but would
still forbid :
- to define mutually recursive variables
- to define non-recursive functions within a 'let rec'.


Of course, I guess the problem must be harder than that, but I think the
current system isn't completely "natural", as it forbids something that
is mathematically correct... 

Anyway, if this problem is really to complex, or undecidable, or not
worth the effot, why not allow any variable definition in a 'let rec'
and print a warning message? Then, the programmer would decide if the
definition may lead to an error...


regards

dc

-- 
David Chemouil [mailto:chemouil@enseeiht.fr] [mobile: 06 84 16 26 65]

Laboratoire d'informatique et de mathématiques appliquées (IRIT-INPT)

Re: variables in 'let rec'

[Max Skaller]

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

Re: variables in 'let rec'

[Xavier Leroy]

> 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:
> 
> # let rec x = fact 5    (* using usual fact *)
>               ^^^^^^
>   and even = function
>   | 0 -> true
>   | n -> odd (n-1)
>   and odd = function
>   | 1 -> true
>   | n -> even (n-1);;
> This kind of expression is not allowed as right-hand side of `let rec'
> 
> What is "funny" is that it is possible to write 'Some (fact 5)'...

You're correct that the example above could be accepted because "x"
could be computed in advance (fact 5 doesn't depend on the variables of
the recursive equations).  However, this would complicate both the
well-formedness test and the compilation scheme for "let rec".  We
chose to err on the conservative side here.  Notice that your example
can (and should, in the interest of clarity) be written
        let x = fact 5
        let rec even = ... and odd = ...

> Anyway, if this problem is really to complex, or undecidable, or not
> worth the effot, why not allow any variable definition in a 'let rec'
> and print a warning message? Then, the programmer would decide if the
> definition may lead to an error...

We would have no guarantees that the generated code for the "let rec"
is correct, e.g. with the current compilation scheme it could crash
the program.  Better be restrictive here!

- Xavier Leroy

Re: variables in 'let rec'

[John Max Skaller]

Sven LUTHER wrote:
> 
> On Tue, Mar 28, 2000 at 11:03:36AM +1000, Max Skaller wrote:
> > Damien Doligez wrote:
> > >
> > > >From: Max Skaller <maxs@in.ot.com.au>
> > > >
> > > >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).
> > >
> > > But that doesn't work for "let rec x = 1 :: x", which is the most
> > > interesting feature of O'Caml's recursive value definitions.
> >
> >       It doesn't?
> >
> >       let rec x'() = 1 :: x()'
> >       let x = x'()
> 
> FYI :
> 
> bash-2.03$ ocaml
>         Objective Caml version 2.99 (99/12/08)
> 
> # let rec x = 1 :: x ;;
> val x : int list =
>   [1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
>    ...]

Ah! I withdraw my last comment: the list is constructed as instructed,
resulting in a circular list. The printer routines recognizes this,
or at least is smart enough to apply a printing limit. 

_Traversing_ the list may take infinite time, but examining 
the first n elements will not. (And the construction is 
constant time :-)

-- 
John (Max) Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
checkout Vyper http://Vyper.sourceforge.net
download Interscript http://Interscript.sourceforge.net

Re: variables in 'let rec'

[John Max Skaller]

Damien Doligez wrote:
> 
> >From: Max Skaller <maxs@in.ot.com.au>
> 
> >        let rec x'() = 1 :: x()'
> >        let x = x'()
> >
> >Seems to work fine. Of course, this will loop forever in an eager
> >language: the result is an infinite list of 1s.
> 
> Looping forever is not quite the same as returning an infinite list
> of 1s, which is what the current implementation does for
>     let rec x = 1::x

I don't understand: to construct an infinite list of 1's would seem to
me to take infinite time in an eager language. So it comes to the same
thing, doesn't it?

-- 
John (Max) Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
checkout Vyper http://Vyper.sourceforge.net
download Interscript http://Interscript.sourceforge.net

Re: variables in 'let rec'

[Sven LUTHER]

On Tue, Mar 28, 2000 at 11:03:36AM +1000, Max Skaller wrote:
> Damien Doligez wrote:
> > 
> > >From: Max Skaller <maxs@in.ot.com.au>
> > >
> > >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).
> > 
> > But that doesn't work for "let rec x = 1 :: x", which is the most
> > interesting feature of O'Caml's recursive value definitions.
> 
> 	It doesn't?
> 
> 	let rec x'() = 1 :: x()'
> 	let x = x'()

FYI :

bash-2.03$ ocaml  
        Objective Caml version 2.99 (99/12/08)

# let rec x = 1 :: x ;;
val x : int list =
  [1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1; 1;
   ...]
# let rec x = 1 :: 2 :: x ;;
val x : int list =
  [1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1;
   2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2;
   1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1;
   2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2;
   1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1;
   2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2;
   1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1;
   2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2;
   1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1;
   2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2;
   1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1;
   2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1; 2; 1;
   ...]

Friendly,

Sven LUTHER

Re: variables in 'let rec'

[Damien Doligez]

>From: Max Skaller <maxs@in.ot.com.au>

>        let rec x'() = 1 :: x()'
>        let x = x'()
>
>Seems to work fine. Of course, this will loop forever in an eager
>language: the result is an infinite list of 1s.

Looping forever is not quite the same as returning an infinite list
of 1s, which is what the current implementation does for
    let rec x = 1::x

-- Damien

Re: variables in 'let rec'

[Max Skaller]

Damien Doligez wrote:
> 
> >From: Max Skaller <maxs@in.ot.com.au>
> >
> >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).
> 
> But that doesn't work for "let rec x = 1 :: x", which is the most
> interesting feature of O'Caml's recursive value definitions.

	It doesn't?

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

Seems to work fine. Of course, this will loop forever in an eager
language: the result is an infinite list of 1s.

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

Re: variables in 'let rec'

[Damien Doligez]

>From: Max Skaller <maxs@in.ot.com.au>
>
>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).

But that doesn't work for "let rec x = 1 :: x", which is the most
interesting feature of O'Caml's recursive value definitions.

-- Damien