Как это определение ArrowLoop.loop работает?

Экземпляр функции для ArrowLoop содержит

loop :: ((b,d) -> (c,d)) -> (b -> c)
loop f b = let (c,d) = f (b,d) in c

Сначала у меня проблема с сигнатурой: как мы можем получить b -> c из (b,d) -> (c,d)? Я имею в виду, что c в полученном кортеже может зависеть от обоих элементов ввода, как можно "отрезать" влияние d?

Во-вторых, я не понимаю, как работает let. Не содержит (c,d) = f (b,d) циклическое определение для d? Откуда приходит d? Честно говоря, я удивлен, что это допустимый синтаксис, поскольку, похоже, мы бы пересмотрели d.

Я имею в виду, что в математике это имело бы смысл, например. f может быть сложной функцией, но я бы предоставил только реальную часть b, и мне нужно было бы выбрать мнимую часть d таким образом, чтобы она не менялась, когда я оценивал f (b, d), что сделало бы ее некоторая фиксированная точка. Но если эта аналогия имеет место, выражение let должно каким-то образом "искать" для этой неподвижной точки для d (и может быть больше одного). Которая выглядит близко к магии для меня. Или я считаю слишком сложным?

Ответ 1

Это работает так же, как работает стандартное определение fix:

fix f = let x = f x in x

i.e, он находит неподвижную точку в точно так же, как fix делает: рекурсивно.

Например, в качестве тривиального примера рассмотрим loop (\((),xs) -> (xs, 1:xs)) (). Это похоже на fix (\xs -> 1:xs); мы игнорируем наш вход и используем вывод d (здесь xs) в качестве нашего основного вывода. Дополнительный элемент в кортеже, который loop имеет, состоит только в том, чтобы содержать входной параметр и выходное значение, поскольку стрелки не могут выполнять currying. Подумайте, как определить факториальную функцию с помощью fix - вы закончите использование currying, но при использовании стрелок вы будете использовать дополнительный параметр и вывод, который дает loop.

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

Ответ 2

"Поиск фиксированной точки" - это именно то, что это делает. Это ленивость Хаскелла в действии. Подробнее см. Wikipedia.