Provalarda ilkel işlemler

Question

Bağımlı türleri öğrenmek için, eski Haskell oyunumu Idris'da yeniden yazıyorum. Şu anda oyun „motor“ Word8 gibi yerleşik integral türlerini kullanıyor. Bu sayıların sayısal özelliklerini içeren bazı lemmaları ispatlamak isterim (bu çift olumsuzluk, kimliktir). Ancak, ilkel aritmetik işlemlerin davranışları hakkında bir şey söylemek mümkün değildir. believe_me veya diğer el sıkışmalarını (en azından en temel özellikler için) kullanmak veya Nat, Fin ve diğer "yüksek düzey" sayısal türlerini kullanarak kodumu yeniden yazmak için daha iyi ne olurdu?

Answer 1

postulate, gereksinim duyduğunuz ilkel özellikler için, yalnızca söz konusu sayısal türler için aslında doğru olan şeyleri kullanmak için dikkatli olmanızı öneririm elbette ki (ki bu sadece temelde taşma konusunda dikkatli olmaktır). Eğer ispat bazı hesaplama davranışını gerekmedikçe

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

believe_me iyi kaçınılmalıdır: Yani gibi şeyler söyleyebiliriz. Ama dürüst olmak gerekirse, hala ilkelleri akıl yürütürken bu şeyleri yapmaya çalışıyoruz ...

Answer 2

Şu an için, Nat'u kullanabildiğiniz zaman genel olarak daha iyi olduğuna inanıyorum. İdris devleri, sonunda, prova dostu tiplerin, derleme sırasında hızlı ilkel olanlarla değiştirilmesi için genel bir mekanizma geliştirmeyi planlıyorlar, ancak şimdilik sadece Nat. Gerçekten istiyorsan, believe_me yapabilirsin, ama kanıtlarla çalışmak için çok kolay olmayan fonksiyonlarla sonuçlanırdın. believe_me ile oynamaya karar verirseniz, really_believe_me'u da göz önünde bulundurmalısınız, ki bu da tür denetleyicisine daha inandırıcı bir özelliktir.