Я не претендую на то, что понимаю это вообще, но если это кому-нибудь поможет ... тогда идиот.
Рассмотрим определение fix
.fix f = let x = f x in x
.Потрясающая часть состоит в том, что x
определяется как f x
.Но подумайте минутку.
x = f x
Поскольку x = fx, тогда мы можем подставить значение x
в правой части этого, верно?Таким образом, поэтому ...
x = f . f $ x -- or x = f (f x)
x = f . f . f $ x -- or x = f (f (f x))
x = f . f . f . f . f . f . f . f . f . f . f $ x -- etc.
Таким образом, хитрость заключается в том, что для завершения f
необходимо сгенерировать какую-то структуру, чтобы более поздний f
мог сопоставить шаблон с этой структурой и завершитьрекурсия, фактически не заботясь о полном «значении» ее параметра (?)
Если, конечно, вы не захотите сделать что-то вроде создания бесконечного списка, как иллюстрировал Luqui.
TomMD'sфакториальное объяснение это хорошо.Тип подписи исправления (a -> a) -> a
.Подпись типа для (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1)
- (b -> b) -> b -> b
, другими словами, (b -> b) -> (b -> b)
.Таким образом, мы можем сказать, что a = (b -> b)
.Таким образом, fix принимает нашу функцию, которая a -> a
, или действительно, (b -> b) -> (b -> b)
, и возвращает результат типа a
, другими словами, b -> b
, другими словами, другую функцию!
Подождите, я думал, что это должно было вернуть фиксированную точку ... не функцию.Ну, это так, вроде (поскольку функции являются данными).Вы можете себе представить, что это дало нам окончательную функцию для поиска факториала.Мы дали ему функцию, которая не знает, как выполнить рекурсию (следовательно, один из параметров для нее - это функция, используемая для рекурсии), и fix
научил ее, как выполнять рекурсию.
Помните, как я сказал, чтоf
должен генерировать какую-то структуру, чтобы более поздний f
мог сопоставить и завершить шаблон?Ну, это не совсем верно, я думаю.TomMD проиллюстрировал, как мы можем расширить x
, чтобы применить функцию и перейти к базовому сценарию.Для своей функции он использовал if / then, и это является причиной прекращения.После многократных замен часть in
всего определения fix
в конце концов перестает быть определена в терминах x
, и именно тогда она вычислима и завершена.