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

Question

Экземпляр функции для 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 (а их может быть несколько).Который выглядит близко к магии для меня.Или я считаю слишком сложным?

Answer 1

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

fix f = let x = f x in x

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

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

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

Answer 2

«Поиск фиксированной точки» равен точно , что это делает.Это лень Хаскелла в действии.Подробнее на Википедии .