在Idris中使用类型谓词生成运行时证明 [英] Generating run time proofs with type predicates in Idris

问题描述

我正在使用这种类型来推理可以在其上执行可确定的解析的字符串:

I am using this type to reason about strings on which decidable parsing can be performed:

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]:

For example, defining the digits [0-9] like this:

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

然后我们可以具有以下功能:

then we can have the following functions:

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)，然后才能使用该函数.

This s2n function will now work fine at compile time, but then that isn't very useful in of itself. To use it at runtime we must construct the proof Every Digit (unpack s) before we can use the function.

所以我认为我现在想编写类似此功能的内容:

So I think I now want to write something like this function:

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

那个或我们想要返回成员资格证明或非成员资格证明，但是我不完全确定如何以一般的方式来做这两种事情.因此，我尝试仅针对字符执行Maybe版本:

That or we want to return either a proof of membership or a proof of non-membership, but I'm not entirely sure how to do either of these things in a general way. So instead I tried doing the Maybe version for just characters:

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

但随后出现此统一错误:

But then I get this unification error:

    Can't unify
            Type
    with
            p '0'

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

但是p 是类型的 .我不确定是什么原因导致此统一失败，但认为该问题可能与我之前的问题.

But p is of type Char -> Type. I'm not sure what is causing this unification failure, but think the problem may be related to my previous question.

这是我要做的明智的选择吗?我觉得目前这工作量不大，应该可以使用这些功能的更通用版本.如果可以使用auto关键字来编写一个函数，为您提供Maybe proof或Either proof proofThatItIsNot，这与DecEq类的工作方式类似，那就太好了.

Is this a sensible approach to what I am trying to do? I feel like it is a little to much work at the moment, and more general versions of these functions should be possible. It would be nice if the auto keyword could be used to write a function gives you a Maybe proof or an Either proof proofThatItIsNot, in a similar way to how the DecEq class works.

推荐答案

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

The error message is correct: you provided a value of type Type, but you need a value of type p '0'. You are also correct that p is of type Char -> Type, and therefore that p '0' is of type Type. However, p '0' is not of type p '0'.

使用更简单的类型也许更容易发现此问题:3具有类型Int，而Int具有类型Type，但是Int没有类型Int.

Perhaps the issue would be easier to see with simpler types: 3 has type Int, and Int has type Type, but Int does not have type Int.

现在，我们如何解决该问题?好吧，p是一个谓词，意味着它构造了其居民是该谓词证明的类型.因此，我们需要提供的类型p '0'的值将是一个证明，在这种情况下，证明'0'是一个数字. Zero恰恰是这样的证明.但是在every的签名中，p变量不是在谈论数字:它是一个抽象谓词，对此我们一无所知.因此，没有可用的值代替p '0'.相反，我们必须更改every的类型.

Now, how do we fix the problem? Well, p is a predicate, meaning that it constructs types whose inhabitants are proofs of this predicate. So the value of type p '0' we need to provide would be a proof, in this case a proof that '0' is a digit. Zero happens to be such a proof. But in the signature of every, the p variable isn't talking about digits: it's an abstract predicate, about which we know nothing. For this reason, there are no values we could use instead of p '0'. We must instead change the type of every.

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

One possibility would be to write a more specialized version version of every, one which would only work for the particular predicate Digit instead of working for an arbitrary 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.

Instead of incorrectly using the value p '0' in a spot which needs a value of type p '0', I have used the value Zero in a spot which now needs a value of type Digit '0'.

另一种可能性是修改every，以便除了为每个Char提供证明类型的谓词p外，我们还将收到一个证明产生函数mkPrf，该函数将提供相应的证明类型每个Char的证明值.

Another possibility would be to modify every so that in addition to the predicate p which gives a proof type for every Char, we would also receive a proof-making function mkPrf which would give the corresponding proof value for every Char, when possible.

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上的模式匹配.

I am no longer pattern-matching on the Char, instead I am asking mkPrf to examine the Char. I then pattern-match on the result, to see if it found a proof. It is the implementation of mkPrf which pattern-matches on the 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是可以接受的证明.

In the implementation of mkPrf, we are again constructing a proof for the concrete type Digit '0' instead of the abstract type p '0', so Zero is an acceptable proof.

这篇关于在Idris中使用类型谓词生成运行时证明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！