agdaagda-stdlib

lookup using Maps from Data.Tree.AVL.Map in Agda

I don't understand how to use the provided Map from Stdlib. I tried creating a Map from String to String, and it worked, but whenever I try using the lookup function I get weird errors:

This is a simplification of my code:

open import Data.Maybe
open import Data.String
open import Data.String.Properties
open import Data.Tree.AVL.Map (<-strictTotalOrder-≈) using (Map ; singleton ; lookup)

singletonMap : Map String
singletonMap = singleton "test" "a"

test : Maybe String
test = lookup singletonMap "test"

I get the following error:

(Data.Tree.AVL.Tree <-strictTotalOrder-≈
 (Data.Tree.AVL.Value.const
  (Relation.Binary.Bundles.StrictPartialOrder.Eq.setoid
   (Relation.Binary.Bundles.StrictTotalOrder.strictPartialOrder
    <-strictTotalOrder-≈))
  String))
!=< String
when checking that the expression singletonMap has type
Relation.Binary.Bundles.StrictTotalOrder.Carrier
<-strictTotalOrder-≈

I'm having trouble trying to even understand what's happening, it looks like lookup is not expecting an argument like singletonMap, because the types do not match, but how can that be possible? I created it using singleton, and the functions have the following types (they can be seen in Data.Tree.AVL.Map as well):

singleton : Key → V → Map V

lookup : Map V → Key → Maybe V

They are literally the same.

Solution

  • You're linking to the documentation of the current dev version. In older, released versions, lookup takes the key first, and the Map second. You should write

    test : Maybe String
test = lookup "test" singletonMap

    The dev version is gearing up to release a version 2.0 with breaking changes in the name of uniformity (all lookups will now have a type of the form Container -> Key -> Val because the type of keys may depend on the type of the container, but not the other way around).