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!

idris dependent-types