與伊德里斯

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是一個可以接受的證明。