使用Agda标准库Data.Tree.AVL.Map的lookup函数遇类型错误求助

你遇到的问题核心是AVL Map模块中lookup函数的参数顺序和你预期的相反。你的代码中调用lookup singletonMap "test"时，Agda将singletonMap（类型为Map String）识别为Key类型（即String），这就导致了类型不匹配错误。

问题根源 #

你看到的简化类型签名可能误导了你，在Data.Tree.AVL.Map模块中，lookup的实际参数顺序是：先传入Key，再传入Map，而非你以为的Map V → Key → Maybe V。该模块的lookup真实类型为：

lookup : Key → Map V → Maybe V

修正后的代码 #

将lookup的参数顺序调换即可解决问题：

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 "test" singletonMap  -- 调换参数顺序：Key在前，Map在后

补充说明 #

Data.Tree.AVL.Map的设计遵循了Agda标准库中部分函数的常见参数顺序——将查询用的Key放在前面，这样更便于进行柯里化和函数组合。

内容的提问来源于stack exchange，提问作者Stack Overflow User