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

以小写字母开头的类型声明中的名称是隐式绑定的,因此它将'type'视为类型参数.您可以为'type'指定一个以大写字母开头的新名称(按照惯例,这是大多数人在Idris中所做的事情),或者您可以使用其所在的模块(Main,here)明确限定名称.

Idris过去曾试图猜测像"类型"这样的名称是否意图隐含或意图引用全局,如此处所示.尽管如此,还是有各种各样的伏都教,所以它经常失败,所以它现在实现了这个更简单的规则.在这种情况下,这有点令人讨厌,但替代行为更令人讨厌(并且更难解释).