In Pizarnik, we can define functions on lists and they will work on non-empty lists.

type List a = { `nil ⊕ List(a) a `cons };

type NE a = { List(a) a `cons };

foldl : 'B [ 'B a -- 'B ] List(a) -- 'B
      := [ { `nil⁻¹ drop
           & `cons⁻¹ [dup] dip2 (142) [$] dip2 foldl
           }

type Unit = {`unit};

x : -- NE(Unit)
  := [ `nil `unit `cons ]

z : -- Unit
  := [ `unit [nip] x foldl ]

foldr accepts a List(a), i.e. { `nil ⊕ List(a) a `cons } as an argument; we can imagine how a pattern match that handles both the `nil and List(a) a `cons cases should handle an argument of type NE(a) = { List(a) `cons }.

Non-empty lists enforce the same safety as in Haskell:

         ]

Had we tried to write head : List(a) -- a:

5:17: {`nil ⊕ List(a) a `cons} ⊀ {ρ₁ a `cons}

Moreover, pattern-match exhaustiveness is enforced for non-empty lists, viz.

y : -- Unit
  := [ x head ]

is admissible, but

x : -- List(Unit)
  := [ `nil ]

w : -- Unit
  := [ x head ]

will fail:

23:8: ‘{`nil ⊕
       List( Unit ) Unit `cons}’ is not an acceptable argument, expected ‘{List( a ) a `cons}’

Polarity and Analogy

Doing the above in Haskell (for instance) is more fickle. We can define foldr to apply to both lists and non-empty lists using a typeclass, but we still need to write the implementation twice. And typeclass instance scoping is fraught.

Extensible cases (Blume et al. 2006) avoid this, in a way dual to row polymorphism—where it works, it is strictly preferable (McKenna 2013).

References