8

我正在使用这种类型来推断可以执行可判定解析的字符串：

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类的工作方式一样。

4

1 回答 1

8

错误消息是正确的：您提供了 type 的值Type，但您需要 type 的值p '0'。您也是正确的 that pis of type Char -> Type，因此 that p '0'is of type 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'需要 type 值的地方错误地使用该值，而是在现在需要 type 值的地方使用了该值。p '0'ZeroDigit '0'

另一种可能性是进行修改every，以便除了为 everyp提供证明类型的谓词之外Char，我们还将收到一个证明函数mkPrf，该函数将在可能的情况下为 every 提供相应的证明值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是可接受的证明。

于 2014-11-25T02:57:37.290 回答