Generazione di eseguire prove di tempo con il tipo di predicati a Idris

Question

Sto usando questo tipo di ragionare sulle stringhe su cui l'analisi decidibile può essere eseguita:

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) 

Per esempio, la definizione delle cifre [0-9] come questo:

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 

allora possiamo avere le seguenti funzioni:

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) 

QuestoLa funzione 0 ora funzionerà bene al momento della compilazione, ma non è molto utile in sé. Per utilizzarlo in fase di esecuzione, è necessario costruire la prova Every Digit (unpack s) prima di poter utilizzare la funzione.

Quindi penso che ora voglio scrivere qualcosa di simile a questa funzione:

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

Che o vogliamo tornare sia una prova di composizione o una prova della non-appartenenza, ma non sono del tutto sicuro come fare entrambe queste cose in modo generale. Così, invece Ho provato a fare la versione Maybe solo per i personaggi:

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 

Ma poi ho ottenere questo errore unificazione:

Can't unify 
      Type 
    with 
      p '0' 

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

Ma pè di tipo Char -> Type. Non sono sicuro di cosa stia causando questo errore di unificazione, ma penso che il problema potrebbe essere correlato a my previous question.

È un approccio ragionevole a quello che sto cercando di fare? Mi sembra che al momento sia un po 'troppo impegnativo, e dovrebbero essere possibili versioni più generali di queste funzioni. Sarebbe bello se la parola chiave auto potesse essere usata per scrivere una funzione che ti dia un Maybe proof o un Either proof proofThatItIsNot, in modo simile a come funziona la classe DecEq.

Answer 1

Il messaggio di errore è corretto: è stato fornito un valore di tipo Type, ma è necessario un valore di tipo p '0'. Si è inoltre corretto che p è di tipo Char -> Type e che pertanto p '0' è di tipo Type. Tuttavia, p '0' non è di tipo p '0'.

Forse il problema sarebbe più facile da vedere con i tipi più semplici: 3 è di tipo Int, e Int ha digitare Type, ma Int non hanno tipo Int.

Ora, come risolviamo il problema? Bene, p è un predicato, nel senso che costruisce tipi i cui abitanti sono la prova di questo predicato. Quindi il valore di tipo p '0' che dobbiamo fornire sarebbe una prova, in questo caso una prova che '0' è una cifra. Zero sembra essere una prova del genere. Ma nella firma di every, la variabile p non sta parlando di cifre: è un predicato astratto, di cui non sappiamo nulla. Per questo motivo, non ci sono valori che potremmo usare al posto di p '0'. Dobbiamo invece modificare il tipo di every.

Una possibilità sarebbe quella di scrivere una versione più specializzata versione di every, uno che funziona solo per la particolare predicato Digit invece di lavorare per un arbitrario 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 

Anziché correttamente utilizzando il valore p '0' in un punto che ha bisogno di un valore di tipo p '0', ho utilizzato il valore Zero in un punto che ora ha bisogno di un valore di tipo Digit '0'.

Un'altra possibilità sarebbe quella di modificare every modo che oltre al predicato p che dà un tipo di prova per ogni Char, ci sarebbe anche ricevere una funzione a prova di rendere mkPrf che darebbe il valore prova corrispondente per ogni Char, quando possibile.

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 

io non sono un pattern-matching è più sul Char, invece chiedo mkPrf per esaminare la Char. Ho quindi modellato il risultato, per vedere se ha trovato una prova. È l'implementazione di mkPrf che corrisponde alle corrispondenze su 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 

Nell'attuazione mkPrf, ci sono ancora costruendo una prova per il tipo concreto Digit '0' invece del tipo astratto p '0', così Zero è una prova accettabile.