[Caml-list] Strange behavior of mutualy recursive definitions

[Caml-list] Strange behavior of mutualy recursive definitions

[rixed]

I met this strangeness today and would like to know is it a FAQ? Is it
intentional? Is it fixable?

# let inc f x = (f x)+1 and dec f x = (f x)-1;;
val inc : ('a -> int) -> 'a -> int = <fun>
val dec : ('a -> int) -> 'a -> int = <fun>
# let rec toto = inc titi and titi = dec toto;;
Error: This kind of expression is not allowed as right-hand side of `let rec'

Now after reading http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#s:letrecvalues ,
this is unclear why toto and titi definitions are not 'statistically constructive':
It seams that one could trivially add a "fun f -> ... f" around the
function bodies in order to comply with the rules. And actually, this
even simpler (but to my knowledge equivalent) definition works :

# let rec toto x = inc titi x and titi x = dec toto x;;
val toto : 'a -> int = <fun>
val titi : 'a -> int = <fun>

So why was the first version rejected?

Re: [Caml-list] Strange behavior of mutualy recursive definitions

[Guillaume Yziquel]

Le Wednesday 27 Apr 2011 à 22:46:29 (+0200), rixed@happyleptic.org a écrit :
> I met this strangeness today and would like to know is it a FAQ? Is it
> intentional? Is it fixable?
> 
> # let inc f x = (f x)+1 and dec f x = (f x)-1;;
> val inc : ('a -> int) -> 'a -> int = <fun>
> val dec : ('a -> int) -> 'a -> int = <fun>
> # let rec toto = inc titi and titi = dec toto;;
> Error: This kind of expression is not allowed as right-hand side of `let rec'
> 
> Now after reading http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#s:letrecvalues ,
> this is unclear why toto and titi definitions are not 'statistically constructive':
> It seams that one could trivially add a "fun f -> ... f" around the
> function bodies in order to comply with the rules. And actually, this
> even simpler (but to my knowledge equivalent) definition works :
> 
> # let rec toto x = inc titi x and titi x = dec toto x;;
> val toto : 'a -> int = <fun>
> val titi : 'a -> int = <fun>
> 
> So why was the first version rejected?

Because to evaluate toto, you need to have titi evaluated beforehand
(wouldn't be the case if you had 'let rec toto = titi inc' instead of
'inc titi', typically). And to evaluate titi, you need to have evaluated
beforehand the value toto.

The second version only defines toto as a function that calls titi. No
need to have titi evaluated to be able to evalue toto. You only need to
know where it is declared. That's the main difference.

-- 
     Guillaume Yziquel

Re: [Caml-list] Strange behavior of mutualy recursive definitions

[rixed]

Thank you for the explanation but I fear they are not enough for me to
understand.  Specifically, I do not understand why to compile "let rec
toto = inc titi and titi = dec toto" this is not enough to know the
address of titi and toto functions. I don't see what's the difference
from let rec toto = titi inc ..." in this regard.

> The second version only defines toto as a function that calls titi. No
> need to have titi evaluated to be able to evalue toto. You only need to
> know where it is declared. That's the main difference.

But in the first version, toto is a function that calls inc with, as
first parameter, the address of titi. I don't see why it's more complex.

And suppose I would understand this, I'd still have to figure out why
merely adding the mute variable x suddenly turns the definitions valid.

Re: [Caml-list] Strange behavior of mutualy recursive definitions

[Guillaume Yziquel]

Le Wednesday 27 Apr 2011 à 23:28:52 (+0200), rixed@happyleptic.org a écrit :
> Thank you for the explanation but I fear they are not enough for me to
> understand.  Specifically, I do not understand why to compile "let rec
> toto = inc titi and titi = dec toto" this is not enough to know the
> address of titi and toto functions. I don't see what's the difference
> from let rec toto = titi inc ..." in this regard.

let rec toto = inc titi and titi = dec toto

This asks to evaluate both toto and titi.

Evaluating toto means feeding an evaluated titi to inc. So you need to
evaluate titi beforehand. Evaluating titi means feeding an evaluated
toto to dec. There's some kind of bootstrap here... that cannot be
solved.

let rec toto x = inc titi x and titi x = dec toto x

This asks to evaluate toto. Well, toto is a function that takes x and
does stuff with it... but this stuff is not done when you evaluate toto.
This stuff is only done when you apply some x value to toto.

This means that you do not need to have titi evaluated in order to be
able to evaluate toto. [rec] keyword: much the same behaviour as 'let
rec f x = f x'; no need to have f evaluated in order to evaluate f.

However, 'let rec f = f' will fail for the exact same reason as before:
To evaluate f, you need to have evaluated f beforehand.

Just focus on the difference between:

	let rec f x = f x
	let rec f = f

That's the only issue you have in your two code samples.

> > The second version only defines toto as a function that calls titi. No
> > need to have titi evaluated to be able to evalue toto. You only need to
> > know where it is declared. That's the main difference.
> 
> But in the first version, toto is a function that calls inc with, as
> first parameter, the address of titi. I don't see why it's more complex.

No. Not with the address of titi. With a pointer to closure block. and
this closure must be initialised / evaluated beforehand.

In your second case, you do not to have it evaluated beforehand, as it
only makes sense to have it initialised when the function call is made.
The 'rec' keyword allows to tie this knot.

The 'rec' keyword doesn't work in the first case. Just think at what 'let rec
f = f' should compile to...

> And suppose I would understand this, I'd still have to figure out why
> merely adding the mute variable x suddenly turns the definitions valid.

Because in 'let rec f = f', you need to have f evaluated with the code
you give to it: i.e. f. No way.

In 'let rec f x = f x', you're just defining a function that calls
itself repeatitively. It's a tad different.

'let rec f = f' isn't something that calls itself. You're defining it by
hand-waving, essentially saying "be what you are". Quite unhelpful for
the compiler. Why on earth should "be what you are" be interpreted as
"be a function that calls yourself". The former is very problematic. The
latter is very explicit.

-- 
     Guillaume Yziquel

Re: [Caml-list] Strange behavior of mutualy recursive definitions

[rixed]

-[ Wed, Apr 27, 2011 at 11:51:46PM +0200, Guillaume Yziquel ]----
> able to evaluate toto. [rec] keyword: much the same behaviour as
> 'let rec f x = f x'; no need to have f evaluated in order to evaluate f.
>
> However, 'let rec f = f' will fail for the exact same reason as before:
> To evaluate f, you need to have evaluated f beforehand.
>
> Just focus on the difference between:
> 
>       let rec f x = f x
>       let rec f = f

Very good idea let's focus on this example.
Why 'let rec f = f' is rejected is clear: you cannot type f.  In my
original example, however, the point was precisely that both toto and
titi types were known to be 'a -> int beforehand (because of the type of
inc and dec).

So, an equivalent and simpler question would be:

Although "let rec f = f" is unsound and rejected as expected,
why is "let rec f : unit -> unit = f" also rejected, since it seams
trivially equivalent to "let rec f () : unit = f ()" (which is
accepted) ?


Now that I think about it, another equivalent question would be:
Why is "let rec f = f" rejected with the error "This kind of expression
is not allowed" instead of being rejected by the type system ?
I'm under the impression that the mutual recursion rules stated in
manual section 7.3 are checked somewhat too early, and that the typer
could resolve some practical cases that are ruled out by mutual
recursion acceptability checks.

Either that, or there is something fundamentally simple in ocaml that I
still failed to grasp despite your patient explanations :-)

