# Being Positively Negative.

We will need some helpers…

import Decidable.Equality
import Data.List
import Data.Nat
import Data.Zippable


# Being Truthful

namespace Intro


Predicates and their decision procedures are a core technique in dependently-typed programming to represent truth (predicate) and a way to discern if something holds (the decision procedure). Take for example, existential quantification that an element is in a list. Standard functional programming techniques would represent this as a boolean test.

  isElem : Eq type
=> (x  :      type)
-> (xs : List type)
-> Bool
isElem x []
= False
isElem x (y :: ys)
= x == y || isElem x ys


# Predicates hold the Truth

namespace Predicates


We can make this programme stronger using dependent types. First we define a predicate to describe what it means for an element to exist within a list.

  data IsElem : (x  :      type)
-> (xs : List type)
-> Type
where


If we find the element we are looking for then stop.

    Here : (prf : x = y)
-> IsElem x (y::ys)


Otherwise, carry on looking.

    There : (no : x = y -> Void)
-> (later : IsElem x     ys)
-> IsElem x (y::ys)


This is the ‘proof’ (or truth) that some element is in a list. Although IsElem is a proof it contains both positive and negative structures. Positive structures are constructive i.e. we can construct them; and Negative structures are those we must show are false. With this definition we cannot use Idris2’s program synthesis to construct instances of IsElem. Generally speaking, we cannot construct negative structures Thus we use a more strictly positive version:

  namespace Strictly
public export
data IsElem : (x  :      type)
-> (xs : List type)
-> Type
where

Here : (prf : x = y)
-> Strictly.IsElem x (y::ys)
There : (later : Strictly.IsElem x     ys)
-> Strictly.IsElem x (y::ys)


If we examine the definition of IsElem, we can see that it only works for non-empty lists. We can use this fact to identify and present the case when we cannot inhabit (i.e. fill-in) one of the type-level values for the IsElem type. In this case that empty lists cannot happen.

  export
Uninhabited (Strictly.IsElem x Nil) where
uninhabited (Here prf) impossible
uninhabited (There later) impossible


# Decisions, Decisions, Decisions

namespace Decisions


We must now write a function (decision procedure) to attempt to build this truth. The return result, however, cannot be an instance of Bool, the result needs to be the ’truth’. Realistically, the truth is not always possible and we need to represent this in our result.

Intuitively we can use the Maybe that supports returning Nothing if we fail, or Just a value when we do not. This is, however, not strong enough. When failing we also need to provide evidence of why something is wrong: the contradiction. To this end we need Dec a data structure that will return the truth if the truth is out there, or evidence that the truth is not there. Dec is defined as:

  public export
data Dec : (pred : Type)
-> Type
where
Yes : (prf : prfType)
-> Dec prfType

No : (no : prfType -> Void)
-> Dec prfType


Using Dec we can construct our decision procedure, using decidable equality to help provably decided if two things are equal. If we examine the No case you will see that it only provides the proof of contradition. Later on we will see that this is not sufficient for interactive programs.

  export
isElem : DecEq type
=> (x  :      type)
-> (xs : List type)
-> Dec (IsElem x xs)


Empty lists are absurd.

  isElem x []
= No absurd


  isElem x (y :: xs) with (decEq x y)


If we have found the element then stop.

    isElem x (x :: xs) | (Yes Refl)
= Yes (Here Refl)


Otherwise we examine the tail.

    isElem x (y :: xs) | (No noHead) with (isElem x xs)


If we have found the element later that is good.

      isElem x (y :: xs) | (No _) | (Yes prf)
= Yes (There prf)


Otherwise bail out with a ’localised’ proof that uses the evidence of why not to show why it will not work.

      isElem x (y :: xs) | (No noHead) | (No noTail)
= No neitherHereNorThere
where
neitherHereNorThere : IsElem x (y::xs) -> Void
neitherHereNorThere (Here prf)
neitherHereNorThere (There later)
= noTail later


So far so good. When using IsElem to build interactive programs we can present the truth when it holds, and contradictory evidence when it does not.

# Consider Truths about Association Lists

namespace Consider


Let us now examine another predicate: Given an association list can we state that:

1. a given key-value pair exists;
2. a key exists in the list;
3. a key’s value satisfies a given predicate.

We can describe these truths as instances of IsElem, custom predicates can also be used. The first truth is a straightforward aliasing.

  public export
IsKeyValue : (key     : typeKey)
-> (value   : typeValue)
-> (kvpairs : List (typeKey, typeValue))
-> Type
IsKeyValue key value kvpairs
= IsElem (key,value) kvpairs


The decision procedures for IsKeyValue is straightforward. Modulo some eta-reduction/expansion, isKeyValue is just an instance of isElem.

  export
