# 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.AListimport Data.Boolimport Decidable.EqualitykeyInList : Eq a => a -> List (Pair a b) -> BoolkeyInList k [] = FalsekeyInList k ((k1, v1) :: others) =  if k == k1 then    True  else    keyInList k othersallKeysUniqueInList : Eq a => List (Pair a b) -> BoolallKeysUniqueInList [] = TrueallKeysUniqueInList ((k, v) :: others) = let   headIsUnique = not (keyInList k others)   tailsAreUnique = allKeysUniqueInList others in tailsAreUnique && headIsUniquekvCons : a -> b -> List (Pair a b) -> List (Pair a b)kvCons k v l = (k,v) :: lappendBreak : 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        Reflpublic exportproveList : 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 _ = Nothingpublic exportaddIfUnique : 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 exportinvertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)invertContraBool False False contra = absurd \$ contra ReflinvertContraBool False True contra = ReflinvertContraBool True False contra = ReflinvertContraBool 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 exportinvertContraBool : (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 exportinvertContraBool : (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) = Truecproof = 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 proofPairData.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 -- GoodaddIfUnique k v (MkDPair l p) = appendBreak k v l p-- also good`

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

`public exportproveList : 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`

An old programmer learning new tricks.

## More from art yerkes

An old programmer learning new tricks.