Is there any up to date information regarding the nature and use of the postulate construct in Idris? There is nothing on the subject in the tutorial/manual and I can't seem to find anything in the wiki as well. TIA.
I think we were going to develop the wiki into more of a reference for this sort of thing: https://github.com/idris-lang/Idris-dev/wiki/Manual
The syntax for postulate is:
postulate identifier : type
as in
postulate n : Nat
or
postulate whyNot : 5 = 6
It introduces an unspecified value of that type. This can be useful when you need an instance of a type that you don't otherwise know how to introduce. Say you want to implement something that requires a proof, like this Semigroup typeclass requires a proof that the operation is associative for it to be considered a valid semigroup:
class Semigroup a where
op : a -> a -> a
semigroupOpIsAssoc : (x, y, z : a) -> op (op x y) z = op x (op y z)
That's easy enough to prove for things like Nats and Lists, but what about for something like a machine int where the operation is defined outside of the language? You need to show that the type signature given by semigroupOpIsAssoc is inhabited, but lack a way to do so in the language. So you can postulate the existence of such a thing, as a way of telling the compiler "just trust me on this one".
instance Semigroupz Int where
op = (+)
semigroupOpIsAssoc x y z = intAdditionIsAssoc
where postulate intAdditionIsAssoc : (x + y) + z = x + (y + z)
Programs with postulate like that can still be run and used, as long any postulated "values" aren't reachable from runtime values (what would their value be?). This is fine for equality terms, which aren't used in anywhere but typechecking and are erased at runtime. An exception of sorts is terms whose values can be erased, e.g. the singley-inhabited Unit type:
postulate foo : Unit
main : IO ()
main = print foo
still compiles and runs (prints "()"); the value of the Unit type isn't actually needed by the implementation of show.