isKeyValue : DecEq typeKey
=> DecEq typeValue
=> (key     : typeKey)
-> (value   : typeValue)
-> (kvpairs : List (typeKey, typeValue))
-> Dec (IsKeyValue key value kvpairs)
isKeyValue key value = isElem (key,value)


The second (and third) truth requires us to use dependent pairs to present new evidence when constructing the proof.

  public export
IsKey : {typeValue : Type}
-> (key       : typeKey)
-> (kvpairs   : List (typeKey, typeValue))
-> Type
IsKey {typeValue} key kvpairs
= (value ** IsElem (key,value) kvpairs)


First we deal with the absurd case of empty lists.


Uninhabited (IsKey key Nil) where
uninhabited (MkDPair _ prf) with (prf)
uninhabited (MkDPair _ prf) | (Here _) _ impossible


With that we can now present the decision procedure.

  export
isKey : DecEq typeKey
=> DecEq typeValue
=> (key     : typeKey)
-> (kvpairs : List (typeKey, typeValue))
-> Dec (IsKey key kvpairs)


Remember, empty lists are absurd.

  isKey key []
= No absurd


When examining each element:

  isKey key ((key', v) :: xs) with (decEq key key')


If we have found it stop.

    isKey key ((key, v) :: xs) | (Yes Refl)
= Yes (MkDPair v (Here Refl))


Otherwise carry on until the end.

    isKey key ((key', v) :: xs) | (No noHead) with (isKey key xs)
isKey key ((key', v) :: xs) | (No noHead) | (Yes prf) with (prf)
isKey key ((key', v) :: xs) | (No noHead) | (Yes prf) | (MkDPair v' rest)
= Yes (MkDPair v' (There rest))
isKey key ((key', v) :: xs) | (No noHead) | (No no)
= No (\(v ** prf) => case prf of
(There later) => no (MkDPair v later))


The third truth needs a double nesting. As an aside once you start going two levels deep, you may want to consider rolling these truths as distinct datatypes rather than aliasing.

  public export
HoldsFor : {typeValue : Type}
-> (key       : typeKey)
-> (p         : typeValue -> Type)
-> (kvpairs   : List (typeKey, typeValue))
-> Type
HoldsFor key p kvpairs
= (value ** prf : p value ** IsElem (key,value) kvpairs)

  export
Uninhabited (HoldsFor k p Nil) where
uninhabited (MkDPair v rest) with (rest)
uninhabited (MkDPair v rest) | (MkDPair _ pE) with (pE)
uninhabited (MkDPair v rest) | (MkDPair _ pE) | (Here prf) impossible
uninhabited (MkDPair v rest) | (MkDPair _ pE) | (There later) impossible


When constructing the decision procedure for HoldsFor we also need to rely on an externally given decision procedure for the predicate that needs attesting to.

  export
holdsFor : {typeValue : Type}
-> {p         : typeValue -> Type}
-> DecEq typeKey
=> (key       : typeKey)
-> (f         : (value : typeValue) -> Dec (p value))
-> (kvpairs   : List (typeKey, typeValue))
-> Dec (HoldsFor key p kvpairs)


As always empty lists are absurd.

  holdsFor key f []
= No absurd


We know inspect each element in the list, and when we find a matching key we also check if v satisfies the given predicate.

  holdsFor key f ((key',v) :: xs) with (decEq key key')
holdsFor key f ((key,v) :: xs) | (Yes Refl) with (f v)


If the shoe fits!

      holdsFor key f ((key,v) :: xs) | (Yes Refl) | (Yes prf)
= Yes (MkDPair v (MkDPair prf (Here Refl)))


If not, then check else down the list, as we are dealing with lists not sets, so the key might be used elsewhere in the listdate: 2022-06-02-PosNeg.md —please don’t hate me it is the truth!

      holdsFor key f ((key,v) :: xs) | (Yes Refl) | (No noV) with (holdsFor key f xs)
holdsFor key f ((key,v) :: xs) | (Yes Refl) | (No noV) | (Yes (MkDPair v' (MkDPair pV pE)))
= Yes (MkDPair v' (MkDPair pV (There pE)))
holdsFor key f ((key,v) :: xs) | (Yes Refl) | (No noV) | (No noLater)
= No (\(v' ** pV ** pE) => case pE of
(Here Refl) => noV pV
(There later) => noLater (MkDPair v' (MkDPair pV later)))


The last truth is the truth!

    holdsFor key f ((key',v) :: xs) | (No noHere) with (holdsFor key f xs)
holdsFor key f ((key',v) :: xs) | (No noHere) | (Yes (MkDPair v' (MkDPair pV pE)))
= Yes (MkDPair v' (MkDPair pV (There pE)))

holdsFor key f ((key',v) :: xs) | (No noHere) | (No noLater)
= No (\(v' ** pV ** pE) => case pE of
(Here Refl) => noHere Refl
(There later) => noLater (MkDPair v' (MkDPair pV later)))


# It is all too Negative!

namespace Contradiction


So that last decision procedure was a bit of a mouthful. But let us now look at their use, especially in positive and negative cases. We will use the following data:

  export
examplePairs : List (String, Nat)
examplePairs
= zip ["a", "b", "c"]
[1,   2,   3]


## IsKeyValue

First we look at isKeyValue:

### Positive

λΠ> isKeyValue ("c",3) examplePairs
Yes (There (There (Here Refl)))


### Negative

λΠ> isElem ("d",3) examplePairs
No (neitherHereNorThere (String, Nat) (DecEq at Decidable.Equality.Core:9:1--13:48 (\x1,
x2 => decEq x1 x2)) ("d", 3) [("b", 2), ("c", 3)] (neitherHereNorThere (String,
Nat) (DecEq at Decidable.Equality.Core:9:1--13:48 (\x1, x2 => decEq x1 x2)) ("d", 3) [("c",
3)] (neitherHereNorThere (String,
Nat) (DecEq at Decidable.Equality.Core:9:1--13:48 (\x1, x2 => decEq x1 x2)) ("d", 3) [] absurd ("c",
3) (\x => ())) ("b", 2) (\x => ())) ("a", 1) (\x => ()))


## IsKey

Then isKey:

### Positive

λΠ> isKey "c" examplePairs
Yes (MkDPair 3 (There (There (Here Refl))))


### Negative

λΠ> isKey "d" examplePairs
No (\lamc => let MkDPair v prf = lamc
in let lamc = MkDPair v prf
in case prf of { Here Refl => noHead Refl ; There later => no (MkDPair v later) })


## HoldsFor

And finally, holdsFor:

### Positive

λΠ> holdsFor "b" (isGT 3) examplePairs
Yes (MkDPair 2 (MkDPair (LTESucc (LTESucc (LTESucc LTEZero))) (There (Here Refl))))


### Negative One

λΠ> holdsFor "f" (isGT 3) examplePairs
No (\lamc => let MkDPair v' (MkDPair pV pE) = lamc
in let lamc = MkDPair v' (MkDPair pV pE)
in case pE of
{ Here Refl => noHere Refl
; There later => noLater (MkDPair v' (MkDPair pV later))
})


### Negative Two

λΠ> holdsFor "b" (decEq 3) examplePairs
No (\lamc => let MkDPair v' (MkDPair pV pE) = lamc
in let lamc = MkDPair v' (MkDPair pV pE)
in case pE of
{ Here Refl => noHere Refl
; There later => noLater (MkDPair v' (MkDPair pV later))
})


The interesting cases happen to be the negative ones. If we examine these negative cases, we cannot tell easily why the decision failed. If we look at the definition of Dec this is obvious, we get a proof of void. This is a computation, and not data, something needs to budge.

# Being Informative

namespace Informative


We have been round the houses to describe the problem of using Dec but it is important to see the examples for real. If we think about Dec, it is actually a variant of the Maybe datatype, but carries the falsehood in the negative response. To help make error reporting more positive we need to allow our decision procedures a chance to say why as well as the contradiction/falsehood.

For this, I created a variant of Dec based on the Either datatype that returns the Right result or we are Left with an error message. This datatype I created is DecInfo, it is an informative Dec.

  public export
data DecInfo : (neg : Type)
-> (pos : Type)
-> Type
where


The positive case is the same as before.

      Yes : (prf : pos)
-> DecInfo neg pos


The negative case supports positive information to be presented.

      No : (prf : neg)
-> (no  : pos -> Void)
-> DecInfo neg pos


So how does this work in practice. Let us return to our HoldsFor example. The error cases are:

1. the list is empty;
2. The key is not a key; and
3. the value doesn’t satisfy the predicate.

We can provide a descriptive summary of these states, much like we describe error messages.

  namespace HoldsFor

public export
data HoldsForNot e
= NotAKey
| PredicateFails e


Note that we do not present the error state that the list is empty. Detecting if the list is empty of the key is not found is ambiguous. If the presented key is not found then we must have reached the end of the list, which means we have traversed the list to it’s end.

The descriptive information is parameterised with a type as if we are going to make holdsFor informative we better make the predicate over the value to.

  export
holdsFor : {typeValue : Type}
-> {p         : typeValue -> Type}
-> DecEq typeKey
=> (key       : typeKey)
-> (f         : (value : typeValue) -> DecInfo e (p value))
-> (kvpairs   : List (typeKey, typeValue))
-> DecInfo (HoldsForNot e)
(HoldsFor key p kvpairs)


We skip the body of the function and note that it does not differ from before, aside from use of the error messages to make the negative results more informative.

For the coming examples, it would be nice to embed non-informative results into DecInfo. We do so with embed.

  export
embed : { p : type -> Type}
-> (f  : (value : type) -> Dec (p value))
-> (value : type)
-> DecInfo () (p value)


Now returning to the examples for holdsFor:

## Positive

λΠ> holdsFor "b" (embed (isGT 3)) examplePairs
Yes (MkDPair 2 (MkDPair (LTESucc (LTESucc (LTESucc LTEZero))) (There (Here Refl))))


## Negative

λΠ> holdsFor "f" (embed (isGT 3)) examplePairs
No NotAKey (\lamc => let MkDPair v' (MkDPair pV pE) = lamc
in let lamc = MkDPair v' (MkDPair pV pE)
in case pE of
{ Here Refl => noHere Refl
; There later => noLater (MkDPair v' (MkDPair pV later))
})

λΠ> holdsFor "b" (embed (decEq 3)) examplePairs
No (PredicateFails ()) (\lamc => let MkDPair v' (MkDPair pV pE) = lamc
in let lamc = MkDPair v' (MkDPair pV pE)
in case pE of
{ Here Refl => noHere Refl
; There later => noLater (MkDPair v' (MkDPair pV later))
})


Our negative results are more informative, are more positive. This is great, we can have a bit more information as to why the negative cases are negative.

# Why should you care?

DecInfo is important as it supports better error message generation in a more verified setting. The example of an association list (i.e. key-value was no accident). I have written several well-typed-well-scoped DSLs in Idris, and their construction (i.e. elaboration/type checking/type synthesis) is made much more informative when using predicates and their decision procedures. I can write error messages; instead of saying: no!

To list a few concrete examples.

# Are we finished?

namespace Sufficiency


An interesting question arises to the soundness and completeness of DecInfo. We are mixing positive and negative evidence together, but in an unbalanced way. I was, originally, concerned with presenting descriptive error messages rather than being positively negative. The examples I have listed are primarily returning descriptive information.

Recently, Bob Atkey tweeted at me when I was shouting to the abyss that the majority of my toolkit contained Dec based decision procedures rather than DecInfo. A recent trend in Bob’s work has looked at being positively negative. More precisely:

  public export
Truth : Type
Truth
= (pos : Type **
neg : Type ** (pos -> neg -> Void))


That is we combine two positive things that when combine cancel each other out. From this Truth we can extract our DecInfo as:

  public export
DecInfo : Truth -> Type
DecInfo (MkDPair pos (MkDPair neg no))
= Either neg pos


One example being to reason about the order of natural numbers such that we can pair the greater than proof with the less than or equal proof.

First we provide the positive contradiction

  public export
prf : GT  x y
-> LTE x y
-> Void
prf (LTESucc z) (LTESucc w)
= prf z w


We then define the truth:

  public export
GT : (x,y : Nat) -> Truth
GT x y
= (GT  x y **
LTE x y ** prf)


et voila

  export
isGT : (x,y : Nat) -> DecInfo (GT x y)
isGT 0 0 = Left LTEZero
isGT 0 (S k) = Left LTEZero
isGT (S k) 0 = Right (LTESucc LTEZero)
isGT (S k) (S j) with (Sufficiency.isGT k j)
isGT (S k) (S j) | (Left x) = Left (LTESucc x)
isGT (S k) (S j) | (Right x) = Right (LTESucc x)


This is an interesting set up that needs more exploring before we roll it out into production. isGT is incredibly positive, almost bubbling with joy. However, I am intrigued over the lack of negativity. I would like to provide proofs of void, the classic form of negativity. My brain hasn’t quite fathomed how to do this, but I am interested in Bob’s work here and how I can put his theory into my practice.

# Can DecInfo be better?

namespace Better


Bob’s work is interesting. Whilst I still am thinking of how best to put his theory into practise, we can still use the idea of being positively negative to good use. For example, rather than ’embedding’ isGT into DecInfo let us rewrite it:

  export
isGT : (x,y : Nat)
-> DecInfo (LTE x y)
(GT  x y)
isGT 0 0
= No LTEZero succNotLTEzero
isGT 0 (S k)
= No LTEZero succNotLTEzero
isGT (S k) 0
= Yes (LTESucc LTEZero)

isGT (S k) (S j) with (Better.isGT k j)
isGT (S k) (S j) | (Yes prf)
= Yes (LTESucc prf)

isGT (S k) (S j) | (No prf no)
= No (LTESucc prf)
(no . fromLteSucc)


For more complex decision procedures we can also mix positive and negative information, and descriptive structures with positive and negative ones. The possibilities are interesting, and worth thinking about for making verified programs more interactive.

# Coda

I have used DecInfo for a while, and was prompted to write this up more properly in response to FancyTypes question: What do you like about programming with dependent-types?