Re: Question point fixe

Xavier Leroy (Xavier.Leroy@inria.fr)
Wed, 19 Oct 1994 09:59:48 +0100 (MET)

From: Xavier Leroy <Xavier.Leroy@inria.fr>
Message-Id: <9410190859.AA23880@pauillac.inria.fr>
Subject: Re: Question point fixe
To: Damien.Doligez@inria.fr (Damien Doligez)
Date: Wed, 19 Oct 1994 09:59:48 +0100 (MET)
In-Reply-To: <9410181917.AA27432@couchey.inria.fr> from "Damien Doligez" at Oct 18, 94 08:17:17 pm

> > Why is it impossible to write:
> > let rec monf = build monf;;
>
> Because the compiler does not want to know anything about "build"
> (except its type) when it compiles "monf". Thus it doesn't know
> whether "build" will use its argument or not. If "build" does use its
> argument, there is no way to make this work. This is the same as
> writing:
> let rec x = succ x;;

Not quite, because "monf" is a function while "x" above is an integer.

For a function, the compiler could initialize "monf" with
(fun _ -> raise Bottom), then evaluate "build monf" (raising "Bottom"
if "build" applies "monf"), then update the initial value as usual.

I'm not saying the compiler should do that: it's painful to implement
and it breaks a nice property of the current compilation for "let
rec", which is that if a "let rec" definition is accepted, then it
always succeeds at run-time in finding the fixpoint.

I would suggest that Vincent Poirriez either tolerates the efficiency
loss implied by "let rec monf x = build monf x", or uses a reference
to compute the fixpoint himself.

- Xavier Leroy