Re: recursive definition

[Damien.Doligez@inria.fr (Damien Doligez)]

(English version below)

>From: "QUERCIA Michel (T) Math" <querciam@l-carnot1.ac-dijon.fr>

>Il a ete explique dans un post precedent que "let rec x = f(x)"
>n'est compilable que si "x" est une fonction ou si la compilation
>de "f(x)" ne depend pas de "x".

En un mot, c'est une explication boguee.

Il est garanti que "let rec x = Expr" est compilable si "Expr" est
de la forme "fun z...y -> ..." ou "function y -> ...", et c'est tout.

L'implementation actuelle de Caml Light va un peu plus loin et accepte
de compiler si "Expr" est un constructeur de type concret (ou de
paire, de liste, de record, de tableau) ou une constante.

On accepte aussi un "let v = E1 in E2" a condition que E1 et E2
verifient aussi la condition, ca c'est alors equivalent a
"let rec x = E2 and v = E1".  Peut-etre qu'il y a d'autres cas que
j'ai oublies dans les coins.

Cette restriction nous est imposee par la technique de compilation du
"let rec", elle n'a rien a voir avec le systeme de types.  Le seul
rapport avec le typeur, c'est que c'est le typeur qui detecte les
erreurs a ce niveau.  On aurait pu le faire dans le parseur, et alors
le message d'erreur serait "Erreur de syntaxe".

Ca n'a rien a voir avec le typage, ce qui explique que le message
d'erreur parle de "genre" d'expression et non de "type".

Avec un peu de chance, il y a un moyen d'ecrire un "remember_rec" qui
integre un combinateur de point fixe dans "remember".

--------------

>I remember a post where it was explained that "let rec x = f(x)" is
>handled only when "x" is a function or when "f(x)" may be compiled
>with no knowledge of "x".

That post was wrong.

The only guarantee is that "let rec x = Expr" will be accepted if
"Expr" is an expression of the form "fun z...y -> ..." or
"function y -> ...".

The current implementation has an extension that will also accept it
if "Expr" is a constructor for a concrete type (or pair, list, record,
array), or a constant.

It also accepts "let v = E1 in E2" for "Expr", if E1 and E2 also have
the same form, because this is equivalent to "let rec x = E2 and v = E1".
There may be some other cases, I don't remember.

This restriction comes from the compilation technique used for "let
rec".  It has nothing to do with the type system.  The only connection
with types is that the type checker is used to detect problems in "let
rec".  We could have changed the grammar and let the parser handle
them, you would get a syntax error.

Again, this has nothing to do with typing, which explains that the
error message says "kind of expression" and not "type of expression".

There may be a way of writing a "remember_rec" to combine the
fix-point combinator with memoization.

-- Damien