Почему тип этой функции (a → a) → a?

Ответ 1

Ну, y должен иметь тип (a -> b) -> c, для некоторых a, b и c мы пока не знаем; в конце концов, она принимает функцию f и применяет ее к аргументу, поэтому она должна быть функцией, принимающей функцию.

Так как y f = f x (опять-таки, для некоторого x), мы знаем, что возвращаемый тип y должен быть возвратным типом f. Итак, мы можем немного уточнить тип y: он должен быть (a -> b) -> b для некоторых a и b, которые мы еще не знаем.

Чтобы выяснить, что такое a, нам просто нужно посмотреть тип значения, переданного в f. Это y f, который является выражением, которое мы пытаемся выяснить сейчас. Мы говорим, что тип y равен (a -> b) -> b (для некоторых a, b и т.д.), Поэтому мы можем сказать, что это приложение y f должно быть самого типа b.

Итак, тип аргумента f равен b. Поместите все это вместе, и мы получим (b -> b) -> b - это, конечно, то же самое, что и (a -> a) -> a.

Здесь более интуитивный, но менее точный взгляд на вещи: мы говорим, что y f = f (y f), которые мы можем развернуть до эквивалентных y f = f (f (y f)), y f = f (f (f (y f))) и т.д. Итак, мы знаем, что мы можем всегда применять еще один f вокруг всего этого, и поскольку "все это" является результатом применения аргумента f к аргументу, f должен иметь тип a -> a; и поскольку мы только пришли к выводу, что все это результат применения аргумента f к аргументу, возвращаемый тип y должен соответствовать типу f - вместе, опять же, как (a -> a) -> a.

Ответ 2

@ehird проделал хорошую работу по объяснению типа, поэтому я хотел бы показать, как он может решить значение с помощью некоторых примеров.

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

Вы можете выполнить те же действия с любой функцией, которая вам нравится, чтобы увидеть, что произойдет. Оба эти примера сходятся к значениям, но это не всегда происходит.

Ответ 3

Всего два вопроса, чтобы добавить к ответам других людей.

Функция, которую вы определяете, обычно называется fix, и это комбинатор с фиксированной запятой: функция, которая вычисляет фиксированная точка другой функции. В математике неподвижной точкой функции f является аргумент x такой, что f x = x. Это уже позволяет сделать вывод о том, что тип fix должен быть (a -> a) -> a; ", которая принимает функцию от a до a и возвращает a."

Вы вызвали свою функцию y, которая, кажется, после Y combinator, но это неточное имя: Y combinator - это один конкретный комбинатор с фиксированной точкой, но не тот, который вы определили здесь.

Я не понимаю, как f (y f) разрешает значение.

Ну, трюк в том, что Haskell - это нестрогий (a.k.a. "ленивый" ) язык. Расчет f (y f) может завершиться, если f не нужно оценивать аргумент y f во всех случаях. Итак, если вы определяете факториал (как поясняет Джон L), fac (y fac) 1 оценивает 1 без оценки y fac.

Строгие языки не могут этого сделать, поэтому в этих языках вы не можете определить комбинатор с фиксированной точкой таким образом. В этих языках комбинатор с фиксированной запятой учебника представляет собой Y combinator.

Ответ 4

Позвольте мне рассказать о комбинаторе. Он назвал "комбинатор исправлений" и обладает следующим свойством:

Свойство: "комбинатор исправлений" принимает функцию f :: (a -> a) и обнаруживает "фиксированную точку" x :: a этой функции, такую ​​что f x == x. Некоторые реализации комбинатора fixpoint могут быть лучше или хуже при "обнаружении", но при условии, что он завершается, он будет создавать фиксированную точку входной функции. Любая функция, удовлетворяющая свойству, может быть названа "комбинатором фиксированных точек".

Назовите этот "комбинатор исправлений" y. Исходя из того, что мы только что сказали, верно следующее:

-- as we said, y 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)

Итак, вы идете. Вы определили y в терминах существенного свойства комбинатора fixpoint:
y f == f (y f). Вместо того, чтобы предполагать, что y f обнаруживает x, вы можете предположить, что x представляет расходящееся вычисление и все равно приходит к одному и тому же выводу (iinm).

Так как ваша функция удовлетворяет Свойству, мы можем заключить, что это комбинатор фиксированных точек и что другие свойства, которые мы сформулировали, включая тип, применимы к вашей функции.

Это не совсем точное доказательство, но я надеюсь, что это даст дополнительную информацию.