Y Combinator en Haskell

Question

Est-il possible d'écrire le Y Combinator en Haskell ?

Il semble qu'il aurait un type infiniment récursif.

 Y :: f -> b -> c
 where f :: (f -> b -> c)

ou quelque chose comme ça. Même une simple factorielle légèrement factorisée

factMaker _ 0 = 1
factMaker fn n = n * ((fn fn) (n -1)

{- to be called as
(factMaker factMaker) 5
-}

échoue avec "Occurs check : cannot construct the infinite type : t = t -> t2 -> t1" (vérification de l'existence d'un type infini)

(Le Y combinator ressemble à ceci

(define Y
    (lambda (X)
      ((lambda (procedure)
         (X (lambda (arg) ((procedure procedure) arg))))
       (lambda (procedure)
         (X (lambda (arg) ((procedure procedure) arg)))))))

dans le schéma) Ou, plus succinctement, comme

(λ (f) ((λ (x) (f (λ (a) ((x x) a))))
        (λ (x) (f (λ (a) ((x x) a))))))

Pour l'ordre applicatif Et

(λ (f) ((λ (x) (f (x x)))
        (λ (x) (f (x x)))))

Ce qui est juste une contraction de eta pour la version paresseuse.

Si vous préférez des noms de variables courts.

Answer 1

Voici une définition non-récursive du y-combinateur en haskell :

newtype Mu a = Mu (Mu a -> a)
y f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)

Conseil d'administration

Answer 2

Le Y combinator ne peut pas être typé à l'aide des types de Hindley-Milner, le lambda calculus polymorphe sur lequel le système de types de Haskell est basé. Vous pouvez le prouver en faisant appel aux règles du système de types.

Je ne sais pas s'il est possible de typer le combinateur Y en lui donnant un type de rang supérieur. Cela me surprendrait, mais je n'ai pas de preuve que ce n'est pas possible. (La clé serait d'identifier un type convenablement polymorphe pour le lambda-bound. x .)

Si vous voulez un opérateur à virgule fixe en Haskell, vous pouvez en définir un très facilement car en Haskell, la liaison par let a une sémantique de virgule fixe :

fix :: (a -> a) -> a
fix f = f (fix f)

Vous pouvez l'utiliser de la manière habituelle pour définir des fonctions et même certaines structures de données finies ou infinies.

Il est également possible d'utiliser des fonctions sur des types récursifs pour mettre en œuvre des points fixes.

Si vous vous intéressez à la programmation avec des points fixes, vous devez lire le rapport technique de Bruce McAdam C'est tout ce qu'il y a à dire. .

Answer 3

La définition canonique du combinateur Y est la suivante :

y = \f -> (\x -> f (x x)) (\x -> f (x x))

Bien qu'il soit bien typé, il n'y a pas de vérification de type en Haskell à cause de l'attribut x x . Cela nécessiterait un type infini :

x :: a -> b -- x is a function
x :: a      -- x is applied to x
--------------------------------
a = a -> b  -- infinite type

Cependant, vous pouvez le forcer à vérifier la typologie en utilisant unsafeCoerce :: a -> b :

import Unsafe.Coerce

y :: (a -> a) -> a
y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x))

main = putStrLn $ y ("circular reasoning works because " ++)

Answer 4

Oh

cette page wiki et Cette réponse de Stack Overflow semblent répondre à ma question.
J'écrirai plus tard une explication plus détaillée.

Maintenant, j'ai trouvé quelque chose d'intéressant sur ce type de Mu. Considérons S = Mu Bool.

Data S = S (S -> Bool)

Si l'on considère S comme un ensemble et le signe égal comme un isomorphisme, alors l'équation devient

S ⇋ S -> Bool ⇋ Powerset(S)

Donc S est l'ensemble des ensembles qui sont isomorphes à leur powerset ! Mais nous savons, grâce à l'argument diagonal de Cantor, que la cardinalité de Powerset(S) est toujours strictement supérieure à la cardinalité de S, et qu'ils ne sont donc jamais isomorphes. Je pense que c'est la raison pour laquelle vous pouvez maintenant définir un opérateur de point fixe, même si vous ne pouvez pas le faire sans.