Granularizing "Not P" for error messages

Given a proposition P represented in Idris language, you can state that it's decidable by providing a proof for the following proposition:

p_is_decidable : Dec P

Decidability means that we can either refute or prove a proposition.

data Dec : Type -> Type where
  Yes : (prf : prop) -> Dec prop
  No  : (contra : prop -> Void) -> Dec prop

Lets provide some more difficult decidable property such as "Sum of numbers in a list":

data SumOf : List Nat -> Nat -> Type where
  ZeroSum : SumOf [] Z
  MoreSum : SumOf xs j -> k=i+j -> SumOf (i::xs) k

And lets provide a function that decides whether we have correct sum for a list.

nope_sum : SumOf (S x :: xs) Z -> Void
nope_sum ZeroSum impossible
nope_sum (MoreSum _ Refl) impossible

s_inj : S x = S y -> x = y
s_inj Refl = Refl

dec_sum : (xs:List Nat) -> (sum:Nat) -> Dec (SumOf xs sum)
dec_sum [] Z = Yes ZeroSum
dec_sum [] (S _) = No (\asum => case asum of
  ZeroSum impossible
  (MoreSum _ Refl) impossible)
dec_sum (Z :: xs) sum = case dec_sum xs sum of
  (Yes prf) => (Yes (MoreSum prf Refl))
  (No contra) => (No (\asum => case asum of 
    (MoreSum x Refl) => contra x))
dec_sum (S x :: xs) Z = No nope_sum
dec_sum (S x :: xs) (S y) = case dec_sum (x::xs) y of
  (Yes (MoreSum x prf)) => Yes (MoreSum x (cong prf))
  (No contra) => No (\asum => case asum of
    (MoreSum x prf) => contra (MoreSum x (s_inj prf)))

Now the Idris REPL can give us refutations and proofs that we can check:

*Refu> dec_sum [1,2] 2
No (\asum =>
      case asum of
        MoreSum x prf => contra (MoreSum x
                                         (s_inj prf))) : Dec (SumOf [1, 2] 2)
*Refu> dec_sum [1,2] 3
Yes (MoreSum (MoreSum ZeroSum Refl) Refl) : Dec (SumOf [1, 2] 3)

These proofs may be interesting because they describe how the property is holding for the values. Peeking at the definition we got proofs of SumOf xs j and 3=1+j contained in that structure, so we know the sum of the sublist is 2.

Negative proofs equally have information contained in them. You can see how different negative results keep changing:

*Refu> dec_sum [4] 3
No (\asum =>
      case asum of
        MoreSum x prf => contra (MoreSum x
                                         (s_inj prf))) : Dec (SumOf [4] 3)
*Refu> dec_sum [] 2
No (\asum =>
      case asum of
        ZeroSum => _
        MoreSum imp Refl => _) : Dec (SumOf [] 2)

At glance the negative proof doesn't provide anything we could deconstruct like we could do with positive proof.

You can construct a function to "unravel" the refutation and take it into parts:

minus_unit : {j:Nat} -> (j = j - 0)
minus_unit {j = Z} = Refl
minus_unit {j = (S k)} = Refl

incr_first : SumOf (left :: xs) right -> SumOf (S left :: xs) (S right)
incr_first (MoreSum x prf) = MoreSum x (cong prf)

unravel : (Not (SumOf (i::xs) j)) -> LTE i j -> (Not (SumOf xs (j-i)))
unravel f y z = case y of
  LTEZero => f (MoreSum z minus_unit)
  (LTESucc x) => unravel (f . incr_first) x z

There would seem to be a mechanical way to extract "destructors" for negation. We can apply the involution present in linear logic.

Translation to linear logic

There seem to be at least two ways to translate intuitionistic logic to linear logic. Let's use the call-by-name translation:

{X}     = X
{A → B} = !{A} ⊸ {B}
{A ∧ B} = {A} & {B}
{1}     = ⊤ 
{A ∨ B} = !{A} ⊕ !{B}
{0}     = 0
{∀xA}   = ∀x{A}
{∃xA}   = ∃x!{A}

Lets also translate our condition to these connectives:

data SumOf : List Nat -> Nat -> Type where
  ZeroSum : SumOf [] Z
  MoreSum : SumOf xs j -> k=i+j -> SumOf (i::xs) k

Lets first translate it to intuitionistic logic connectives:

SumOf xs j
    = ZeroSum: (list=[] ∧ sum=Z)
    ∨ MoreSum: (∃ys.∃i.∃k. SumOf ys k ∧ (j=i+k) ∧ (xs=i::ys))

I extract open the indexing proofs and added implicit arguments there. Here's the linear logic version:

SumOf xs j
    = ZeroSum: !(list=[] & sum=Z)
    ⊕ MoreSum: !(∃ys.!∃i.!∃k.!((SumOf ys k) & (j=i+k) & (xs=i::ys)))

