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

Question

Довольно увлекательная 2013 вводного поста в Haskell основой KiCS2 реализации Curry Вольфганга Jeltsch, A Taste of 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 в потенциальный FUNC в качестве конструктора данных, но ++ в (также функциональном) шаблоне (xs ++ ys) в качестве имени функции?

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

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

P.S. Я адаптировал имена и типы подписей чуть-чуть по сравнению с исходным сообщением, чтобы упростить этот вопрос.

Answer 1

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

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

Answer 2

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

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

f (id x) = x 

преобразуется в

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

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

Теперь вы можете столкнуться с тем, что 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 для инверсии функций с различными уровнями.