Idris中map查找未化简问题及编译时验证键值对方法咨询

为什么函数调用没被自动化简？ #

你遇到的问题本质上是Idris类型检查器的化简逻辑导致的：虽然我们从逻辑上知道lookup "a" (fromList [("a", Nat), ("b", String)])的结果肯定是Just Nat，但Idris默认不会在类型检查阶段主动展开并计算这类函数组合的结果。

具体来说，fromList和lookup都属于运行时可计算的函数，但它们没有被标记为编译期自动化简的函数（比如没有%inline注解，也没有内置的重写规则让类型检查器直接推导结果）。所以类型检查器只会把lookup "a" N当作一个未求值的表达式，不会自动把它替换成Just Nat，这就导致了Refl的类型（Just Nat = Just Nat）和预期的类型（lookup "a" N = Just Nat）不匹配。

如何在编译时验证SortedMap包含指定键值对？ #

要让类型检查器认可这个等式，我们需要用Idris的证明机制来明确建立lookup "a" N和Just Nat的相等关系，这里有几种可行的方法：

方法1：用with语句解构查询结果 #

通过解构lookup的返回值，我们可以直接在匹配到Just Nat的分支里用Refl证明等式，同时排除不可能的Nothing分支：

import Data.SortedMap

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

t : lookup "a" N = Just Nat
t with (lookup "a" N)
  t | Just Nat = Refl
  t | Nothing = void (believe_me ())  -- 这个分支逻辑上不可能，用believe_me跳过类型检查

方法2：编写辅助引理并使用重写 #

如果你需要多次验证类似的键值对，可以先编写一个通用的引理，再用rewrite来应用它：

import Data.SortedMap

lookup_fromList_singleton : (k : String) -> (v : Type) -> lookup k (fromList [(k, v)]) = Just v
lookup_fromList_singleton k v = Refl

-- 对于包含多个键值对的场景，可扩展引理逻辑
lookup_a_N : lookup "a" (fromList [("a", Nat), ("b", String)]) = Just Nat
lookup_a_N = rewrite lookup_fromList_singleton "a" Nat in Refl

方法3：使用believe_me快速确认（谨慎使用） #

如果你已经通过REPL的compute命令确认lookup "a" N的结果确实是Just Nat，可以用believe_me直接让类型检查器接受这个等式（注意：该操作会跳过类型检查，仅在逻辑绝对正确时使用）：

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

内容的提问来源于stack exchange，提问作者michaelmesser