dependent-type - 如何在 Idris 中表达范围有效性？

Question

我正在尝试在 Idris 中构建一个简单的调查表单，目前正在努力验证用户输入，该输入以字符串形式出现。所提出问题的类型。

目前我有以下类型:

data Question : Type where
  QCM : {numOptions : Nat}
      -> (question : String) 
      -> (qcmOptions : Vect numOptions String)
      -> (expected : Fin numOptions)
      -> Question

data Answer : (q : Question) -> Type where
   AnswerQCM : (option : Fin n) -> Answer (QCM {numOptions = n } q opts exp)

total 
isCorrectAnswer : (q : Question ) -> Answer q -> Bool
isCorrectAnswer (QCM {numOptions} question qcmOptions expected) (AnswerQCM option) = option == expected


data IsAnswer : (s : String) -> (q : Question) -> Type where
     ValidQCM : (option : Fin n) -> IsAnswer s (QCM {numOptions = n } q opts exp)

notInRange : (num : Fin n) -> { auto prf : GT numOptions n } 
           -> IsAnswer s (QCM {numOptions} q opts exp) -> Void
notInRange num x = ?notInRange_rhs

我不知道如何编写 notInRange 函数，该函数应该证明某些数字可能不是多项选择题调查的有效答案:该数字应该是正确的问题中提供的选项数量范围。

更一般地说，我想编写一个 readAnswer 函数，如下所示:

readAnswer : (s : String) -> (q : Question) -> Dec (IsAnswer s q)
readAnswer s (QCM question qcmOptions expected) = ?readAnswer_rhs_1

看来我很难找到 Dec 的 contra 部分，因为我的类型没有正确表达我想要的约束，以至于某些类型可以证明它们无人居住。

Answer 1

嗯，你的问题的答案相当大。您有几个设计问题。我不会只粘贴结果代码。相反，我将尝试解释正在发生的事情以及您当前的方法存在哪些问题。也许我的解决方案并不完全是您想要的(也许您甚至不需要您想要的)，但我希望它对您有所帮助。

一个大问题出在您的 isCorrectAnswer 函数中。它返回 Bool ，而 Bool 不利于证明，因为编译器对 Bool 的值了解不多。如果您想要更多的证明能力，您应该使用 Refl 而不是 True/False。 Maybe 和 Dec 的情况相同。如果 Maybe 就足够了，那么就可以了，但是如果您希望您的实现是可证明的，您应该使用 Dec 而不是 Maybe。一旦您决定在函数中使用 Dec，您正在使用和调用的所有函数也应该包含更多可证明的信息。

思考过程的良好开端是考虑具有如下功能:

isCorrectAnswer : (q: Question) -> (a: Answer q) -> expected q = option a 

不幸的是，由于两个问题，这个函数无法存在。

1. 这是一个证据，而证据就是永远正确的。如果您有任意的问题和答案，那么预期的答案并不总是与给出的答案完全相同。因此，您应该将此函数转换为具有此类属性的数据类型。这只是一个通用方法。
2. 好吧，在当前情况下，您甚至无法为 Question 数据类型编写预期函数。也许有人可以，但我尝试过但失败了。此预期函数不是当前实现中相应字段的名称。 numOptions 是 Question 的一些内部事物。如果没有模式匹配，从外部看不到它。因此，根据向量长度对 Question 进行参数化是一件好事。

为了解决 2，我将通过以下方式稍微转换您的数据类型:

record Question (numOptions : Nat) where
    constructor QCM
    question   : String
    qcmOptions : Vect numOptions String
    expected   : Fin  numOptions

record Answer (q : Question n) where
    constructor AnswerQCM
    option : Fin n

现在属性可以如下所示:

data IsCorrectAnswer : (q : Question n) -> (a: Answer q) -> Type where
   IsCorrect : {q: Question n} 
            -> {a: Answer q} 
            -> expected q = option a 
            -> IsCorrectAnswer q a

这是简单的决定过程:

isCorrectAnswer : (q : Question n) -> (a: Answer q) -> Dec (IsCorrectAnswer q a)
isCorrectAnswer (QCM  _ _ expected) (AnswerQCM option) =
    case decEq expected option of
        Yes prf   => Yes (IsCorrect prf)
        No contra => No (\(IsCorrect prf) => contra prf)

在你的问题中，你想要String和Question之间的属性，而我在Answer和Question之间实现。因此，现在理论上您可以在 qcmOptions 中查找该字符串，找到 Fin 索引，将其转换为答案并获取 IsCorrectAnswer< 的 Dec/。嗯，有点像。但事实证明它非常非常不平凡。只是因为你无法证明你想要的定理的原因。

在您的数据类型中，没有任何东西可以将 s: String 与 (option : Fin n) 连接起来。也许，几个附加属性和数据类型可以提供帮助。但更简单的解决方案是使用 Elem property 让您的 IsAnswer 属性包含更多信息。对于Vect。这是与 isCorrectAnswer 几乎相同的最终实现:

data IsAnswer : (s : String) -> (q : Question n) -> Type where
    ValidQCM : {q: Question n} -> Elem s (qcmOptions q) -> IsAnswer s q

readAnswer : (s : String) -> (q: Question n) -> Dec (IsAnswer s q)
readAnswer s (QCM _ options _) = case isElem s options of
    Yes prf   => Yes (ValidQCM prf)
    No contra => No (\(ValidQCM prf) => contra prf)

您可以注意到，我在这里没有使用 isCorrectAnswer，而且由于我之前提到的问题，我可能无法使用它。但我不需要在这里使用它。解决方案越简单越好。

P.S.抱歉，文字墙很长，我可能写了较短的答案，但我希望通过这种方式，这个答案可以向您澄清更多事情。