theorem-proving - idris中类型计算函数结果的模式匹配

Question

考虑以下片段:

import Data.List

%default total

x : Elem 1 [1, 2]
x = Here

type : Type
type = Elem 1 [1, 2]

y : type
y = Here

这给出了错误:

检查 y 的右侧时:之间的类型不匹配 Elem x (x::xs) (此处的类型)和 iType(预期类型)

查询时y的类型为:

type : Type
-----------
y : type

是否可以强制type在y的类型归属期间或之前进行评估，以便y的类型为Elem 1 [1, 2]？

我的用例是我希望能够定义通用谓词来返回正确的证明命题项，例如:

subset : List a -> List a -> Type
subset xs ys = (e : a) -> Elem e xs -> Elem e ys

thm_filter_subset : subset (filter p xs) xs

Answer 1

类型声明中以小写字母开头的名称是隐式绑定(bind)的，因此它将“type”视为类型参数。您可以给“键入”一个以大写字母开头的新名称(按照惯例，这是大多数人在 Idris 中所做的)，或者您可以使用它所在的模块显式限定该名称(此处为 Main)。

Idris 过去常尝试猜测诸如“type”之类的名称是隐含的还是指全局的，如此处所示。不过，要实现这一点需要用到各种各样的巫术，所以它经常失败，所以它现在实现了这个更简单的规则。在这种情况下，这有点烦人，但替代行为通常更烦人(并且更难以解释)。