使用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

那或者我们想要返回会员证明或非会员证明,但我不完全确定如何以一般方式做这些事情.所以我尝试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.我不确定导致这种统一失败的原因,但认为问题可能与我之前的问题有关.

这是一个明智的方法,我想做什么？我觉得此刻它的工作量有点大,应该可以使用这些功能的更多通用版本.如果auto关键字可以用来编写一个函数给你一个Maybe proof或Either proof proofThatItIsNot一个类似于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以便除了p为每个人提供证明类型的谓词之外Char,我们还将收到一个证明制作函数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',因此Zero是可接受的证据.