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
```

Let us examine the head.

```
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)
= noHead 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:

- a given key-value pair exists;
- a key exists in the list;
- 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
(Here Refl) => noHead Refl
(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:

- the list is empty;
- The key is not a key; and
- 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.

## Libraries

`DeBruijn`

is part of my toolkit for working with intrinsically typed terms in Idris. I use`DecInfo`

when: testing predicates over items in the typing context; traversing over the typing context- Quantifiers over Collections. It is good to know how many satisfied items there are in a list when there should only be a certain amount; and if we expect all items in a list to satisfy a predicate (useful for reasoning about the degrees of vertices in a graph) and what was the location of the first dissenting element. Naturally, this works for vectors too, and quantifiers over quantifiers.

## Projects

`LightClick`

I have used`DecInfo`

to present more meaningful errors when reasoning about connecting ports together. This is used in the project’s typechecker to check the connections and to lookup items in a stateful typing context. This uses an older version of`DeBruijn`

. Not the ’throwing’ and reporting of errors is taken care of by a custom computation context`Linear Circuits`

is a project to reason about the wiring of NetLists (digital circuits). There are several little DSLs to explore ideas, and each of them uses`DecInfo`

in much the same way as`DeBruijn`

: To provide proofs for the intrinsically typed terms, and reason about the typing context using`DeBruijn`

. This project is on going, and I am rewriting the Linearly-wired language from the ground up so that the proofs about usage are fully informative and positively negative.`Olaf`

The plan is to convert the type-checking code to use`DecInfo`

where possible.

# 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?

We’ve seen the long answer, but the short answer is:

Being positively negative!