Y Combinator en Haskell

y-combinator

Question

¿Es posible escribir el Y Combinator en Haskell?

Parece que tendría un tipo infinitamente recursivo.

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

o algo. Incluso un simple factorial ligeramente factorizado

factMaker _ 0 = 1
factMaker fn n = n * ((fn fn) (n -1)
{- to be called as
(factMaker factMaker) 5
-}

falla con "Ocurre verificación: no se puede construir el tipo infinito: t = t -> t2 -> t1"

(El combinador Y se ve así

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

en el esquema) O, más sucintamente como

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

Para el orden de aplicación Y

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

Lo cual es solo una contracción de eta para la versión perezosa.

Si prefiere nombres cortos de variables.

Answer 1

Aquí hay una definición no recursiva del y-combinator en haskell:

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

punta de sombrero

Answer 2

El combinador Y no se puede tipear utilizando los tipos Hindley-Milner, el cálculo lambda polimórfico en el que se basa el sistema de tipos de Haskell. Puede probar esto recurriendo a las reglas del sistema de tipos.

No sé si es posible escribir el combinador Y dándole un tipo de rango superior. Me sorprendería, pero no tengo una prueba de que no sea posible. (La clave sería identificar un tipo polimórfico adecuado para la lambda-bound x ).

Si quiere un operador de punto fijo en Haskell, puede definir uno muy fácilmente porque en Haskell, let-binding tiene semántica de punto fijo:

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

Puede usar esto de la manera habitual para definir funciones e incluso algunas estructuras de datos finitas o infinitas.

También es posible usar funciones en tipos recursivos para implementar puntos fijos.

Si le interesa programar con puntos fijos, quiere leer el informe técnico de Bruce McAdam That About Wraps it Up .

Answer 3

La definición canónica del combinador Y es la siguiente:

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

Pero no comprueba el tipo en Haskell debido a xx , ya que requeriría un tipo infinito:

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

Si el sistema de tipos permitiera tales tipos recursivos, haría que la comprobación del tipo fuese indecidible (propenso a bucles infinitos).

Pero el combinador Y funcionará si lo fuerza a la verificación de tipo, por ejemplo, usando 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 " ++)

Esto no es seguro (obviamente). La respuesta de rampion demuestra una forma más segura de escribir un combinador de punto fijo en Haskell sin usar la recursión.

Answer 4

Oh

esta página wiki y esta respuesta de desbordamiento de pila parecen responder mi pregunta.
Escribiré más de una explicación más adelante.

Ahora, he encontrado algo interesante sobre ese tipo de Mu. Considera S = Mu Bool.

data S = S (S -> Bool)

Si uno trata a S como un conjunto y eso equivale a signo como isomorfismo, entonces la ecuación se vuelve

S ⇋ S -> Bool ⇋ Powerset(S)

¡Así que S es el conjunto de conjuntos que son isomórficos para su conjunto de poder! Pero sabemos por el argumento diagonal de Cantor que la cardinalidad de Powerset (S) es siempre estrictamente mayor que la cardinalidad de S, por lo que nunca son isomorfas. Creo que esta es la razón por la que ahora puede definir un operador de punto fijo, aunque no puede hacerlo sin uno.