parsing - 在 Idris 中使用类型谓词生成运行时证明

Question

我使用这种类型来推理可以执行可判定解析的字符串:

data Every : (a -> Type) -> List a -> Type where
  Nil : {P : a -> Type} -> Every P []
  (::) : {P : a -> Type} -> P x -> Every P xs -> Every P (x::xs)

例如，像这样定义数字 [0-9]:

data Digit : Char -> Type where
  Zero  : Digit '0'
  One   : Digit '1'
  Two   : Digit '2'
  Three : Digit '3'
  Four  : Digit '4'
  Five  : Digit '5'
  Six   : Digit '6'
  Seven : Digit '7'
  Eight : Digit '8'
  Nine  : Digit '9'

digitToNat : Digit a -> Nat
digitToNat Zero  = 0
digitToNat One   = 1
digitToNat Two   = 2
digitToNat Three = 3
digitToNat Four  = 4
digitToNat Five  = 5
digitToNat Six   = 6
digitToNat Seven = 7
digitToNat Eight = 8
digitToNat Nine  = 9

那么我们可以有以下功能:

fromDigits : Every Digit xs -> Nat -> Nat
fromDigits [] k = 0
fromDigits (x :: xs) k = (digitToNat x) * (pow 10 k) + fromDigits xs (k-1)

s2n : (s : String) -> {auto p : Every Digit (unpack s)} -> Nat
s2n {p} s = fromDigits p (length s - 1)

这个 s2n 函数现在可以在编译时正常工作，但其本身并不是很有用。要在运行时使用它，我们必须先构造证明Every Digit (unpack s)，然后才能使用该函数。

所以我想我现在想写一些像这样的函数:

every : (p : a -> Type) -> (xs : List a) -> Maybe $ Every p xs

或者我们想要返回成员(member)证明或非成员(member)证明，但我不完全确定如何以一般方式执行这些操作。因此，我尝试仅针对字符执行 Maybe 版本:

every : (p : Char -> Type) -> (xs : List Char) -> Maybe $ Every p xs
every p [] = Just []
every p (x :: xs) with (decEq x '0')
  every p ('0' :: xs) | (Yes Refl)  = Just $ p '0' :: !(every p xs)
  every p (x   :: xs) | (No contra) = Nothing

但是后来我得到了这个统一错误:

    Can't unify
            Type
    with
            p '0'

    Specifically:
            Can't unify
                    Type
            with
                    p '0'

但是p属于Char -> Type类型。我不确定是什么导致了统一失败，但认为问题可能与 my previous question 有关。 .

对于我想要做的事情来说，这是一个明智的方法吗？我觉得目前的工作量有点大，而且这些函数的更通用版本应该是可能的。如果可以使用 auto 关键字编写一个函数，以类似的方式为您提供一个 Maybeproof 或 EitherproofproofThatItIsNot ，那就太好了了解 DecEq 类的工作原理。

Answer 1

错误消息是正确的:您提供了 Type 类型的值，但您需要 p '0' 类型的值。您还正确地认为 p 的类型为 Char -> Type，因此 p '0' 的类型为 Type。但是，p '0' 不是 p '0' 类型。

也许使用更简单的类型会更容易看到问题:3 的类型为 Int，而 Int 的类型为 Type，但 Int 没有类型 Int。

现在，我们如何解决这个问题？嗯，p 是一个谓词，这意味着它构造的类型的居民是该谓词的证明。因此，我们需要提供的 p '0' 类型的值将是一个证明，在本例中是 '0' 是数字的证明。 Zero 恰好就是这样一个证明。但在 every 的签名中，p 变量并不是在谈论数字:它是一个抽象谓词，我们对此一无所知。因此，我们无法使用任何值来代替 p '0'。我们必须更改 every 的类型。

一种可能性是编写一个更专门的 every 版本，该版本仅适用于特定谓词 Digit，而不是适用于任意 p:

everyDigit : (xs : List Char) -> Maybe $ Every Digit xs
everyDigit [] = Just []
everyDigit (x :: xs) with (decEq x '0')
  everyDigit ('0' :: xs) | (Yes Refl)  = Just $ Zero :: !(everyDigit xs)
  everyDigit (x   :: xs) | (No contra) = Nothing

我没有在需要 p '0' 类型值的地方错误地使用值 p '0'，而是使用了值 Zero 位于现在需要 Digit '0' 类型值的位置。

另一种可能性是修改 every，这样除了为每个 Char 提供证明类型的谓词 p 之外，我们还可以还接收一个证明制作函数 mkPrf，如果可能的话，它将为每个 Char 提供相应的证明值。

every : (p : Char -> Type)
     -> (mkPrf : (c : Char) -> Maybe $ p c)
     -> (xs : List Char)
     -> Maybe $ Every p xs
every p mkPrf [] = Just []
every p mkPrf (x :: xs) with (mkPrf x)
  every p mkPrf (x :: xs) | Just prf = Just $ prf :: !(every p mkPrf xs)
  every p mkPrf (x :: xs) | Nothing  = Nothing

我不再对 Char 进行模式匹配，而是要求 mkPrf 检查 Char。然后我对结果进行模式匹配，看看是否找到了证据。它是 mkPrf 的实现，它在 Char 上进行模式匹配。

everyDigit' : (xs : List Char) -> Maybe $ Every Digit xs
everyDigit' = every Digit mkPrf
  where
    mkPrf : (c : Char) -> Maybe $ Digit c
    mkPrf '0' = Just Zero
    mkPrf _   = Nothing

在 mkPrf 的实现中，我们再次构造具体类型 Digit '0' 而不是抽象类型 p '0'< 的证明，所以零是一个可接受的证明。