idris proofs: a tale of alists with guaranteed unique values and a bunch of misc

I wanted alists with guaranteed unique values, and finally decided to sit down and work out how this functions in idris. For those not as old as dirt, an alist in lisp is a list of pairs where the (car) of each is considered to be the key, so it functions like Dict or Map in most languages (functions like assoc and mem in lisp act on these). I’m not aware of any library providing this functionality in idris, even though it’s useful for a lot of things (for example, many json formats use a list of objects with a name field each to reduce duplication in json, but they must be unique names).

Things one can learn from this:

• How to actually use absurd.
• How to use the “No contra” result from DecEq in a with rule.
• How to use Idris’ DPair.

module Data.AList
import Data.Bool
import Decidable.Equality
keyInList : Eq a => a -> List (Pair a b) -> Bool
keyInList k [] = False
keyInList k ((k1, v1) :: others) =
  if k == k1 then
    True
  else
    keyInList k others
allKeysUniqueInList : Eq a => List (Pair a b) -> Bool
allKeysUniqueInList [] = True
allKeysUniqueInList ((k, v) :: others) =
 let
   headIsUnique = not (keyInList k others)
   tailsAreUnique = allKeysUniqueInList others
 in
 tailsAreUnique && headIsUnique
kvCons : a -> b -> List (Pair a b) -> List (Pair a b)
kvCons k v l = (k,v) :: l
appendBreak : Eq a => (k : a) -> (v : b) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True))
appendBreak k v l p with (decEq (keyInList k l) True)
  appendBreak k v l p | Yes prf = (l ** p)
  appendBreak k v l p | No contra =
    let
      cproof = invertContraBool (keyInList k l) True contra
    in
    (kvCons k v l ** outProof k l p cproof)
    where
      outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
      outProof k l p kp =
        rewrite kp in
        rewrite p in
        Refl
public export
proveList : Eq a => (l : List (Pair a b)) -> Maybe (DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True))
proveList l with (decEq (allKeysUniqueInList l) True)
  proveList l | Yes prf = Just (l ** prf)
  proveList l | No _ = Nothing
public export
addIfUnique : Eq a => (k : a) -> (v : b) -> (l : DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True)) -> DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True)
addIfUnique k v (l ** p) = appendBreak k v l p

Supported by a function I’ve PR’d for Data.Bool: invertContraBool

---------------------------------------
-- Decidability specialized on bool
---------------------------------------
||| You can reverse decidability when bool is involved.
-- Given a contra on bool equality (a = b) -> Void, produce a proof of the opposite (that (not a) = b)
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool False False contra = absurd $ contra Refl
invertContraBool False True contra = Refl
invertContraBool True False contra = Refl
invertContraBool True True contra = absurd $ contra Refl

Something I’ve been confused by for a while is how to get any utility out of contra. Usually it’s taunting me with a function taking an impossible proof and yielding Void, but what can I actually do with that? What does it solve?

I think the use of the absurd could use concrete explanation here:

Idris’ documentation for Prelude.Uninhabited, including the “absurd” function and Uninhabited typeclass.

Reading these words, I thought I understood it, but didn’t really get what idris was doing mechanically, then I finally decided to look over every use I could see of absurd and try to see what they were doing. Ultimately, the important thing is that absurd is like idris_crash in that its result is an unpaired ‘a’ type variable so it can satisfy the result of any function, but more importantly, mechanically it is passing on the property of unhabitation to the thing that uses it, erasing the need to return a result for some case.

Since contra is a function taking a proof, if we can supply it with that proof, we can get a Void to plug into absurd:

public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool False False contra = absurd $ contra Refl

Or more elaborately to show what’s happening:

public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool a b contra = invertContraBool_ a b contra
  where
    fEf : False = False
    fEf = Refl
    tEt : True = True
    tEt = Refl
    invertContraBool_ : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
    invertContraBool_ False False contra = absurd (contra fEf)
    invertContraBool_ False True contra = Refl
    invertContraBool_ True False contra = Refl
    invertContraBool_ True True contra = absurd (contra tEt)

Since contra is the contradiction of a proof that a = b, a proof that a = b (such as True = True) when a and b are True, satisfies it and gives us the Void object, which we can use with absurd to satisfy this case (return a) without really knowing how. Idris knows that this code is unreachable due to absurd being satisfied.

So how do you use invertContraBool?

Take a look at appendBreak in the code (I use ‘break’ or ‘broken’ often to mean ‘with arguments separated out’)

appendBreak : Eq a => (k : a) -> (v : b) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True))
appendBreak k v l p with (decEq (keyInList k l) True)
  appendBreak k v l p | Yes prf = (l ** p)
  appendBreak k v l p | No contra =
    let
      cproof = invertContraBool (keyInList k l) True contra
    in
    (kvCons k v l ** outProof k l p cproof)
    where
      outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
      outProof k l p kp =
        rewrite kp in
        rewrite p in
        Refl

We’re building a dependent pair (more on that in a moment) that contains the list and a function yielding a proof about a list, and we start with the opposite of any kind of proof. In our case the only information we have is that we can use absurd if keyInList k l = True. Even worse, we already know that it isn’t, so this contra function would appear to be totally useless most of the time, when we’re dealing with concrete data.

Since Bool has only 2 values though, we can enumerate all the cases and show idris that the only sensible result is that a and b aren’t equal (since we have a function that shows idris that it can ignore the idea that they could be) and therefore show that the other cases work to show not a = b. The function is total and we haven’t missed any cases, therefore I believe this proof is sound.

So now, starting with the mess of a = b -> Void, we have the more useful (not a = b), which we capture here into

cproof : not (keyInList k l) = True
cproof = invertContraBool (keyInList k l) True contra

And from there, we can figure out a way to write the proof that the new list also has unique keys:

outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
      outProof k l p kp =
        rewrite kp in
        rewrite p in
        Refl

Using the very proof we were able to get, not (keyInList k l) = True

We rewrite with that and the proof given with the original list, that all its keys were unique and satisfy allKeysUniqueInList:

allKeysUniqueInList ((k, v) :: others) =
 let
   headIsUnique = not (keyInList k others)
   tailsAreUnique = allKeysUniqueInList others
 in
 tailsAreUnique && headIsUnique

Now is the time to discuss how to use DPair. It has mechanics that are complicated and so in my view, situational.

What I found was that Idris is able to understand simple constructions using ** in types:

proofPair : (v : a) -> (f : a -> Bool) -> (p : f v = True) -> (v ** f v = True)
proofPair v f p = MkDPair v p

Idris definitely DWIM here:

λΠ> :t proofPair
Data.AList.proofPair : (v : a) -> (f : (a -> Bool)) -> f v = True -> DPair a (\v => f v = True)

But other times I struggled to write the expression I wanted into the type, getting all sorts of generic-y errors. When this happens, declare the type more formally:

DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True)

You can use the ** data constructor to either pick apart a dpair (or you can name the constructor with MkDPair

addIfUnique k v (l ** p) = appendBreak k v l p -- Good
addIfUnique k v (MkDPair l p) = appendBreak k v l p-- also good

And you can of course construct them either way at runtime:

public export
proveList : Eq a => (l : List (Pair a b)) -> Maybe (DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True))
proveList l with (decEq (allKeysUniqueInList l) True)
  proveList l | Yes prf = Just (l ** prf) -- (MkDPair l prf) works too
  proveList l | No _ = Nothing