如何编写 SortedMap k (Maybe v) -> SortedMap k v？

【问题标题】：How to write SortedMap k (Maybe v) -> SortedMap k v?如何编写 SortedMap k (Maybe v) -> SortedMap k v？
【发布时间】：2019-05-05 04:04:55
【问题描述】：

有没有一种简单的方法可以从SortedMap k (Maybe v) 到SortedMap k v 而无需列出并返回？什么都应该删除，Justs应该保留。

【问题讨论】：

标签： idris

【解决方案1】：

我不这么认为，因为SortedMap 没有公开它的构造函数（它只是exporting 顶级定义）。从 API 的角度来看，似乎转换为列表并返回是要走的路。

export
data SortedMap : Type -> Type -> Type where
  Empty : Ord k => SortedMap k v
  M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v

【讨论】：