package monadlib

You can search for identifiers within the package.

in-package search v0.2.0

monadlib
- Applicative
  - Applicative
  - Base
  - Make
    
    A
  - Transform
    
    A
    
    Inner
- LazyList
- Monad
  - BaseCollectionM
  - BaseLazyPlus
  - BasePlus
  - CollectionOpt
    
    C
  - CollectionState
    
    C
    
    T
  - CollectionWriter
    
    C
    
    Mon
  - Continuation
    
    T
  - Error
    
    E
  - LazyListM
  - LazyM
  - LazyPlus
  - LazyT
    
    M
  - List
  - ListT
    
    M
  - Make
    
    M
  - MakeLazyPlus
    
    M
  - MakePlus
    
    M
  - MakeStream
    
    M
  - MakeStreamC
    
    M
  - Monad
  - MonadPlus
  - Monoid
  - Option
  - OptionT
    
    M
  - Reader
    
    T
  - State
    
    T
  - StateT
    
    M
    
    T
  - Stream
  - StreamC
  - Writer
    
    M
  - WriterT
    
    M
    
    Mon
- TagTree
  - Make
    
    Tag
  - Tree

Legend:
Library
Module
Module type
Parameter
Class
Class type

Streams supporting fair and unbounded search.

Spivey has a nice and authoratitive paper on this, understanding streams as a breadth-first search. If that description appeals to you, I recommend his paper. Personally, I found it helpful to understand streams a bit differently, as concurrent processes that go off and discover data.

First, we have generations, which are collections of zero or more data. The data in each generation is discovered simultaneously, and therefore, it doesn't make much sense to have any ordering imposed on the generations. In fact, the lack of an ordering is essential for getting the associativity laws of the monad, and is why Spivey's paper works with bags.

Now a stream is just a lazy list of generations. We want to think of the indices into these streams as temporal indices. So the first generation in the lazy list was discovered at time 0. The second was discovered at time 1. The third was discovered at time 2. And so on.

Thinking this way helped me figure out return and join. Here, return x gives you the process which immediately discovers x and then terminates.

With join xss, we should interpret the xss as a process which discovers other processes. When we join them, we ask the outer process to fork each inner process as soon as it is discovered, and then merge in all the values found by the forked processes. For instance, if xs discovers a process p at time 5, and in turn, p discovers the string "hello world!" at time 13, then join xs discovers "hello world!" at time 5 + 13 = 18.

Now we can understand bind, realising that it is just the result of doing a map and then a join. The expression bind xs f forks processes f which depend on a discovered value x, and then merges back all their values.

Technically, all our streams should be infinite, and the processes should run forever, but this gave me sad performance in my theorem proving code. So for efficiency, our streams can be truncated, which represents a process that terminates.

Note that it is impossible to define a general BaseLazyPlus.null predicate for streams, because we would have to be able to decide whether an infinite stream of values consists entirely of the empty generation. Turing says that's impossible, and I believe him. As a crude approximation, then, we have it that BaseLazyPlus.null returns true just for the special case that its input is an empty lazy list.

type 'a t

include LazyPlus with type 'a m = 'a t Lazy.t

include BaseLazyPlus with type 'a m = 'a t Lazy.t

include BatInterfaces.Monad with type 'a m = 'a t Lazy.t

type 'a m = 'a t Lazy.t

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

val lplus : 'a m -> 'a m Lazy.t -> 'a m

include MonadPlus with type 'a m := 'a m

include BasePlus with type 'a m := 'a m

include BatInterfaces.Monad with type 'a m := 'a m

val zero : unit -> 'a m

val plus : 'a m -> 'a m -> 'a m

val null : 'a m -> bool

null x implies that x is zero. If you do not want to or cannot answer whether a given x is zero, then null x should be false. I have provided this so that streams can be implemented more efficiently.

include Monad with type 'a m := 'a m

include BatInterfaces.Monad with type 'a m := 'a m

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 filter : ('a -> bool) -> 'a m -> 'a m

val of_list : 'a list -> 'a m

val sum : 'a list m -> 'a m

val msum : 'a m list -> 'a m

val guard : bool -> 'a m -> 'a m

val transpose : 'a list m -> 'a m list

Generalises matrix transposition. This will loop infinitely if BasePlus.null cannot answer true for zeroes.

val of_llist : 'a LazyList.t -> 'a m

val lsum : 'a LazyList.t m -> 'a m

val lmsum : 'a m LazyList.t -> 'a m

val ltranspose : 'a LazyList.t m -> 'a m LazyList.t

Generalises matrix transposition. You don't necessarily have to worry about correctly implementing BaseLazyPlus.null for this function, since the return value can happily be infinite.

val iterate : ('a m -> 'a m) -> 'a m -> 'a m

The sum of the stream [f x, f (f x), f (f (f x)),...]

val delay : 'a m -> 'a m

Delay a stream by one time step. This is needed when you write recursive streams and you have to avoid deadlock. The nice thing about Ocaml here is that it will generally detect deadlock for you, announcing to you that you're writing viciously circular lists!

val to_depth : int -> 'a m -> 'a m

Terminate discovery at some depth.