Y Combinator en Haskell

Question

¿Es posible escribir la Y Combinator en Haskell?

Parece que tendría un tipo infinitamente recursiva.

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

o algo así. Incluso un simple ligeramente factorizada factorial

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

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

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

(Los Y Combinator tiene este aspecto

(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 la orden aplicativa Y

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

¿Qué es una contracción eta distancia para la versión perezoso.

Si prefiere nombres cortos variables.

Answer 1

Oh

esta página wiki y Esta respuesta desbordamiento de pila parecen responder a mi pregunta.
Voy a escribir más de una explicación más tarde.

Ahora, he encontrado algo interesante acerca de ese tipo Mu. Considere S = Mu Bool.

data S = S (S -> Bool)

Si uno trata a S como un conjunto y que es igual signo 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 argumento diagonal de Cantor que la cardinalidad de Powerset (S) siempre es estrictamente mayor que la cardinalidad de S, por lo que nunca son isomorfos. Creo que esto es por lo que ahora se puede definir un operador de punto fijo, a pesar de que no se puede sin él.

Answer 2

Aquí hay 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)

sombrero de punta

Answer 3

El combinador Y no puede ser escrito utilizando tipos Hindley-Milner, el cálculo lambda polimórfica en la que el sistema de tipos de Haskell se basa. Puede probar esto apelando 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 es posible. (La clave sería identificar un tipo adecuadamente polimórfico para el x lambda-bound.)

Si quieres un operador de coma fija en Haskell, se puede definir muy fácilmente porque en Haskell, y mucho vinculante tiene la semántica de punto fijo:

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

Se puede utilizar esta en la forma habitual para definir las funciones e incluso algunas estructuras de datos finita o infinita.

También es posible utilizar las funciones de tipos recursivos para implementar puntos fijos.

Si está interesado en la programación con puntos fijos, que desea leer el informe técnico de Bruce McAdam Ese Sobre lo envuelve .

Answer 4

La definición canónica del combinador Y es como sigue:

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

Pero no tipo de comprobación en Haskell, debido a la x x, ya que requeriría un tipo infinita:

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

Si el sistema de tipos iban a permitir que tales tipos recursivos, que harían que la comprobación de tipos indecidible (propenso a bucles infinitos).

Sin embargo, el combinador Y funcionará si lo fuerzas a typecheck, por ejemplo, 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 respuesta demuestra una forma más segura para escribir un combinador punto fijo en Haskell sin utilizar la recursividad.