Once you have a linear logic proposition, it's trivial to invert it.

~SumOf xs j
    = ZeroSum: ?(list≠[] ⊕ sum≠Z)
    & MoreSum: ?(∀ys.?∀i.?∀k.?((~SumOf ys k) ⊕ (j≠i+k) ⊕ (xs≠i::ys)))

There you have it. You can take 'fst' or 'snd' of the '&' -expression and obtain more interesting information.

If you take the 'ZeroSum' -branch, in this case you find out that the list is not empty, or then the sum is not zero. The question mark there has a meaning too, but it's a bit difficult to explain.

You have a similar situation going in the another branch. By varying the parameters ys, i, k you can get different conclusions about what's going on in the branch.

If we look at our unravel -function, it'd seem to follow the shape here. We just pass in values that ensure the (j=i+k) and (xs=i::ys) hold, so that the function cannot pass anything else except what we want. Of course if we pass something else, then we get a different answer!

The call-by-name translation means that we convert intuitionistic conjunction into a structure that is usually "incompatible" because we tend to assign enumerations into additive connectives. Call-by-value doesn't have this problem so it's interesting to see how the expression translates there. Here's the Call-by-value translation rules from the same source:

{X}     = X
{A → B} = !({A} ⊸ {B})
{A ∧ B} = !({A} ⊗ {B})
{1}     = !1 
{A ∨ B} = !({A} ⊕ !{B})
{0}     = !0
{∀xA}   = !∀x{A}
{∃xA}   = !∃x{A}

The translation is looking like this:

SumOf xs j
    = !(ZeroSum: !(!list=[] ⊗ !sum=Z)
      ⊕ MoreSum: !(∃ys.!∃i.!∃k.!(!SumOf ys k ⊗ !(j=i+k) ⊗ !(xs=i::ys))))

And the inverse of this is:

~SumOf xs j
    = ?(ZeroSum: ?(?list≠[] ⅋ ?sum≠Z)
      & MoreSum: ?(∀ys.?∀i.?∀k.?(?~SumOf ys k ⅋ ?(j≠i+k) ⅋ ?(xs≠i::ys))))

This expression doesn't seem to differ much from the earlier except that there's much of scoping and we have multiplicative connectives in there.

The connective (⅋) can be more difficult to understand, but it doesn't make this much worse. Basically we have this kind of thing going on:

?list≠[] ⅋ ?sum≠Z      is same as...

!list=[] ⊸ ?sum≠Z

!sum=Z ⊸ ?list≠[]

The information is same as before. The ZeroSum doesn't form a valid proof either because list isn't empty, or the sum isn't zero.

On the other side this is basically already a function:

∀ys.?∀i.?∀k.?(?~SumOf ys k ⅋ ?(j≠i+k) ⅋ ?(xs≠i::ys))

If we supply !(j=i+k) and !(xs=i::ys), we get ?~Sumof ys k.

There you have it, a simple way to deconstruct refutations. The only problem is that it's expressed in classical linear logic and that there's not an immediate, obvious way to translate it back.

Application in error messaging

So you may be still wondering "what does this have to do with error messaging?", in case you do here's a short explanation.

Computer systems usually do not tell people what went wrong, because there's extra effort involved in explaining why things didn't go like expected. It involves understanding the motivations of the user and examination of the problem against a model of some kind.

Error messages are usually short blurps explaining what step failed in the program. They are representative of ¬P, some proposition doesn't hold.

We really can't access the details directly because "Not P" is encoded as P → 0, which states that we can't supply a proof of P. There is no constructors for 0 and therefore there can't be a way to construct P because otherwise we'd be able to apply this function to produce 0.

But since we can't apply the function it means we can't directly deconstruct it either. Above we've produce an equivalent negative proposition that can be deconstructed directly. In linear logic every proposition has a De Morgan dual, which means that negation can be shifted downwards in the expression.

~(A ⊗ B) = ~A ⅋ ~B

This means that instead of "the stuff's not adding up", your program could present a model that you can fill up. "Did you expect that you gave in empty or filled list?" "There's this much sum left after the first number is taken out, do you think that adds up?" "Empty list can only sum to zero", etc...

Likewise this stuff can compose, how about the list must be 7 numbers long? Just add it to the conclusion and derive the inverted proof again. Keeps telling you that list can't be 3 numbers long then.

Often for good error reporting the program would have to do bit of more work. If there's problem with fetching network resources you usually like to know which resources you can't fetch, this involves attempting to fetch them. Such behavior would have to be included in the program but it isn't present in "stop as soon as there's a failure". To have that the behavior of the program needs to invert its behavior in middle and prepare an explanation for why it didn't go through. To do that you need to be able to decompose the inversion of the program and here you have it.

Similar posts