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

Почему тип этой функции (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

Но это все еще до смешного сбивает с толку. Что происходит?

21
задан TheIronKnuckle 18 January 2012 в 23:20
поделиться

1 ответ

@ 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

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

9
ответ дан 29 November 2019 в 06:53
поделиться
Другие вопросы по тегам:

Похожие вопросы: