在伊德里斯看似矛盾的说法

Question

我有一个关于向量的谓词的以下定义,它确定一个是否是一个集合(没有重复的元素).我用类型级布尔值定义成员资格:

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 xstypecheck上匹配？

更令人困惑的是,类似下面的类型检查:

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

根据上面的IsSet和ElemBool的定义,这似乎是一个矛盾.exampleidris评估的值如下:

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]一个案例块？我%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)

由于并非所有Vects都可以设置,因此需要返回a Maybe.可悲的是,它不能返回更精确的东西,比如Dec (IsSet xs)因为你使用布尔相等Eq而不是通过可判断的相等,DecEq但也许这就是你想要的你的版本集.