[Caml-list] Re: Strange behavior of mutualy recursive definitions

[Jeffrey Scofield]

rixed@happyleptic.org writes:

> Why 'let rec f = f' is rejected is clear: you cannot type f.

In my thinking, f is typeable with type 'a (fully general type).
I don't think it's untypeable, it just doesn't have a useful type.
It's similar to the type of failwith : string -> 'a, but without
the string.

In Haskell the equivalent definition has useful purposes.
It represents "bottom" (erroneous computation).  In a strict
language you can't have such a value hanging around, seems
like.  So in OCaml you have failwith instead (a lazy version of an
erroneous computation).

So to me it makes sense that it's rejected not on typing but on
other grounds.

It's also worth noting that

    let rec f x = f x

is just a shorthand for

    let rec f = fun x -> f x

This also is typeable with type 'a -> 'b.  Again this isn't a
very useful type, but there's no problem with this value in a strict
language, because the lambda ("fun") essentially makes it lazy.

Jeffrey

Re: [Caml-list] Strange behavior of mutualy recursive definitions

[Fabrice Le Fessant]

[-- Attachment #1: Type: text/plain, Size: 594 bytes --]

On 04/28/2011 06:06 AM, rixed@happyleptic.org wrote:
> Although "let rec f = f" is unsound and rejected as expected,
> why is "let rec f : unit -> unit = f" also rejected, since it seams
> trivially equivalent to "let rec f () : unit = f ()" (which is
> accepted) ?

Eta-conversion (transforming "let f = f into let f () = f ()") is
unsound in the general case. Indeed, take for example:

let f () = print_string "titi"; function () -> print_string "toto"

Is "let g = f ()" equivalent to "let g () = f () ()" ? No.

So, no eta-expansion is ever performed using only type information.

Fabrice

[-- Attachment #2: fabrice_le_fessant.vcf --]
[-- Type: text/x-vcard, Size: 380 bytes --]

begin:vcard
fn:Fabrice LE FESSANT
n:LE FESSANT;Fabrice
org:INRIA Saclay -- Ile-de-France;P2P & OCaml
adr;quoted-printable:;;Parc Orsay Universit=C3=A9 ;Orsay CEDEX;;91893;France
email;internet:fabrice.le_fessant@inria.fr
title;quoted-printable:Charg=C3=A9 de Recherche
tel;work:+33 1 74 85 42 14
tel;fax:+33 1 74 85 42 49 
url:http://fabrice.lefessant.net/
version:2.1
end:vcard

Re: [Caml-list] Re: Strange behavior of mutualy recursive definitions

[Guillaume Yziquel]

Le Thursday 28 Apr 2011 à 01:24:33 (-0500), Jeffrey Scofield a écrit :
> rixed@happyleptic.org writes:
> 
> > Why 'let rec f = f' is rejected is clear: you cannot type f.
> 
> In my thinking, f is typeable with type 'a (fully general type).
> I don't think it's untypeable, it just doesn't have a useful type.
> It's similar to the type of failwith : string -> 'a, but without
> the string.

Exactly.

-- 
     Guillaume Yziquel

Re: [Caml-list] Strange behavior of mutualy recursive definitions

[rixed]

-[ Thu, Apr 28, 2011 at 09:26:10AM +0200, Fabrice Le Fessant ]----
> On 04/28/2011 06:06 AM, rixed@happyleptic.org wrote:
> > Although "let rec f = f" is unsound and rejected as expected,
> > why is "let rec f : unit -> unit = f" also rejected, since it seams
> > trivially equivalent to "let rec f () : unit = f ()" (which is
> > accepted) ?
> 
> Eta-conversion (transforming "let f = f into let f () = f ()") is
> unsound in the general case. Indeed, take for example:
> 
> let f () = print_string "titi"; function () -> print_string "toto"
> 
> Is "let g = f ()" equivalent to "let g () = f () ()" ? No.
> 
> So, no eta-expansion is ever performed using only type information.

Oh, you are right! I really couldn't imagine a case where they were not
equivalent.

So I was wrong (and a little bit ridiculous) when I asserted that "let f
= g" is "trivially" (!! :-)) equivalent to "let f x = g x" when the
signature of g is known.

That's fine. The other shorter syntax was more appealing but I will be
more cautious with it from now on.

Re: [Caml-list] Re: Strange behavior of mutualy recursive definitions

[rixed]

-[ Thu, Apr 28, 2011 at 10:45:57AM +0200, Guillaume Yziquel ]----
> Le Thursday 28 Apr 2011 à 01:24:33 (-0500), Jeffrey Scofield a écrit :
> > rixed@happyleptic.org writes:
> > 
> > > Why 'let rec f = f' is rejected is clear: you cannot type f.
> > 
> > In my thinking, f is typeable with type 'a (fully general type).
> 
> Exactly.

Yep. My convictions are quickly collapsing. :-)