package monadlib

  1. Overview
  2. Docs

For the incorruptible programmer:

A continuation of type 'a has type ('a -> 'r) -> 'r

The first argument to this continuation is a final value of type 'r which depends on some intermediate value of type 'a. In other words, we can understand the continuation as a result of type 'r which depends on the future of an intermediate value.

The function return just throws its return value to the future in order to produce the final result. The bind intercedes in the future, inserting a computation.

Call-with-current-continuation allows one to effectively reflect into one's own future. That is, callCC is a computation which depends on another computation taking the future as a first-class value. One can store this future, and at any time, throw it a return value to reinstate it.

If you are into the Curry-Howard Isomorphism, call-with-current-continuation has a type which corresponds to a law of classical logic (Pierce's Law). Writing your code in the continuation monad corresponds to embedding classical logic intuitionistically. Allowing callCC corresponds to assuming a classical hypothesis.

Parameters

module T : sig ... end

Signature

include Monad with type 'a m = ('a -> T.r) -> T.r
include BatInterfaces.Monad with type 'a m = ('a -> T.r) -> T.r
type 'a m = ('a -> T.r) -> T.r

The type of a monad producing values of type 'a.

val bind : 'a m -> ('a -> 'b m) -> 'b m

Monadic binding.

bind m f executes first m then f, using the result of m.

include Applicative.Applicative with type 'a m := 'a m
include Applicative.Base with type 'a m := 'a m
val return : 'a -> 'a m
val (<*>) : ('a -> 'b) m -> 'a m -> 'b m
val lift1 : ('a -> 'b) -> 'a m -> 'b m
val lift2 : ('a -> 'b -> 'c) -> 'a m -> 'b m -> 'c m
val lift3 : ('a -> 'b -> 'c -> 'd) -> 'a m -> 'b m -> 'c m -> 'd m
val lift4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a m -> 'b m -> 'c m -> 'd m -> 'e m
val (<$>) : ('a -> 'b) -> 'a m -> 'b m

Alias for lift1.

val sequence : 'a m list -> 'a list m
val map_a : ('a -> 'b m) -> 'a list -> 'b list m
val (<*) : 'a m -> 'b m -> 'a m
val (>*) : 'a m -> 'b m -> 'b m
val (>>=) : 'a m -> ('a -> 'b m) -> 'b m
val join : 'a m m -> 'a m
val filter_m : ('a -> bool m) -> 'a list -> 'a list m
val onlyif : bool -> unit m -> unit m
val unless : bool -> unit m -> unit m
val ignore : 'a m -> unit m
val callCC : (('a -> 'r m) -> 'a m) -> 'a m