13

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.

1 Answer 1

15

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.

1
  • 1
    Edwin said a postulated value can be referenced at runtime when "a value can be generated from its indices alone, or its type alone; so at most one canonical element"
    – pdxleif
    Commented Jan 18, 2015 at 8:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.