Heterogeneous key/value collection in Idris

Question

I have just started programming a heterogeneous key/value collection to better understand proofs. Here is my code:

data Collection : Type where
  None : Collection
  Cons : {a : Type} ->
         (name : String) ->
         (value : a) ->
         Collection ->
         Collection

example : Collection
example = Cons "str" "tralala" (Cons {a = Int} "num" 1 None)

data AllValues : (p : a -> Type) -> Collection -> Type where
  First : AllValues p None
  Next  : p a => AllValues p col -> AllValues p (Cons {a} k v col)

printCollection : (col : Collection) -> {auto prf : AllValues Show col} -> String
printCollection None {prf = First} = "."
printCollection (Cons key value rest) {prf = (Next later)} =
  "(" ++ key ++ ": " ++ show value ++ "), " ++ printCollection rest

--------------------------------------------------------------------------------
data IsNewKey : (key : String) -> Collection -> Type where
  U1 : IsNewKey key None
  U2 : Not (key = k) => IsNewKey key col -> IsNewKey key (Cons k value col)

insert : {a : Type} ->
         (name : String) ->
         (value : a) ->
         {auto notIn : IsNewKey name col} ->
         (col : Collection) ->
         Collection
insert {a} name value col = Cons {a} name value col

data IsElement : String -> Collection -> Type where
  Here  : IsElement key (Cons key value rest)
  There : (later : IsElement key rest) -> IsElement key (Cons name value rest)

update : (key : String) ->
         (newVal : ty) ->
         (col : Collection) ->
         {auto prf : IsElement key col} ->
         Collection
update key newVal (Cons key _ rest) {prf = Here} = Cons key newVal rest
update key newVal (Cons name value rest) {prf = (There later)} =
  Cons name value (update key newVal rest)

GetType : (key : String) -> (col : Collection) -> {auto prf : IsElement key col} -> Type
GetType key (Cons {a} key _ _) {prf = Here} = a
GetType key (Cons _ _ rest) {prf = There later} = GetType key rest

get : (key : String) -> (col : Collection) -> {auto prf : IsElement key col} -> GetType key col
get key (Cons key value _) {prf = Here} = value
get key (Cons _ _ rest) {prf = There later} = get key rest

I have two problems here:

1. Somehow Not (key = k) does not work, I am able to insert duplicated keys.
2. How to derive an instance for the Show? Where to put All Show...? (Probably it is not possible)

Any ideas?

Answer 1

OK, finally I was able to fix insert function with an advice from michaelmesser.

getKeys : Collection -> List String
getKeys None = []
getKeys (Cons name _ rest) = name :: getKeys rest

fromFalse : (d : Dec p) -> {auto isFalse : decAsBool d = False} -> Not p
fromFalse (Yes _) {isFalse = Refl} impossible
fromFalse (No contra) = contra

data NotEq : a -> a -> Type where
    MkNotEq : {a : t} -> {b : t} -> Not (a = b) -> NotEq a b

%hint
notEq : DecEq t => {a : t} -> {b : t} -> {auto isFalse : decAsBool (decEq a b) = False} -> NotEq a b
notEq = MkNotEq (fromFalse (decEq _ _))

insert : {a : Type} ->
         (name : String) ->
         (value : a) ->
         (col : Collection) ->
         {auto prf : All (NotEq name) (getKeys col)} ->
         Collection
insert {a} name value col = Cons {a} name value col

I also added another useful functions: delete, decompose, hasKey, upsert.

infixr 7 .::
(.::) : (String, a) -> (col : Collection) -> Collection
(.::) (name, value) col = Cons name value col

delete : (key : String) ->
         (col : Collection) ->
         {auto prf : IsElement key col} ->
         Collection
delete key (Cons key _ rest) {prf = Here} = rest
delete key (Cons name value rest) {prf = (There later)} =
  Cons name value (delete key rest)

HeadType : Collection -> Type
HeadType None = Maybe ()
HeadType (Cons {a} _ _ _) = a

data NotEmpty : Collection -> Type where
  MkNotEmpty : NotEmpty (Cons k v r)

decompose : (col : Collection) -> {auto prf : NotEmpty col} -> (HeadType col, Collection)
decompose (Cons k v r) {prf = MkNotEmpty} = (v, r)

notInNone : IsElement key None -> Void
notInNone Here impossible
notInNone (There _) impossible

notInTail : (notThere : IsElement key rest -> Void) ->
            (notHere : (key = name) -> Void) ->
            IsElement key (Cons name value rest) -> Void
notInTail _ notHere Here = notHere Refl
notInTail notThere _ (There later) = notThere later

hasKey : (key : String) -> (col : Collection) -> Dec (IsElement key col)
hasKey key None = No notInNone
hasKey key (Cons name value rest) =
  case key `decEq` name of
    Yes Refl => Yes Here
    No notHere =>
        case hasKey key rest of
          Yes later => Yes (There later)
          No notThere => No (notInTail notThere notHere)

upsert : {a : Type} ->
         (name : String) ->
         (value : a) ->
         (col : Collection) ->
         Collection
upsert name value col =
  case hasKey name col of
    Yes _ => update name value col
    No _  => (name, value) .:: col