Postulates in Idris

Question

Is there any updated information on the nature and use of the postulate construct in Idris? There is nothing in this tutorial / guide on this, and I, too, cannot find anything on the wiki. TIA.

Answer 1

I think we are going to develop a wiki in most of the help for this kind of thing: https://github.com/idris-lang/Idris-dev/wiki/Manual

The syntax for postulate :

 postulate identifier : type 

how in

 postulate n : Nat 

or

 postulate whyNot : 5 = 6 

It introduces an undefined value of this type. This can be useful when you need an instance of a type that you otherwise don't know how to enter. Suppose you want to implement something that needs proof, for example, this class of semigroups requires proof that the operation is associative in order to be considered an admissible semigroup:

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

It's easy enough to prove for things like Nats and Lists, but what about something like an int machine, where the operation is defined outside the language? You need to show that the type signature given by semigroupOpIsAssoc is populated, but there is no way to do it in the language. Thus, you can postulate the existence of such a thing as a way to tell the compiler "just trust me on this."

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

Programs with a similar postulate can still be run and used, since any postulated "values" are not available from the run-time values ​​(what would be their value?). This is normal for equality terms that are not used anywhere other than type checking and are erased at run time. Sort exclusions are terms whose values ​​may be erased, for example. single type Unit :

 postulate foo : Unit main : IO () main = print foo 

still compiles and starts (prints "()"); a value of type Unit is not actually required in the implementation of show .