什么是非线性模式 [英] What are nonlinear patterns

问题描述

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

引用来自第5.2节类型安全链接（强调添加了me）

 类型系列ElSymbol e（s :: Symbol）a :: Bool其中
 ElSymbol（s：> e）sa = Elem ea 
 ElSymbol esa = False 
  

请注意，GHC中的类型族 - 与正常函数定义不同 -
允许非线性模式，并且 s 第一个案例左边的
手边意味着两个符号必须相同。

haskell中的线性模式？

s 必须相等的事实是清楚这是 ScopedTypeVariables -pragma的结果。

我知道lin耳朵/非线性函数仅在数学上下文中，其中 y = kx + d 是一个（1维）线性函数，类似于 y =x²sin（x）是一个非线性函数的例子。

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

 数据（item :: k）：> api 
 infixr 9：> 
  

但我不明白是什么让这个非线性的，和如果我的猜测是正确的，构造函数将引入非线性，那么线性构造函数的一个例子是什么？ 解析方案

>一个线性模式是一个模式，其中每个变量至多出现一个模式。

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

文档的意思是非线性模式在类型族定义中被接受，而在正常函数定义中 not ：

  Prelude> let fxx = x 
 
< interactive>：2：7：
'x'
的定义冲突：< interactive>：2：7 
 < interactive>：2：9 
在等式'f'中
  

深在这。还有其他语言允许在函数定义中使用非线性模式（例如Curry）。

因此：不，类型构造函数与线性/非线性无关。就是你在模式匹配中如何使用变量。

---

至于为什么Haskell没有函数的非线性模式定义：有缺点。例如，什么应该 \x x - > x 是什么意思？ \x - > \x - > X ？或 \ x y | x == y - > x ？

fxx = 1 would not 是一个总功能。有一个隐藏的警卫，因此 f [1 ..] [1 ..] 会永远循环，而不是简单地返回 1 。

---

正如在评论中已经指出的那样，线性来自 线性逻辑 。这个逻辑有一个资源解释，从根本上说，这意味着消耗了它的先行词为了产生结果。

在它的连续微积分中，你不能像经典逻辑那样多次重复使用一个假设。这类似于线性模式：您不能多次重复使用相同的变量。
_{后续问题：线性逻辑为什么称为线性逻辑？不知道。}

I am reading the paper about the servant-api DSL (see pdf here)

Quoting from Section 5.2 Type safe Links (emphasize added by me)

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

Note that type families in GHC – unlike normal function definitions – allow non-linear patterns, and the double occurrence of s on the left hand side of the first case implies that both symbols must be equal.

What are non-linear patterns in haskell?

The fact that both occurrences of s need to be equal, is clear this is a consequence of the ScopedTypeVariables-pragma.

I know linear/non-linear functions only from the context of mathematics where y = kx + d is a (1-dimensional) linear function and something like y = x² sin(x) would be an example for a non-linear function.

I guess the non-linearity comes from the type constructor (Quoting from Section 3.3 Types are first-class citizens)

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

but I cannot quite understand what makes this non-linear, and what would be an example of a linear constructor, if my guess is correct, that the constructor is introducing the non-linearity.

解决方案

A linear pattern is a patter where each variable appears at most one.

A non-linear pattern allows reusing the same variable name implying that all the values matched by it must be equal.

What the documentation is saying is that non linear patterns are accepted in type families definitions while they are not in normal function definitions:

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’

There's nothing "deep" in this. There are other languages which allow "non linear" patterns in function definitions (e.g. Curry).

So: no, type constructors have nothing to do with linearity/non linerity. Is just how you use variables in the pattern matching.

---

As to why Haskell doesn't have non linear patterns for function definitions: there are cons. For example what should \x x -> x mean? \x -> \x -> x? Or \x y | x == y -> x?

Also f x x = 1 would not be a total function. There's an hidden guard, and thus f [1..] [1..] would loop forever instead of simply returning 1.

---

As has been pointed out in the comments, the linear term may come from linear logic. This logic has a "resource interpretation" where, fundamentally, implication "consumes" its antecedent in order to produce the consequent.

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.}

这篇关于什么是非线性模式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！