Error Hierarchies

A common situation: suppose various parts of a program can fail in specific, overlapping ways.

@lib/either

type RewriteError = { `scope };

type TypeError = RewriteError ∪ { `unificationFailed };

tyE : -- Either(TypeError,b)
    := [ `scope `left ]

handleRewrite : Either(RewriteError,Int) -- Int
              := [ { `left⁻¹ `scope⁻¹ 0 & `right⁻¹ } ]

handleTypeError : Either(TypeError,Int) -- Int
                := [ { `left⁻¹ `scope⁻¹ 0 & `right⁻¹ } ]

With tyE we can raise a `scope error while typechecking. handleRewrite allows us to (locally) handle a `scope error without being forced to handle a `unificationFailed where it will not occur.

Since handleTypeError is inexhaustive, however, we are faced with:

test/examples/errorHierarchy.piz:13:19: {`scope ⊕ `unificationFailed} ⊀ (ρ₁ ⊃ {`scope})

Thus our scheme is safe; with extensible cases, we do not need to resort to the lens kludge.