Gibt es aktuelle Informationen zur Art und Verwendung des postulate Konstrukts in Idris? Es gibt nichts zum Thema im Tutorial / Handbuch und ich kann auch nichts im Wiki finden. TIA.
Ich denke, wir würden das Wiki zu einer Referenz für so etwas entwickeln: Ссылка
Die Syntax für postulate lautet:
wie in
%Vor%oder
%Vor%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. Nehmen wir an, Sie möchten etwas implementieren, das einen Beweis benötigt, wie diese Semigroup-Typklasse einen Beweis benötigt, dass die Operation assoziativ ist, damit sie als gültige Halbgruppe betrachtet werden kann:
%Vor%Das ist einfach genug, um Dinge wie Nats und Lists zu beweisen, aber was ist mit etwas wie einer 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. Sie können also die Existenz einer solchen Sache postulieren, um dem Compiler zu sagen, "vertrauen Sie mir einfach auf dieses eine".
%Vor% Programme mit solchen Postulaten können weiterhin ausgeführt und verwendet werden, solange keine postulierten "Werte" aus Laufzeitwerten erreichbar sind (was wäre ihr Wert?). 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. der single-bewohnte Unit type:
kompiliert und läuft noch (druckt "()"); Der Wert des Typs Unit wird von der Implementierung von show nicht wirklich benötigt.
Tags und Links idris