与伊德里斯

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型。我不确定是什么导致了统一失败，但认为这个问题可能与my previous question有关。

这是一个明智的做法是什么，我想干什么？我觉得目前有很多工作要做，而且这些功能的更一般版本应该是可能的。如果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'类型的值的地方，我已经在值为Digit '0'的地方使用值Zero。当

另一种可能性是修改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'，所以Zero是一个可以接受的证明。