Frama-C API - S

Monad signature with let-bindings

This signature provides all the usual monadic operators along with let-bindings definitions used to simplify codes relying on monads. The provided operators are as follows:

• return embeds a value x in the monad.
• bind encodes the idea of "sequence" in the monadic world, i.e the call bind f m comes down to performing the computation m before applying the next computation step, represented by the function f, to the resulting value.
• map applies a function through the monad. One can examplify it by making a parallel with the list map operator.
• flatten is used to handle nested applications of the monad.

The provided let-bindings operators can be used to write simpler and cleaner code. For example, one can write let+ v = compute x in v + 1 instead of map (fun v -> v + 1) (compute x). The more monadic steps, the simpler the code will get when written using those operators. In this module, >>- and let* always correspond to the bind operator while >>-: and let+ always correspond to the map. All those operators are provided in an Operators module to avoid namespace conflicts. Indeed, one can use the expression let open MyMonad.Operators in to use all the let-bindings without risking conflicts by including the other definitions, which have rather common names. This idiom also helps indicate which monad is currently used in a code.

• since Frama-C+dev