Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Postulates in Idris

Tags:

idris

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.

like image 733
Arets Paeglis Avatar asked Jan 17 '15 12:01

Arets Paeglis


1 Answers

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.

like image 77
pdxleif Avatar answered Oct 08 '22 01:10

pdxleif