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。この統合の失敗の原因はわかりませんが、問題は以前の質問に関連している可能性があると思います。

これは私がやろうとしていることに対する賢明なアプローチですか? 現時点では少し多すぎるように感じますが、これらの関数のより一般的なバージョンが可能になるはずです。クラスがどのように機能するかと同様の方法で、キーワードを使用して aまたはautoを与える関数を記述できるとよいでしょう。Maybe proofEither proof proofThatItIsNotDecEq

4

1 に答える 1

8

エラー メッセージは正しいです。 type の値を指定しましTypeたが、 type の値が必要ですp '0'。pあなたはそれがタイプであることも正しいChar -> Typeので、それp '0'はタイプTypeです。ただし、p '0'タイプではありませんp '0'。

3おそらく、この問題は単純な型 ( has type Int、Inthas type Type、 but Intdoes not have type )で確認しやすいでしょうInt。

さて、問題をどのように修正しますか？述語pです。つまり、この述語の証明である型を構築します。したがって、p '0'提供する必要がある type の値は証明であり、この場合'0'は数字である証明です。Zeroたまたまそのような証拠です。しかし、 の署名でeveryは、p変数は数字について話しているのではありません。それは、私たちが何も知らない抽象的な述語です。このため、 の代わりに使用できる値はありませんp '0'。代わりに の型を変更する必要がありeveryます。

1 つの可能性は、任意の ではなくevery、特定の述語に対してのみ機能する、より特殊化されたバージョンの を作成することです。Digitp

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'値を使用しZeroましたDigit '0'。

別の可能性としては、可能な場合は、 every の証明型を与えるevery述語に加えて、対応する証明値を与える証明作成関数も受け取るように変更することです。pCharmkPrfChar

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ように求めています。次に、結果に対してパターン マッチを行い、証明が見つかったかどうかを確認します。でのパターンマッチの実装です。mkPrfCharmkPrfChar

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 に答える