Idris 中的异构键/值集合

如何解决Idris 中的异构键/值集合

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

const remainingData = contacts.filter(item => item.contact_id !== data.contact_id)

我有两个问题：

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

有什么想法吗？

解决方法

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

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