什么是非线性模式

Question

我正在阅读有关 servant-api DSL 的论文（请参阅 pdf here）

引用第 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 :>

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

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。

---

正如 cmets 中所指出的，linear 项可能来自 linear logic。这个逻辑有一个"resource interpretation"，从根本上说，隐含“消耗”它的前件以产生结果。

在其后续演算中，您不能像在经典逻辑中那样多次重用假设。这类似于线性模式：您不能多次重复使用同一个变量。 _{追问：为什么线性逻辑叫线性逻辑？不知道。}