let rec pour les valeurs et let rec pour les fonctions en ocaml

Question

Quelle est la meilleure intuition pour expliquer pourquoi la première définition serait refusée, alors que la seconde serait acceptée ?

let rec a = b (* This kind of expression is not allowed as right-hand side of `let rec' *)
and b x = a x

let rec a x = b x (* oki doki *)
and b x = a x

Est-ce lié aux 2 approches de réduction : une règle pour chaque substitution de fonction (et un délimiteur Rec) VS une règle par définition de fonction (et levée de lambda) ?

Answer 1

Il est très difficile de vérifier que les définitions récursives sont valides.

Fondamentalement, vous voulez éviter les modèles dans ce type de forme :

let rec x = x

Dans le cas où chaque partie gauche des définitions est une déclaration de fonction, vous savez que tout va bien se passer. Au pire, vous créez une boucle infinie, mais au moins vous créez une valeur. Mais le x = x ne produit rien et n'a aucune valeur sémantique.

Dans votre cas, vous créez effectivement des fonctions (qui bouclent indéfiniment), mais il est en fait plus difficile de vérifier que c'est bien le cas. Pour éviter d'écrire un code qui tenterait une vérification exhaustive, les développeurs d'OCaml ont décidé d'opter pour un algorithme beaucoup plus simple.

Vous pouvez avoir une vision des règles aquí . En voici un extrait (souligné par moi) :

Elle sera acceptée si chacun des expr1 exprn est statiquement constructif par rapport à name1 namen , n'est pas immédiatement lié à l'un des éléments suivants name1 namen et n'est pas un constructeur de tableau dont les arguments sont de type abstrait.

Comme vous pouvez le constater, la liaison récursive directe de variables n'est pas autorisée.

Il ne s'agit cependant pas d'une règle définitive, car des améliorations sont apportées à cette partie du compilateur en attente de libération . Je n'ai pas testé si votre exemple passe avec, mais un jour votre code pourrait être accepté.