¿Por qué es el tipo de esta función (a -> a) -> a?

Question

¿Por qué es el tipo de esta función (a -> a) -> a?

Prelude> let y f = f (y f) 
Prelude> :t y 
y :: (t -> t) -> t 

¿No debería ser un tipo infinito/recursivo? Iba a tratar de poner en palabras lo que creo que debería ser el tipo, pero simplemente no puedo hacerlo por alguna razón.

y :: (t -> t) -> ?WTFIsGoingOnOnTheRHS? 

No entiendo cómo f (y f) se resuelve a un valor. Lo siguiente tiene un poco más de sentido para mí:

Prelude> let y f x = f (y f) x 
Prelude> :t y 
y :: ((a -> b) -> a -> b) -> a -> b 

Pero todavía es ridículamente confuso. ¿Que esta pasando?

Answer 1

Bueno, y tiene que ser de tipo (a -> b) -> c, por alguna a, bc y no sabemos todavía; después de todo, toma una función, f, y la aplica a un argumento, por lo que debe ser una función que tome una función.

Desde y f = f x (de nuevo, por alguna x), sabemos que el tipo de retorno de y debe ser el tipo de retorno de f sí. Por lo tanto, podemos refinar un poco el tipo de y: debe ser (a -> b) -> b para algunos a y b que aún no conocemos.

Para averiguar qué es a, solo tenemos que mirar el tipo del valor pasado a f. Es y f, que es la expresión que estamos tratando de averiguar el tipo de ahora. Estamos diciendo que el tipo de y es (a -> b) -> b (para algunos a, b, etc.), por lo que podemos decir que esta aplicación de y f debe ser del tipo b.

Por lo tanto, el tipo de argumento para f es b. Vuelva a poner todo junto, y obtenemos (b -> b) -> b, que es, por supuesto, lo mismo que (a -> a) -> a.

Aquí es una visión más intuitiva, pero menos preciso de las cosas: estamos diciendo que y f = f (y f), que podemos ampliar el equivalente a y f = f (f (y f)), y f = f (f (f (y f))), y así sucesivamente. Por lo tanto, sabemos que siempre podemos aplicar otro f en todo el asunto, y dado que "todo" en cuestión es el resultado de aplicar f a un argumento, f tiene que tener el tipo a -> a; y dado que acabamos de concluir que todo es el resultado de aplicar f a un argumento, el tipo de retorno de y debe ser el mismo de f - volviendo a juntarse, una vez más, como (a -> a) -> a.

Answer 2

@ ehird ha hecho un buen trabajo al explicar el tipo, por lo que me gustaría mostrar cómo se puede resolver con algunos ejemplos.

f1 :: Int -> Int 
f1 _ = 5 

-- expansion of y applied to f1 
y f1 
f1 (y f1) -- definition of y 
5   -- definition of f1 (the argument is ignored) 

-- here's an example that uses the argument, a factorial function 
fac :: (Int -> Int) -> (Int -> Int) 
fac next 1 = 1 
fac next n = n * next (n-1) 

y fac :: Int -> Int 
fac (y fac) -- def. of y 
    -- at this point, further evaluation requires the next argument 
    -- so let's try 3 
fac (y fac) 3 :: Int 
3 * (y fac) 2    -- def. of fac 
3 * (fac (y fac) 2)  -- def. of y 
3 * (2 * (y fac) 1)  -- def. of fac 
3 * (2 * (fac (y fac) 1) -- def. of y 
3 * (2 * 1)    -- def. of fac 

Puede seguir los mismos pasos con cualquier función que desee para ver lo que sucederá. Ambos ejemplos convergen en valores, pero eso no siempre sucede.

Answer 3

Déjame contar sobre un combinador.Se llama el "combinador punto fijo" y tiene la siguiente propiedad:

La propiedad: el "punto fijo combinador" toma una función f :: (a -> a) y descubre un "punto fijo" x :: a de esa función tal que f x == x. Algunas implementaciones del combinador de puntos de control pueden ser mejores o peores al "descubrir", pero suponiendo que termine, producirá un punto fijo de la función de entrada. Cualquier función que satisfaga la propiedad se puede llamar un "combinador de punto fijo".

Llama a este "combinador de punto fijo" y. En base a lo que acabamos de decir, los siguientes son verdaderos:

-- as we said, y's input is f :: a -> a, and its output is x :: a, therefore 
y :: (a -> a) -> a 

-- let x be the fixed point discovered by applying f to y 
y f == x -- because y discovers x, a fixed point of f, per The Property 
f x == x -- the behavior of a fixed point, per The Property 

-- now, per substitution of "x" with "f x" in "y f == x" 
y f == f x 
-- again, per substitution of "x" with "y f" in the previous line 
y f == f (y f) 

Así que listo. Tiene definidoy en términos de la propiedad esencial del combinador de punto fijo:
y f == f (y f). En lugar de suponer que y f descubre x, puede suponer que x representa un cálculo divergente y aún así llegar a la misma conclusión (iinm).

Dado que su función cumple con la propiedad, podemos concluir que es un combinador de punto fijo, y que las demás propiedades que hemos mencionado, incluido el tipo, son aplicables a su función.

Esto no es exactamente una prueba sólida, pero espero que proporcione información adicional.

Answer 4

Solo dos puntos para agregar a las respuestas de otras personas.

La función que está definiendo generalmente se llama fix, y es un fixed-point combinator: una función que calcula la fixed point de otra función. En matemáticas, el punto fijo de una función f es un argumento x tal que f x = x. Esto ya le permite inferir que el tipo de fix tiene que ser (a -> a) -> a; "función que toma una función de a a a, y devuelve un a."

que ha llamado a su función y, que parece ser después de la Y combinator, pero esto es un nombre inexacto: el combinador Y es uno combinador de punto fijo específico, pero no es el mismo que el que haya definido aquí.

No entiendo cómo f (y f) se resuelve a un valor.

Bueno, el truco es que Haskell es un lenguaje no estricto (a.k.a. "perezoso"). El cálculo de f (y f) puede finalizar si f no necesita evaluar su argumento y f en todos los casos. Por lo tanto, si define factorial (como lo ilustra John L), fac (y fac) 1 evalúa a 1 sin evaluar y fac.

Los idiomas estrictos no pueden hacer esto, por lo que en esos idiomas no se puede definir un combinador de punto fijo de esta manera. En esos idiomas, el combinador de punto fijo de libro de texto es el combinador en Y adecuado.