Operazioni primitive nelle prove

Question

Per i tipi di apprendimento dipendenti, sto riscrivendo il mio vecchio gioco Haskell in Idris. Attualmente il "motore" del gioco utilizza tipi integrali integrati, come ad esempio Word8. Vorrei provare alcuni lemmi che coinvolgono le proprietà numeriche di quei numeri (ad esempio, quella doppia negazione è l'identità). Tuttavia, non è possibile dire qualcosa sul comportamento delle operazioni aritmetiche primitive. Cosa sarebbe meglio, per usare semplicemente believe_me o altri handwaving (almeno per le proprietà più elementari), o per riscrivere il mio codice usando Nat, Fin e altri tipi "di alto livello" numerici?

Answer 1

Suggerirei di usare postulate per qualsiasi delle proprietà primitive di cui avete bisogno, facendo attenzione solo a usare cose che sono effettivamente vere per i tipi numerici in questione, ovviamente (che fondamentalmente significa solo stare attenti all'overflow). Così si può dire le cose come:

postulate add_commutes : (x, y : Int) -> x + y = y + x 

believe_me è meglio evitare a meno che non avete bisogno di qualche comportamento calcolo della prova. Ma, ad essere onesti, stiamo ancora provando a lavorare su queste cose quando ragioniamo sui primitivi ...

Answer 2

Credo che per il momento sia generalmente meglio usare Nat quando è possibile. Gli sviluppatori di Idris stanno pianificando, alla fine, di implementare un meccanismo generale per sostituire i tipi di prova con quelli veloci primitivi nella compilazione, ma per ora ciò accade solo per Nat. È possibile eseguire believe_me se si desidera veramente, ma si finirebbe con funzioni che non sono così facili da lavorare con prove. Nota che se decidi di giocare con believe_me, dovresti prendere in considerazione anche really_believe_me, che a quanto pare rende più credibile il tipo di controllo.