Idris编译器能否隐式查找证明？及带证明的字典取值函数问题

嗨，我来帮你搞定这个Idris依赖类型编程的问题，正好在这类场景上有不少实践经验～

首先先补全你没贴的基础定义（应该和你想的差不多），先定义字典类型和键存在的证明谓词：

-- 字典类型：schema是(String, Type)的列表，描述每个键对应的类型
data Dict : List (String, Type) -> Type where
  Empty : Dict []
  Insert : (key : String) -> (val : ty) -> Dict rest -> Dict ((key, ty) :: rest)

-- 证明某个键存在于schema中的谓词
data HasKey : String -> List (String, Type) -> Type where
  Here : HasKey key ((key, ty) :: rest)  -- 键在当前列表头部
  There : HasKey key rest -> HasKey key ((other, ty) :: rest)  -- 键在列表剩余部分

接下来就可以写安全的检索函数了，把HasKey作为参数，确保调用时键一定存在：

lookup : (key : String) -> (dict : Dict schema) -> HasKey key schema -> ty
lookup key (Insert key val rest) Here = val
lookup key (Insert other val rest) (There prf) = lookup key rest prf

这里Idris会自动根据HasKey的证明推断出返回值的ty，完全保证类型安全。

答案是当然可以，但需要借助Idris的自动隐式机制，具体可以这么做：

1. 把证明设为自动隐式参数 #

修改lookup函数，用{auto prf : ...}把证明参数标记为自动推导：

lookup : (key : String) -> (dict : Dict schema) -> {auto prf : HasKey key schema} -> ty
lookup key (Insert key val rest) {prf = Here} = val
lookup key (Insert other val rest) {prf = There prf} = lookup key rest

现在调用的时候，只要编译器能通过上下文推断出键确实存在，就不用手动传证明了。比如你构造了一个带"name"键的字典：

myDict : Dict [("name", String), ("age", Nat)]
myDict = Insert "name" "Alice" (Insert "age" 30 Empty)

直接调用lookup "name" myDict，编译器会自动找到Here的证明；调用lookup "age" myDict，会自动找到There Here的证明，完全不用你手动写。

2. 复杂场景下的自动证明 #

如果键的存在不是静态可推断的（比如依赖运行时输入），编译器没办法自动构造证明，这时候可以写一个可判定性函数，让编译器在运行时判断键是否存在：

-- 判定某个键是否存在于schema中，返回Dec（可判定结果）
decHasKey : (key : String) -> (schema : List (String, Type)) -> Dec (HasKey key schema)
decHasKey key [] = No (\prf => case prf of {})  -- 空列表肯定不存在
decHasKey key ((k, ty) :: rest) =
  if key == k
    then Yes Here  -- 当前键匹配，返回存在证明
    else case decHasKey key rest of
           Yes prf => Yes (There prf)  -- 剩余部分存在，包装成There证明
           No contra => No (\Here => contra Here; (There prf) => contra prf)  -- 剩余部分不存在，构造否定证明

有了这个函数，你就可以在运行时处理不确定的键，比如：

handleLookup : String -> Dict schema -> Maybe ty
handleLookup key dict =
  case decHasKey key schema of
    Yes prf => Just (lookup key dict prf)
    No _ => Nothing

总的来说，Idris的自动证明查找对简单的静态场景非常友好，复杂场景则需要你提供可判定性函数来辅助编译器。

内容的提问来源于stack exchange，提问作者Rafael S. Calsaverini