4
votes

Liaisons Haskell `let` dans le calcul lambda

Je veux comprendre comment laissez les liaisons fonctionnent dans Haskell (ou peut-être le calcul lambda, si l'implémentation Haskell diffère?)

Je comprends en lisant Écrivez-vous un Haskell que cela est valide pour une seule liaison let .

(\square -> square 5) ((\times x -> times x x) (\x -> x * x))

Cela a du sens pour moi, car cela est cohérent avec le fonctionnement des liaisons dans le calcul lambda. Là où je suis confus, c'est en utilisant plusieurs liaisons let , où une liaison peut référencer les liaisons ci-dessus. Je vais donner un exemple trivial.

Code d'origine:

(\square times -> square 5) (\x -> times x x) (\x -> x * x)

Ma conjecture sur l'implémentation:

let times x y = x * y
    square x = times x x
in square 5

Cela ne semble pas fonctionner car times n'est pas défini lorsque square est appelé par le lambda. Cependant, cela peut être résolu par cette implémentation:

let x = y in e == (\x -> e) y

Est-ce la bonne façon d'implémenter cette liaison, au moins dans le calcul lambda?

recursion haskell let lambda-calculus letrec

5 commentaires

vous devez probablement définir let times x y = x * y ... sinon cela n'a pas beaucoup de sens.

@karakfa Merci! Petite erreur mentale de ma part. J'ai pris de l'avance moi-même! Je vais éditer. :)

Le let de Haskell n'est pas let , c'est letrec .

@WillNess Si let est en fait letrec , cela signifie-t-il que fix est appliqué à toutes les liaisons, ou uniquement celles récursives?

chaque et toujours. du moins en théorie; un compilateur peut réaliser qu'il n'y a pas de récursivité et optimiser. et nous n'avons pas à utiliser de correctif. la récursivité peut être mise en œuvre directement par l'implémentation, sous le capot.

3 Réponses :

5
votes

L'exemple times / square peut être exprimé en termes de fonctions lambda en utilisant la portée:

(\ones -> take 5 ones)((\f -> (\x -> f (x x))(\x -> f (x x)))(\ones -> 1 : ones))

(\evenodd -> evenodd (\x y -> x) 7)((\f -> (\x -> f (x x))(\x -> f (x x)))(\evenodd c -> c (\n -> n == 0 || evenodd (\x y -> y) (abs n - 1)) (\n -> n /= 0 && evenodd (\x y -> x) (abs n - 1))))

Mais la portée ne suffit pas pour les liaisons let récursives ou mutuellement récursives comme

(\f -> (\x -> f (x x))(\x -> f (x x)))

Dans le calcul lambda, vous pouvez définir le y-combinator pour la récursivité en tant que

let ones = 1 : ones in take 5 ones

let even n = n == 0 || odd (abs n - 1)
    odd n  = n /= 0 && even (abs n - 1)
in even 7

Cela vous permet de définir des fonctions et des valeurs en fonction d'elles-mêmes. Cette formulation n'est pas légale en raison de contraintes de frappe mais il existe des moyens de contourner cela . p>

L'utilisation du combinateur y nous permet d'exprimer les liaisons let ci-dessus en utilisant le calcul lambda:

(\times -> (\square -> square 5)(\x -> times x x))(\x y -> x * y)

3 commentaires

Je vous remercie! J'étais déjà conscient de l'utilisation de fix avec le lambda supplémentaire pour faire de la récursivité, mais je n'avais pas vu de liaisons mutuellement récursives, alors merci! C'est vraiment cool. Avec votre exemple de portée, je vois que c'est comme mon implémentation échouée, mais avec des crochets supplémentaires. Si je comprends actuellement, l.c. est juste associative, et donc ces deux expressions devraient évaluer la même chose, oui? Votre exemple fonctionne dans GHCi. C'est toujours cool de voir que tant de choses peuvent être faites avec juste le calcul lambda typé.

Oh, je vois la différence. J'ai fait \ square times -> au lieu de \ times -> (\ square . Cela a plus de sens. Je ne comprends toujours pas vraiment pourquoi les crochets sont nécessaires. Peut-être vous pourriez clarifier?

Tout ce dont vous avez besoin est U : Y = U. (. U) . :) (enfin, B aussi).

3
votes

Notez que plusieurs liaisons let peuvent être réduites à une seule, définissant une paire (tuple, dans le cas général). Par exemple. nous pouvons réécrire

(\pair -> snd pair 5) (fix (\pair -> (\x y -> x * y, \x -> fst pair x x)))

comme

let pair = (\x y -> x * y, \x -> fst pair x x)
in snd pair 5

puis

let (times, square) = (\x y -> x * y, \x -> times x x)
in square 5

puis, si on le souhaite ,

let times = \x y -> x * y
    square = \x -> times x x
in square 5

Après cela, nous pouvons appliquer la traduction habituelle du calcul lambda. Si la définition de paire finit par être récursive, comme dans le cas ci-dessus, nous avons besoin d'un combinateur à virgule fixe.

let times x y = x * y
    square x = times x x
in square 5

Notez que cette traduction ne joue pas avec les algorithmes d'inférence de type, qui gèrent let d'une manière spéciale, introduisant le polymorphisme. Ce n’est pas important si nous ne nous soucions que des aspects dynamiques de notre programme.

0 commentaires

2
votes

Je vais répondre à ma propre question pour peut-être fournir une perspective utile à ceux qui la consultent.

Nous voulons implémenter le programme suivant avec deux liaisons let:

(\times -> (\square  -> square 5) (\x -> times x x)) (\a b -> a * b) =>
(\square -> square 5) (\x -> (\a b -> a * b) x x)                    =>
(\square -> square 5) (\x -> (\b -> x * b) x)                        => 
(\square -> square 5) (\x -> x * x)                                  => 
(\x -> x * x) 5                                                      =>
5 * 5                                                                => 
25

Pour commencer, simplifions ceci à l'essence de ce que nous voulons:

(\times -> (\square -> square 5) (\x -> times x x)) (\a b -> a * b)

Assez simple. Cependant, square dans ce cas n'est pas défini! Eh bien, nous pouvons le lier en utilisant le mécanisme que notre langage nous fournit - un lambda. Cela nous donne (\ square -> square 5) (\ x -> times x x) . Maintenant square est défini, mais son cousin times ne l'est pas ... Eh bien, nous avons besoin d'un autre lambda! Notre programme final devrait ressembler à ceci:

square 5

Notez que le (\ times -> ...) englobe complètement notre dernière étape, de sorte que fois sera dans la portée car il est lié. Ceci est cohérent avec la réponse donnée par @rampion, et se réduit comme suit:

let times a b = a * b
    square x = times x x
in square 5

Si la fonction square n’avait pas dépendu de fois , on aurait pu facilement écrire (\ times square -> .... . La dépendance signifie qu'il faut imbriquer ces deux environnements, l'un contenant heures , et un autre à l'intérieur de ce qui peut utiliser sa définition.

Merci pour toute votre aide! Je suis époustouflé par la simplicité et la puissance du calcul lambda.

0 commentaires