Vous êtes sur la bonne voie. En fonction des exigences, j'essaierais de partir de ces équations :
compunere 1 f x == f x
Ce qui précède dit qu'en appliquant f
une fois pour x
est exactement la même chose que de faire (f x)
.
compunere 2 f x == f (f x)
De même, l'application f
deux fois devrait calculer f (f x)
. Si vous remplacez (f x)
par un appel à compunere
vous avez :
compunere 2 f x == f (f x) = f (compunere 1 f x)
Le modèle général de récurrence semble être :
compunere n f x == f (compunere (n - 1) f x)
Notez que le type le plus général de f
es a -> b
mais quand f
est appelé à nouveau avec une valeur de type b
ce qui signifie que a
y b
devraient être du même type, et donc f
est en réalité un endomorphisme, une fonction de type a -> a
. C'est le cas pour N >= 1, mais dans le cas dégénéré de N=0, vous pourriez avoir un comportement différent.
Appliquer f
temps zéro pour x
pourrait signifier "retourner x", ce qui signifie que compunere
podría retourne théoriquement une valeur de type a
pour zéro, pour tout f
être un a -> b
fonction, a
y b
peuvent être distincts ; vous pourriez distinguer les deux cas avec plus de code, mais ici nous pouvons simplement laisser le vérificateur de type appliquer la contrainte que a = b
dans tous les cas et ont un comportement uniforme. Vous pouvez également rendre 0 invalide (comme les nombres négatifs) en lançant une exception (les applications négatives pourraient théoriquement être des applications postitives de la fonction inverse, mais vous ne pouvez pas calculer cela lorsque vous ne savez rien de f ; f pourrait être non-invertible).
Votre code est un peu différent :
compunere 3 f x == (compunere 2 f (f x))
== (compunere 1 f (f (f x)))
== (compunere 0 f (f (f (f x))))
...
L'avantage de votre approche est que l'appel récursif à compunere
donne directement le résultat du calcul en cours : il est en position de queue, ce qui permet au compilateur d'effectuer l'élimination des appels de queue.
Lorsque vous atteignez N=0, la valeur liée localement x
donne le résultat souhaité. Ici, pour N=0 en entrée, la seule interprétation naturelle est aussi de retourner x
.