Or-Patterns

Begin by defining Ord:

type Ord = {`lt +. `eq +. `gt};

Then we can write:

gt : Ord -- Bool
    := [ { { `lt⁻¹ & `eq⁻¹ } False & `gt⁻¹ True } ]

{`lt⁻¹ & `eq⁻¹} has type {`lt ⊕ `eq} --. The use of & to juxtapose pattern match arms is intended to recall \((G \oplus H)^\bot = G^\bot \& H^\bot\) from linear logic (Munch-Maccagnoni 2009).

This makes sense—a & (“with”) juxtaposes two pattern-match arms (inverse constructors) to form a (typed) function accepting a sum type as argument.

lte : { `lt +. `eq } --
    := [ { `lt⁻¹ & `eq⁻¹ } ]

gte : { `eq +. `gt } --
    := [ { `eq⁻¹ & `gt⁻¹ } ]

We could have defined gt with the above, viz.

gt : Ord -- Bool
   := [ { lte False & `gt⁻¹ True } ]

Pattern-match exhaustiveness checking in the presence of named or-patterns is still a matter of insisting on precise inverses. Had we written

lte : `lt  --
   := [ `lt⁻¹ ]

gt : Ord -- Bool
   := [ { lte False & `gt⁻¹ True } ]

We would be confronted with:

prelude/ord.piz:8:6: {`lt ⊕ `eq ⊕ `gt} ⊀ {`lt ⊕ `gt}

We can define something like or-patterns binding variables, allowing reuse of negative and positive aspect, viz.

type These a b = { a `left ⊕ b `right ⊕ a b `both };

left : { a `left ⊕ a b `both } -- a
     := [ { `left⁻¹ & `both⁻¹ nip } ]

maybeLeft : These(a,b) -- Maybe(a)
          := [ { left `just & `right⁻¹ drop `nothing } ]

hasLeft : These(a,b) -- Bool
        := [ { left drop True & `right⁻¹ drop False } ]

Inexhaustive patterns are still caught, i.e.

left : { a `left } -- a
     := [ { `left⁻¹ } ]

maybeLeft : These(a,b) -- Maybe(a)
          := [ { left `just & `right⁻¹ drop `nothing } ]

yields

test/examples/badOr.piz:9:13: {a `left ⊕ b `right ⊕ a b `both} ⊀ {a `left ⊕ b `right}

and

left : { a `left ⊕ a b `both } -- a
     := [ { `left⁻¹ & `both⁻¹ nip } ]

maybeLeft : These(a,b) -- Maybe(a)
          := [ { left `just } ]

yields

test/examples/badOr2.piz:9:13: {a `left ⊕ b `right ⊕ a b `both} ⊀ {a `left ⊕ a b `both}