什麼是Idris字典/地圖的類型

Question

我該如何定義一個？我沒有在文檔中找到有關此事的任何信息。只關於List和Vector。

Answer 1

在contrib包Data.SortedMap實現了有一個Ord實例類型有限的地圖，與通常的接口：

data SortedMap : Type -> Type -> Type 

empty : Ord k => SortedMap k v 
lookup : k -> SortedMap k v -> Maybe v 
insert : k -> v -> SortedMap k v -> SortedMap k v 
delete : k -> SortedMap k v -> SortedMap k v 

fromList : Ord k => List (k, v) -> SortedMap k v 
toList : SortedMap k v -> List (k, v) 

implementation Functor (SortedMap k)