# 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.Bool

import Decidable.EqualitykeyInList : Eq a => a -> List (Pair a b) -> Bool

keyInList k [] = False

keyInList k ((k1, v1) :: others) =

if k == k1 then

True

else

keyInList k othersallKeysUniqueInList : Eq a => List (Pair a b) -> Bool

allKeysUniqueInList [] = True

allKeysUniqueInList ((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 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 _ = Nothingpublic 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:

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