Каковы нелинейные модели

Question

Я читал газету о servant -api DSL (см PDF here)

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

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

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

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

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

Я знаю линейные/нелинейные функции только из контекста математики, где y = kx + d является (одномерной) линейной функцией и что-то вроде 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’ 

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

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

---

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

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

---

Как уже отмечались в комментариях линейного термина может исходить от linear logic. Эта логика имеет "resource interpretation", где, по сути, импликация «поглощает» ее антецедент, чтобы произвести последующую.

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