Idris

Question

我有一个 Idris 模块，它定义了某个 type/predicate IsSet 和一个可判定性函数 isSet。它还定义了一些辅助函数来计算类型检查时的可判定性函数，以获得 IsSet.

的证明

在模块内正确使用该辅助函数类型检查的表达式，但当我在另一个文件中定义它们并导入原始模块时却没有：

Test1.idr

module Test1

import Data.List

%default total
%access export

data IsSet : List t -> Type where
  IsSetNil : IsSet []
  IsSetCons : Not (Elem x xs) -> IsSet xs -> IsSet (x :: xs)

ifNotSetHereThenNeitherThere : Not (IsSet xs) -> Not (IsSet (x :: xs))
ifNotSetHereThenNeitherThere notXsIsSet (IsSetCons xIsInXs xsIsSet) = notXsIsSet xsIsSet  

ifIsElemThenConsIsNotSet : Elem x xs -> Not (IsSet (x :: xs))      
ifIsElemThenConsIsNotSet xIsInXs (IsSetCons notXIsInXs xsIsSet) = notXIsInXs xIsInXs

isSet : DecEq t => (xs : List t) -> Dec (IsSet xs)
isSet [] = Yes IsSetNil
isSet (x :: xs) with (isSet xs)
  isSet (x :: xs) | No notXsIsSet = No $ ifNotSetHereThenNeitherThere notXsIsSet
  isSet (x :: xs) | Yes xsIsSet with (isElem x xs)
    isSet (x :: xs) | Yes xsIsSet | No notXInXs = Yes $ IsSetCons notXInXs xsIsSet
    isSet (x :: xs) | Yes xsIsSet | Yes xInXs = No $ ifIsElemThenConsIsNotSet xInXs

getYes : (d : Dec p) -> case d of { No _ => (); Yes _ => p}
getYes (No _ ) = ()
getYes (Yes prf) = prf

getNo : (d : Dec p) -> case d of { No _ => Not p; Yes _ => ()}
getNo (No cnt) = cnt
getNo (Yes _ ) = ()

setTest1 : IsSet ["x"]
setTest1 = getYes $ isSet ["x"]

Test2.idr

module Test2

import Test1

%default total
%access export

setTest2 : IsSet ["x"]
setTest2 = getYes $ isSet ["x"]

setTest1 类型检查正确，但 setTest2 抛出以下错误：

When checking right hand side of setTest2 with expected type
         IsSet ["x"]

 Type mismatch between
         case block in getYes at Test1.idr:26:30 (IsSet ["x"])
                                                 (isSet ["x"])
                                                 (isSet ["x"]) (Type of getYes (isSet ["x"]))
 and
         IsSet ["x"] (Expected type)

我正在使用 Idris 0.12

Answer 1

当类型检查 Test2.idr 时，类型检查器不知道定义（而不仅仅是类型）isSet，因此它不能减少 getYes 的类型签名，因此类型不匹配。为了使其工作，您必须 public export 函数 isSet。由于 Idris 的可见性规则，您还必须至少 public export IsSet 类型，因为 isSet 引用其（当前未导出）定义。

无论如何，这可能是个好主意，因为没有它，即使是像

这样的简单函数也不行

isNil : IsSet l -> Bool
isNil IsSetNil = True
isNil (IsSetCons f y) = False

in Test2.idr 会起作用，因为该模块不知道类型的定义，即数据构造函数。

Idris - 从模块导入时表达式不进行类型检查

Idris - Expression doesnt typecheck when imported from module

unification

type-level-computation