Frama-C API - Monad

This module provides generic signatures for monads along with tools to build them based on minimal definitions. Those tools are provided for advanced users that would like to define their own monads. Any user that only wants to use the monads provided by the kernel can completly ignore them.

• since Frama-C+dev

Building monads from minimal signatures

Below are functors for creating monads (with or without product). Both gives a strictly equivalent implementation but differ from the primitives given as argument. For an example of monad implementation based on this module, see Option.

Functors extending minimal signatures

Those functors provide a way to extend a minimal signature into a full monad that satisfies the signatures defined above. This is possible because one can define operations from one monadic definition using the operations required by the others. Indeed :

1. ∀m:('a t), ∀f:('a -> 'b), map f m ≣ bind (fun x -> return (f x)) m

2. ∀m:('a t t), flatten m ≣ bind identity m

3. ∀m:('a t), ∀f:('a -> 'b t), bind f m ≣ flatten (map f m)

All required laws expressed in both minimal signatures are respected using those definitions.

Detailled explanations and category theory

To be pedantic, the map based approach defines a monad as a categoric functor equipped with two natural transformations. This does sound frightening but this breaks down to rather simple concepts.

Let's start at the beginning. A category is just a collection of objets and arrows (or morphisms) between those objets that satisfies two properties: there exists a morphism from all objects to themselves, i.e an identity, and if there is a morphism between objects a and b and a morphism between objects b and c, then there must be a morphism between a and c, i.e morphisms are associative.

There is a strong parallel between categories and type systems. Indeed, if one uses the collection of all types as objects, then for all types 'a and 'b, the function f : 'a -> 'b can be seen as a morphism between the objets 'a and 'b. As functions are naturally associative and, for any type 'a, one can trivially defines the identity function 'a -> 'a, one can conclude that types along with all functions of arity one forms a category.

Next, there is the idea of functors. In the category theory, a functor is a mapping between categories. That means that, given two categories A and B, a functor maps all objects of A to an object of B and maps any morphism of A into a morphism of B. But, not all mappings are functors. Indeed, to be a valid functor, one has to preserve the identity morphisms and the composition of morphims.

The idea of functors can also be seen in a type systems. At least, the more restricted but enough here of an endofunctor, a functor from a category to itself. Indeed, for any type v and for any parametric type 'a t, the type v t can be seen as a mapping from values of type v to values of type v t. Thus the type 'a t encodes the first part of what a functor is, a mapping from objects of the Type category to objects of the Type category. For the second part, we need a way to transform morphisms of the Type category, i.e functions of type 'a -> 'b, in a way that preserves categoric properties. Expressed as a type, this transformation can be seen as a higher-order function map with the type map : ('a -> 'b) -> ('a t -> 'b t).

Finally, this definition of a monad requires two natural transformations. Simply put, a natural transformation is a mapping between functors that preserves the structures of all the underlying categories (mathematicians and naming conventions...). That may be quite complicated to grasp, but in this case, the two required transformations are quite simple and intuitive.

The first one is the return function that embeds values into the monad, which can be seen as a natural transformation from the identity functor to the monad functor. The second one is the flatten function, which is a transformation from two applications of the monad functor to the monad functor. With this two transformations, any number of application of the monad functor can be taken down to a unique application of the monad.