Question

What is the meaning of and differences among ->, -->, ~>?

Answer

These are all used in designating the type of functions; they are sometimes called arrow types. In each case, A -> B is the type of a function taking an argument of type A and producing a value of type B; The function argument types can be enclosed in parentheses, and if the number of arguments is not 1 or the argument is a tuple type, then the argument types must be enclosed in parentheses. For example, (A, B) -> C is a type of function that takes two arguments; ((A, B)) -> C takes as argument a 2-tuple.

The three symbols in the question denote different sorts of types of functions:

• -> denotes a total function that is independent of the heap; it may not have a requires clause (precondition) or a reads clause
• --> denotes a partial function; it may have a precondition, but may not have a reads clause, and so it also is independent of the heap
• ~> denotes a partial and possibly heap-dependent function; it may have requires and reads clauses

If a function is independent of the heap, it is useful to say so, either in its declaration or the type that describes it. The value returned by a heap-independent function depends only on its arguments and not on the program state; thus it is easier to reason about its properties. Working with heap-dependent functions is much more difficult than with heap-independent functions, so use -> or --> if you can. And note that Dafny does not support polymorphic arrow types.