什么是非线性模式

我正在阅读有关servant-api DSL（参见 pdfhere)

引用自第 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是一个（一维）线性函数，类似y = x² sin(x)将是非线性函数的一个例子。

我猜非线性来自类型构造函数（引用自第 3.3 节 类型是一等公民)

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

但我不太明白是什么让这个非线性，以及线性构造函数的一个例子是什么，如果我的猜测是正确的，构造函数引入了非线性。

线性模式是每个变量最多出现一个的模式。

非线性模式允许重复使用相同的变量名称，这意味着它匹配的所有值必须相等。

该文档所说的是，非线性模式在类型族定义中被接受，而它们是not在普通函数定义中：

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 mean? \x -> \x -> x? Or \x y | x == y -> x?

Also f x x = 1 would not是一个总函数。有一个隐藏的守卫，因此f [1..] [1..]会永远循环而不是简单地返回1.

正如评论中指出的那样，linear术语可能来自线性逻辑。这个逻辑有一个《资源解读》从根本上来说，蕴涵“消耗”其前因以产生结果。

In its sequent calculus you cannot reuse an hypothesis multiple times as you do in classical logic. This is akin to linear patterns: you cannot reuse the same variable multiple times. _{Follow-up question: why is linear logic called linear logic? No idea.}