我使用这种类型来推理可以执行可判定解析的字符串:
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
类的工作原理。
最佳答案
错误消息是正确的:您提供了 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'< 的证明
,所以零
是一个可接受的证明。
关于parsing - 在 Idris 中使用类型谓词生成运行时证明,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/27095563/