Y Combinator en Haskell

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 así. Incluso un simple ligeramente factorizar factorial

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

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

falla con "Ocurre cheque: no se puede construir el tipo infinita: t = t -> t2 -> t1"

(El combinador Y se parece a esto

(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 applicat Para ive Y

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

que se encuentra a la contracción eta distancia para la versión perezoso.

Si prefiere nombres cortos de variables.

Answer 1

Oh

this wiki page y This Stack Overflow answer parecen responder a mi pregunta.
Voy a 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 que el signo igual como isomorfismo, entonces la ecuación se convierte en

S ⇋ S -> Bool ⇋ Powerset(S) 

Así que S es el conjunto de los conjuntos que son isomorfos a su powerset! 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 es por eso que ahora puede definir un operador de punto fijo, aunque no puede hacerlo sin uno.

Answer 2

Aquí es una definición no recursiva de la Y-Combinator en Haskell:

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

hat tip

Answer 3

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

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

Pero no escribe check en Haskell debido al x x, 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 sea indecidible (propenso a bucles infinitos).

Pero el combinador Y funcionará si lo fuerza a la verificación de tipo, p. mediante el uso de 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). rampion's answer demuestra una forma más segura de escribir un combinador de punto fijo en Haskell sin usar recursión.

Answer 4

El combinador Y no se puede escribir con 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 en 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 el lambda-bound x.)

Si quiere un operador de punto fijo en Haskell, puede definir uno muy fácilmente porque en Haskell, dejar-encuadernar ha fijado- la semántica de punto:

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

Usted puede utilizar esto en la forma habitual para definir las funciones e incluso algunas estructuras de datos finito o infinito.

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

Si está interesado en programar puntos fijos, quiere leer el informe técnico de Bruce McAdam That About Wraps it Up.