proof - Idris 中看似矛盾的类型检查

Question

我对向量谓词有以下定义，用于标识一个集合是否为集合(没有重复元素)。我使用类型级 bool 值定义成员资格:

import Data.Vect

%default total

data ElemBool : Eq t => t -> Vect n t -> Bool -> Type where
  ElemBoolNil : Eq t => ElemBool {t=t} a [] False
  ElemBoolCons : Eq t => ElemBool {t=t} x1 xs b -> ElemBool x1 (x2 :: xs) ((x1 == x2) || b)

data IsSet : Eq t => Vect n t -> Type where
  IsSetNil : Eq t => IsSet {t=t} []
  IsSetCons : Eq t => ElemBool {t=t} x xs False -> IsSet xs -> IsSet (x :: xs)

现在我定义了一些允许我创建这个谓词的函数:

fun_1 : Eq t => (x : t) -> (xs : Vect n t) -> (b : Bool ** ElemBool x xs b)
fun_1 x [] = (False ** ElemBoolNil)
fun_1 x1 (x2 :: xs) = 
  let (b ** prfRec) = fun_1 x1 xs
  in (((x1 == x2) || b) ** (ElemBoolCons prfRec))  

fun_2 : Eq t => (xs : Vect n t) -> IsSet xs 
fun_2 [] = IsSetNil
fun_2 (x :: xs) = 
    let prfRec = fun_2 xs
        (False ** isNotMember) = fun_1 x xs
    in IsSetCons isNotMember prfRec

fun_1 的工作方式类似于 ElemBool 上的决策过程。

我的问题是 fun_2。为什么 (False ** isNotMember) = fun_1 x xs 上的模式匹配会进行类型检查？

更令人困惑的是，还有类似以下类型检查的内容:

example : IsSet [1,1]
example = fun_2 [1,1]

根据上面 IsSet 和 ElemBool 的定义，这似乎是矛盾的。example idris 计算的值如下:

case block in fun_2 Integer
                    1
                    1
                    [1]
                    (constructor of Prelude.Classes.Eq (\meth =>
                                                          \meth =>
                                                            intToBool (prim__eqBigInt meth
                                                                                      meth))
                                                       (\meth =>
                                                          \meth =>
                                                            not (intToBool (prim__eqBigInt meth
                                                                                           meth))))
                    (IsSetCons ElemBoolNil IsSetNil)
                    (True ** ElemBoolCons ElemBoolNil) : IsSet [1, 1]

这是有意为之的行为吗？还是自相矛盾？为什么 IsSet [1,1] 类型的值是 case block ？我在文件顶部有 %default total 注释，所以我认为它与偏袒没有任何关系，对吧？

注意:我使用的是 Idris 0.9.18

Answer 1

覆盖率检查器中存在一个错误，这就是此类型检查的原因。它将在 0.9.19 中修复(这是一个微不足道的问题，由内部依赖对构造函数的名称更改引起，由于某种原因，直到现在才被忽视，所以感谢你提醒我!)

无论如何，我按如下方式实现了fun_2:

fun_2 : Eq t => (xs : Vect n t) -> Maybe (IsSet xs)
fun_2 [] = Just IsSetNil
fun_2 (x :: xs) with (fun_1 x xs)
  fun_2 (x :: xs) | (True ** pf) = Nothing
  fun_2 (x :: xs) | (False ** pf) with (fun_2 xs)
    fun_2 (x :: xs) | (False ** pf) | Nothing = Nothing
    fun_2 (x :: xs) | (False ** pf) | (Just prfRec)
        = Just (IsSetCons pf prfRec)

因为不是所有的Vect都可以被设置，这需要返回一个Maybe。可悲的是，它不能返回更精确的东西，比如 Dec (IsSet xs) 因为你使用的是通过 Eq 的 bool 相等性，而不是通过 DecEq 的可判定相等性 但也许这就是您想要的集合版本。