CODEWITHSUNDEEP
agdaagda-stdlib
xbreu
xbreu

Reputation: 65

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.

Upvotes: 1

Views: 130

Answers (1)

gallais
gallais

Reputation: 12113

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).

Upvotes: 2

Related Questions