What is the meaning of and differences among `->`, `-->`, `~>`?
What is the meaning of and differences among
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
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
requiresclause (precondition) or a
-->denotes a partial function; it may have a precondition, but may not have a
readsclause, and so it also is independent of the heap
~>denotes a partial and possibly heap-dependent function; it may have
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
--> if you can. And note that Dafny does not support polymorphic arrow types.