What are nonlinear patterns

Viewed 2808

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.

1 Answers
Related