Idris 中的异构键/值收集

Question

我刚刚开始编写异构键/值集合以更好地理解证明。这是我的代码：

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

我这里有两个问题：

1. 不知何故 Not (key = k) 不起作用，我可以插入重复的 键。
2. 如何为 Show 派生实例？全部放在哪里 显示...？ （可能是不可能的）

有什么想法吗？

Answer 1

好的，我终于能够根据 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

我还添加了另一个有用的函数：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