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

Question

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

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

Разве это не должен быть бесконечный / рекурсивный тип? Я собирался выразить словами то, что, по моему мнению, должно быть написано, но по какой-то причине просто не могу.

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

Я не понимаю, как f (y f) разрешается в значение. Следующее имеет немного больше смысла для меня:

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

Но это все равно смешно. Что происходит?

Answer 1

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

Поскольку y f = f x (опять же, для некоторых x), мы знаем, что тип возвращаемого значения y должен быть типом возврата самого f. Таким образом, мы можем немного уточнить тип y: для некоторых a и b, которые мы пока не знаем, это должно быть (a -> b) -> 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.

Answer 2

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

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

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

Iне поймите, как f (yf) разрешает значение.

Хорошо, уловка в том, что Haskell является нестрогим (иначе говоря, "ленивым") языком.Вычисление f (y f) может быть прекращено, если f не нужно оценивать свой аргумент y f во всех случаях.Итак, если вы определяете факториал (как иллюстрирует Джон Л.), fac (y fac) 1 оценивается как 1 без оценки y fac.

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

Answer 3

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

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

Answer 4

Позвольте мне рассказать о комбинаторе. Он называется «комбинатор точек фиксации» и имеет следующее свойство:

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

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

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

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

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

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