Компактное или полное / подробное определение обратного комбинатора / оператора в карри

Question

Довольно захватывающая вводная статья 2013 года о реализации Curry KiCS2 на Haskell, написанная Вольфгангом Йельчем, "Вкус Curry", дает следующее определение для inverse комбинатор:

inverse :: (a -> b) -> (b -> a)
inverse f y | f x =:= y = x where x free

(Примечание: это делает такие вещи, как inverse (+1) 3 == 2 а также inverse (*3) 12 == 4 а также inverse htmlHodeToStr == parseHtmlNode и бесконечность других невероятно удивительных вещей, для прохожих, не знакомых с Карри)

Кроме того, он также предлагает 2 альтернативных, но эквивалентных определения (недетерминированных) split :: [a] -> ([a], [a]) функция:

split :: [a] -> ([a],[a])
split list | front ++ rear =:= list = (front,rear)

а также

split' :: [a] -> ([a],[a])
split' (xs ++ ys) = (xs,ys)

а также некоторые другие довольно поучительные определения, которые, однако, выходят за рамки этого поста.

Однако мое мышление заставило меня попробовать альтернативное, сжатое определение inverse в духе split а также split':

inverse' :: (a -> b) -> (b -> a)
inverse' f (f x) = x

это, с другой стороны, приводит к следующей ошибке:

Undefined data constructor `f'

Мой вопрос: почему Карри интерпретирует f в потенциальной функциональной схеме (f x) в качестве конструктора данных, но ++ в (также функциональной) схеме (xs ++ ys) как имя функции?

Другими словами, xs а также ys в split' (xs ++ ys) = (xs,ys) кажется, просто точно аналогично x в inverse' f (f x) = x,

Или если аналогия с split' не сразу очевидно, рассмотрим prefix (xs ++ _) = xs или же orig (1 + x) = x и т.д., оба из которых компилируются и работают просто отлично.

PS Я немного адаптировал имена и типовые сигнатуры по сравнению с оригинальным постом, чтобы облегчить понимание этого вопроса.

Answer 1

Для этого ограничения есть семантическая причина (так что автоматическая десагеринг нецелесообразен). Концептуально семантика функциональных шаблонов определяется путем оценки (сужения) функциональных шаблонов до терминов данных и замены функциональных шаблонов этими терминами данных, чтобы они действовали как стандартные шаблоны. Чтобы использовать эту идею в качестве конструктивного определения, требуется, чтобы функции, используемые в функциональных шаблонах, были определены на "более низком уровне", чем функция, содержащая функциональные шаблоны. Следовательно, должно существовать отображение уровня для всех функций. Это подробно описано в статье о функциональных шаблонах (но не проверено текущим компилятором). Как следствие, функциональные переменные в функциональных шаблонах не допускаются.

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

Answer 2

Проще говоря, синтаксис функциональных шаблонов, таких как f x требует функции f быть определенной функцией, доступной в области inverse'вот почему xs ++ ys работает, где f x не.

Это мотивировано реализацией функциональных паттернов. Они превращаются в вызов примитивного оператора =:<= выполняя своего рода "ленивое" объединение (ленивое, потому что оно может связывать свободные переменные с выражениями вместо значений), где переменные, встречающиеся в шаблоне, представляются как свежие логические переменные. Таким образом, функция

f (id x) = x

превращается в

f y | id x =:<= y = x  where x free

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

Теперь вы можете столкнуться с этим f на самом деле не является свободной переменной, так как она определяется первым аргументом inverse'и это действительно так. Определение inverse' также использует синтаксис нелинейных шаблонов (так как f происходит дважды), и его перевод заменяет повторяющиеся переменные новыми, а затем объединяет ранее повторяющиеся переменные путем строгой унификации. Например,

pair (x, x) = success

эквивалентно определению

pair' (x, y) | x =:= y = success

так что ваш пример будет преобразован в

inverse' f y | f =:= g & g x =:<= y = x where g, x free

Обратите внимание, что это требует строгой унификации функций, которая в настоящее время не поддерживается в KiCS2. Однако это определение работает в PAKCS.

Если мы, однако, еще больше упростим это определение, мы получим

inverse' f y | f x =:<= y = x where x free

и, наконец, это определение работает, как и ожидалось, в PAKCS и KiCS2.

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

Наконец, также существует библиотека FunctionInversion для PAKCS и KiCS2, который обеспечивает функции invf1 в invf5 для инверсии функций с разными арностями.