Как написать SortedMap K (Может быть, V) -> SortedMap KV?

Question

Есть ли простой способ перейти от SortedMap k (Maybe v) к SortedMap k v, не переходя в список и обратно?Nothings должны быть удалены, а Justs должны быть сохранены.

Answer 1

Я так не думаю, поскольку SortedMap не раскрывает свои конструкторы (это только export определение верхнего уровня).Судя по 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