package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module type Monad.Based_on_bind

Minimal signature based on bind

This is the usual minimal definition of a monadic type constructor, also called a Kleisli triple. The return function embeds a value x in the monad. The bind function, also called the "combinator", corresponds to 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.

To fully qualify as a monad, these three parts must respect the three following laws :

1. return is a left-identity for bind : ∀f:('a -> 'b t), ∀x:'a, bind f (return x) ≣ return (f x)

2. return is a right-identity for bind : ∀m:'a t, bind return m ≣ m

3. bind is associative : ∀m:'a t, ∀f:('a -> 'b t), ∀g:('b -> 'c t), bind (fun x -> bind g (f x)) m ≣ bind g (bind f m)

As there is no way in the OCaml type system to enforce those properties, users have to trust the implemented monad when using it, and developers have to manually check that they are respected.

  • since 31.0-Gallium
type 'a t
val return : 'a -> 'a t
val bind : ('a -> 'b t) -> 'a t -> 'b t