Postulate in Idris

Question

Gibt es aktuelle Informationen über die Art und die Verwendung des postulate Konstrukts in Idris? Es gibt nichts zum Thema im Tutorial/Handbuch und ich kann auch nichts im Wiki finden. TIA.

Answer 1

Ich denke, wir würden das Wiki in mehr eine Referenz für diese Art der Sache zu entwickeln: https://github.com/idris-lang/Idris-dev/wiki/Manual

Die Syntax für postulate ist:

postulate identifier : type 

wie in

postulate n : Nat 

oder

postulate whyNot : 5 = 6 

Es führt einen unspezifizierten Wert dieses Typs ein. Dies kann nützlich sein, wenn Sie eine Instanz eines Typs benötigen, die Sie sonst nicht einführen könnten. Sagen Sie bitte etwas implementieren möchten, die einen Nachweis darüber verlangt, wie diese Halbgruppentypeclass einen Beweis verlangt, dass die Operation assoziativ ist für sie eine gültige Halbgruppe in Betracht gezogen werden:

class Semigroup a where 
    op : a -> a -> a 
    semigroupOpIsAssoc : (x, y, z : a) -> op (op x y) z = op x (op y z) 

, das einfach genug ist für Dinge wie Nats zu beweisen, und Listen, aber was ist für so etwas wie eine Maschine int, wo die Operation außerhalb der Sprache definiert ist? Sie müssen zeigen, dass die von semigroupOpIsAssoc angegebene Typensignatur bewohnt ist, aber in der Sprache nicht möglich ist. Du kannst also die Existenz eines solchen Dinges postulieren, um dem Compiler zu sagen "vertraue mir einfach auf dieses".

instance Semigroupz Int where 
    op = (+) 
    semigroupOpIsAssoc x y z = intAdditionIsAssoc 
     where postulate intAdditionIsAssoc : (x + y) + z = x + (y + z) 

Programme mit Postulat wie das immer noch laufen und verwendet werden, so lange alle postulierten „Werte“ sind nicht erreichbar von Laufzeitwerte (was würde ihr Wert sein?). Dies ist in Ordnung für Gleichheitsbedingungen, die nirgendwo außer Typprüfung verwendet werden und zur Laufzeit gelöscht werden. Eine Ausnahme sind Arten, deren Werte gelöscht werden können, z. die Singley bewohnten Unit Typ:

postulate foo : Unit 

main : IO() 
main = print foo 

kompiliert noch und läuft (prints "()"); Der Wert des Unit-Typs wird von der Implementierung show nicht tatsächlich benötigt.