What's the type for Dictionary/Map in Idris

Question

How can I define one? I've not found any information about the matter in the documentation. Only about List and Vector.

Answer 1

Data.SortedMap in the contrib package implements finite maps for types that have an Ord instance, with the usual interface:

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)