Idris - 基于可判定属性的类型计算不进行类型检查答案

【问题标题】：Idris - Computation on types based on decidable property doesn't typecheckIdris - 基于可判定属性的类型计算不进行类型检查
【发布时间】：2015-09-28 04:12:11
【问题描述】：

我在 Idris 中遇到了一个问题，我想在其中创建一个基于可判定属性的类型级“检查”，如果该属性成立，我会得到我想要的类型，但如果属性失败，我会得到 @ 987654321@ (())，表示程序处于不一致状态（如果我决定将其用作我的原始类型，则不应编译）。

这是一个例子：

TestType : {k : Nat} -> Nat -> Vect k Nat -> Type
TestType n ls with (isElem n ls)
  TestType n ls | Yes _ = Nat
  TestType n ls | No _ = ()

mkTestTypeFromNat : (n : Nat) -> (ls : Vect k Nat) -> Elem n ls -> Nat -> TestType {k=k} n ls
mkTestTypeFromNat n ls prf res = res

mkTestTypeFromUnit : (n : Nat) -> (ls : Vect k Nat) -> Not (Elem n ls) -> TestType {k=k} n ls
mkTestTypeFromUnit n ls prf = ()

当我尝试编译它时，它显示了以下错误：

When checking right hand side of mkTestTypeFromNat:
Type mismatch between
           Nat (Type of n)
   and
           with block in Extensible_Records.TestType n
                                                     k
                                                     ls
                                                     (isElem n ls) (Expected type)

When checking right hand side of mkTestTypeFromUnit:
Type mismatch between
           () (Type of ())
   and
           with block in Extensible_Records.TestType n
                                                     k
                                                     ls
                                                     (isElem n ls) (Expected type)

在每个mkTestTypeFrom_ 函数中，我提供了可判定属性的证明，要么证明元素在列表中，要么证明它不在。类型检查器不应该意识到它有这些证明，并且能够毫无问题地计算with (isElem n ls) 部分，在每种情况下都给我正确的类型吗？还是我错过了一些东西来说服类型检查员？

【问题讨论】：

标签： dependent-type idris type-level-computation

【解决方案1】：

在你使用它之前，仅仅拥有证据并不能真正帮助你。这是我能想到的最好的类型；我不知道代码是否会被合理地优化，或者如果没有，是否有办法让它们变得高效。编译器肯定会认识到每个案例分析只有一个可到达的分支。对我来说不太清楚的是它是否会意识到它因此不需要评估审查员。

mkTestTypeFromNat : (n : Nat) -> (ls : Vect k Nat) -> Elem n ls -> Nat -> TestType {k=k} n ls
mkTestTypeFromNat n ls prf res with (isElem n ls)
  mkTestTypeFromNat n ls prf res | (Yes x) = res
  mkTestTypeFromNat n ls prf res | (No contra) = absurd (contra prf)

mkTestTypeFromUnit : (n : Nat) -> (ls : Vect k Nat) -> Not (Elem n ls) -> TestType {k=k} n ls
mkTestTypeFromUnit n ls prf with (isElem n ls)
  mkTestTypeFromUnit n ls prf | (Yes x) = absurd (prf x)
  mkTestTypeFromUnit n ls prf | (No contra) = ()

【讨论】：