Что такое нелинейные паттерны

Question

Я читаю газету о servant-api DSL (см. pdf здесь)

Цитата из Раздела 5.2 Напечатайте безопасные ссылки (подчеркните добавленные мной)

type family ElSymbol e (s :: Symbol) a :: Bool where
ElSymbol (s :> e) s a = Elem e a
ElSymbol e s a = False

Обратите внимание, что семейства типов в GHC - в отличие от нормальных определений функций - допускают нелинейные шаблоны и двойное вхождение s С левой стороны первого случая подразумевается, что оба символа должны быть равны.

Что такое нелинейные паттерны в haskell?

Тот факт, что оба случая s должно быть равным, ясно, что это является следствием ScopedTypeVariables-pragma.

Я знаю линейные / нелинейные функции только в контексте математики, где y = kx + d является (1-мерной) линейной функцией и что-то вроде y = x² sin(x) будет примером для нелинейной функции.

Я предполагаю, что нелинейность исходит от конструктора типов (цитата из раздела 3.3. Типы - граждане первого класса)

data (item :: k) :> api
infixr 9 :>

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

Answer 1

Линейный шаблон - это шаблон, в котором каждая переменная появляется не более одного.

Нелинейный шаблон позволяет повторно использовать одно и то же имя переменной, подразумевая, что все значения, которые ему соответствуют, должны быть равны.

Документация говорит, что нелинейные шаблоны принимаются в определениях семейств типов, в то время как их нет в определениях обычных функций:

Prelude> let f x x = x

<interactive>:2:7:
    Conflicting definitions for ‘x’
    Bound at: <interactive>:2:7
              <interactive>:2:9
    In an equation for ‘f’

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

Итак: нет, конструкторы типов не имеют ничего общего с линейностью / нелинейностью. Это просто, как вы используете переменные в сопоставлении с образцом.

---

Что касается того, почему у Haskell нет нелинейных шаблонов для определения функций: есть минусы. Например, что должно \x x -> x имею в виду? \x -> \x -> x? Или же \x y | x == y -> x?

Также f x x = 1 не будет общей функцией. Там скрытый охранник, и, таким образом, f [1..] [1..] будет цикл навсегда вместо простого возвращения 1,

---

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

В его последовательном исчислении вы не можете повторно использовать гипотезу несколько раз, как в классической логике. Это похоже на линейные шаблоны: вы не можете использовать одну и ту же переменную несколько раз. _{Дополнительный вопрос: почему линейная логика называется линейной логикой? Без понятия.}