时间戳

首页 > 解决方案 > 伊德里斯没有减少地图查找

idris - 伊德里斯没有减少地图查找

问题描述

为什么不减少函数调用？如何在编译时验证映射是否包含键值对？

import Data.SortedMap

N : SortedMap String Type
N = fromList
    [ ("a", Nat)
    , ("b", String)
    ]

t : lookup "a" N = Just Nat
t = Refl

Type mismatch between
        Just Nat = Just Nat (Type of Refl)
and
        lookup "a" (fromList [("a", Nat), ("b", String)]) = Just Nat (Expected type)

Specifically:
        Type mismatch between
                Just Nat
        and
                lookup "a" (fromList [("a", Nat), ("b", String)])

标签： idris

解决方案

它必须与SortedMap使用普通List工作的版本的实现有关：

N : List (String, Type)
N =
    [ ("a", Nat)
    , ("b", String)
    ]

t : lookup "a" N = Just Nat
t = Refl

根据文档Data.SortedMap.lookup也是总数，所以它应该减少。可能原因是其中的函数和数据类型SortedMap似乎具有导出限定符，而 Data.List 中的函数和数据类型使用public export.

推荐阅读