por - pattern matching haskell

¿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 intentar 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 (yf) se resuelve en 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 sigue siendo ridículamente confuso. ¿Que esta pasando?

Answer 1

@ ehird ha hecho un buen trabajo explicando el tipo, por lo que me gustaría mostrar cómo se puede resolver con un valor 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 qué sucederá. Ambos ejemplos convergen en valores, pero eso no siempre sucede.

Answer 2

Bueno, y tiene que ser de tipo (a -> b) -> c , para algunos a , b aún no lo sabemos; 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.

Dado que yf = fx (de nuevo, para alguna x ), sabemos que el tipo de retorno de y debe ser el tipo de retorno de f . Entonces, podemos refinar el tipo de y un bit: debe ser (a -> b) -> b para algunos a y b que aún no sabemos.

Para averiguar qué es, solo tenemos que mirar el tipo del valor pasado a f . Es yf , que es la expresión que estamos tratando de descubrir 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 yf debe ser de tipo b sí misma.

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

Aquí hay una visión más intuitiva pero menos precisa de las cosas: estamos diciendo que yf = f (yf) , que podemos expandir al equivalente yf = f (f (yf)) , yf = f (f (f (yf))) , y así sucesivamente. Entonces, sabemos que siempre podemos aplicar otro tipo de f alrededor de todo, 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 el asunto es el resultado de aplicar f a un argumento, el tipo de retorno de y debe ser el de f sí mismo, que vuelve a unirse, de nuevo, como (a -> a) -> a .

Answer 3

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

La propiedad : el "combinador de punto fijo" toma una función f :: (a -> a) y descubre un "punto fijo" x :: a de esa función tal que fx == 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".

Llamar 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)

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

Como su función cumple con la propiedad, podemos concluir que es un combinador de punto fijo y que las otras propiedades que hemos establecido, incluido el tipo, son aplicables a su función.

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

Answer 4

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

La función que está definiendo se suele llamar fix , y es un combinador de punto fijo : una función que calcula el punto fijo de otra función. En matemáticas, el punto fijo de una función f es un argumento x tal que fx = x . Esto ya le permite inferir que el tipo de fix debe ser (a -> a) -> a ; "función que toma una función de a , y devuelve una a ".

Has llamado a tu función y , que parece estar después del combinador Y , pero este es un nombre inexacto: el combinador Y es un combinador de punto fijo específico, pero no el mismo que el que has definido aquí.

No entiendo cómo f (yf) se resuelve en un valor.

Bueno, el truco es que Haskell es un lenguaje no estricto (también conocido como "perezoso"). El cálculo de f (yf) puede terminar si f no necesita evaluar su argumento yf en todos los casos. Entonces, si está definiendo factorial (como lo ilustra John L), fac (y fac) 1 evalúa a 1 sin evaluar y fac .

Los lenguajes 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.