previous   next   up   top

Monads in Haskell and other languages

 


 

LogicT - backtracking monad transformer with fair operations and pruning

[The Abstract of the paper]
We design and implement a library for adding backtracking computations to any Haskell monad. Inspired by logic programming, our library provides, in addition to the operations required by the MonadPlus interface, constructs for fair disjunctions, fair conjunctions, conditionals, pruning, and an expressive top-level interface. Implementing these additional constructs is well-known in models of backtracking based on streams, but not known to be possible in continuation-based models. We show that all these additional constructs can be generically and monadically realized using a single primitive which we call msplit. We present two implementations of the library: one using success and failure continuations; and the other using control operators for manipulating delimited continuations.

It seems that something similar (but not identical) to msplit has been discovered at least twice before: under the names unbuild (Andrew Gill, 1996) and destroy (Josef Svenningsson, ICFP02). Our function reflect is also related to unfoldr. One of the earlier versions of Kanren did indeed implement something like destroy, internally using regular list constructors to split a stream.

However, the present function msplit is significantly more general: it has nothing to do with Haskell lists and never uses any lists constructors, even internally. The functions msplit and reflect operate over any backtracking computation over any base monad. The presence of the base monad makes things trickier as we now must assure that we do not repeat effects. Therefore, the equivalent of the destroy/infoldr rule of Josef Svenningsson's destroy . unfoldr === id is, in ``small-step semantics'':

     rr (lift m >> mzero)     ===  lift m >> mzero
     rr (lift m `mplus` tma)  ===  lift m `mplus` (rr tma)
       where rr tm      =   msplit tm >>= reflect

One can read mzero and mplus as generalized list constructors [] and (:), and read (>>=) as a flipped application. The more complex laws assure that effects are not duplicated. It is fair to say that whereas foldr/build and destroy/unfoldr fusion techniques work for Haskell lists, msplit/reflect in the LogicT paper is a fusion law for a general backtracking computation over arbitrary, perhaps even strict, base monad. That computation may look nothing like list; in fact, the LogicT paper gives an example with delimited continuations, with abort playing the role of nil and shift the role of cons.

Version
The current version is 1.3, September 2010.
References
LogicT.pdf [186K]
Backtracking, Interleaving, and Terminating Monad Transformers
The Functional Pearl paper with Chung-chieh Shan, Daniel P. Friedman and Amr Sabry, presented at ICFP 2005.

LogicT.tar.gz [12K]
The Haskell code accompanying the paper
The code includes two implementations of LogicT: based on the two-continuation model of streams, and the direct-style implementation with first-class delimited continuations, using CCCxe or CCExc libraries. The code has two larger examples: Missionaries and cannibals problem, and playing Tic-Tac-Toe with minimax search and two heuristics. The latter code is rather heavily based on the code by Andrew Bromage.

Generators and LogicT

How to take a tail of a functional stream
A brief and de-sugared explanation of splitting a functional stream

Josef Svenningsson: Shortcut Fusion for Accumulating Parameters and Zip-like Functions. Proc. ICFP'02, 2002, pp. 124-132.

 

Simple fair and terminating backtracking Monad Transformer

The present code is an implementation of MonadPlus and the MonadPlus transformer with fair conjunctions and disjunctions and with distinct good termination properties. This implementation terminates whereas more conventional MonadPlus realizations (e.g., the List monad) diverge. Here's an example:
     pythagorean_triples :: MonadPlus m => m (Int,Int,Int)
     pythagorean_triples = do
         let number = (return 0) `mplus` (number >>= (return . (+1)))
         i <- number
         guard $ i > 0
         j <- number
         guard $ j > 0
         k <- number
         guard $ k > 0
         guard $ i*i + j*j == k*k
         return (i,j,k)
     test = take 7 $ runM Nothing pythagorean_triples
We stress that i, j, and k are all infinite streams of numbers. If we run this example with the standard List monad or with list comprehensions, divergence is imminent, because the backtracking ``gets stuck'' on k. Our fair stream implementation terminates. Our implementation also terminates and gives a stream of non-trivial answers if we remove the i>0 guards and make number to be left-recursive. See the example at the end of the source code.

The function runM :: Maybe Int -> Stream a -> [a] of our monad takes an extra argument: runM (Just n) m runs the computation m for at most n ``backtracking'' steps. This limit is another way to improve termination.

In the present monad the laws are satisfied modulo the order of the answers: we should treat the result of runM as a multi-set rather than a list. This issue is discussed in the LogicT paper.

I used to think that this monad is less capable than those described in the LogicT paper. It turns out that FBackTrackT implements the LogicT interface -- rather trivially. Thus FBackTrackT is an implementation of LogicT, with quite a good performance.

Version
The current version is 1.1.0.1, Oct 31, 2005; added LogicT: January 2014.
References
FBackTrack.hs [3K]
The complete Haskell source code for the plain monad, and an example.

FBackTrackT.hs [6K]
The corresponding monadic transformer (in Haskell98), with examples.

LogicT - backtracking monad transformer with fair operations and pruning

 

Purely Functional Lazy Non-deterministic Programming

[The Abstract of the paper]
Functional logic programming and probabilistic programming have demonstrated the broad benefits of combining laziness (non-strict evaluation with sharing of the results) with non-determinism. Yet these benefits are seldom enjoyed in functional programming, because the existing features for non-strictness, sharing, and non-determinism in functional languages are tricky to combine.

We present a practical way to write purely functional lazy non-deterministic programs that are efficient and perspicuous. We achieve this goal by embedding the programs into existing languages (such as Haskell, SML, and OCaml) with high-quality implementations, by making choices lazily and representing data with non-deterministic components, by working with custom monadic data types and search strategies, and by providing equational laws for the programmer to reason about their code.

This is joint work Sebastian Fischer and Chung-chieh Shan.

Version
The current version is August 2011.
References
lazy-nondet.pdf [283K]
Purely functional lazy nondeterministic programming
Journal of Functional Programming 21(4-5):413--465, 2011.
Copyright Cambridge University Press 2011 doi:10.1017/S0956796811000189
This is the greatly extended, journal version of the paper first published in the Proc. of ICFP 2009, pp. 11-22.

GitHub/Hackage package of explicit sharing of monadic effects
< http://sebfisch.github.com/explicit-sharing/ >
explicit-sharing on Hackage
The ICFP paper derives and explains the code. The code is maintained by Sebastian Fischer.

Deriving1.hs [17K]
Executable small-step semantics based on an alternative set of laws
The laws of non-determinism with explicit sharing described in the paper are concise but not constructive because of pattern-matching on bottom. The present code introduces an alternative set of laws. The code implements small-step semantics of a small monadic language with non-determinism and sharing. The semantics is based on the oriented version of the alternative equational laws. The code is hence the proof that the laws are constructive.
The datatype MP a represents the syntax of the language. The clauses of the function step define the reduction relation, in the declarative form. The semantics is executable; there are functions to evaluate a term, observing intermediate results if desired. The code includes the extensive test suite.

HANSEI: Embedded Probabilistic Programming
Memoization of non-deterministic functions in HANSEI is implemented using thread-local storage, according to the principles explained in the paper.

Efficient Set monads
A different way to share possible intermediate results of non-deterministic computations.

 

Parameterized `monad'

The familiar State monad lets us represent computations with a state that can be queried and updated. The state must have the same type during the entire computation however. One sometimes wants to express a computation where not only the value but also the type of the state can be updated -- while maintaining static typing. We wish for a parameterized `monad' that indexes each monadic type by an initial (type)state and a final (type)state. The effect of an effectful computation thus becomes apparent in the type of the computation, and so can be statically reasoned about.
     class Monadish m where
         gret  :: a -> m p p a
         gbind :: m p q a -> (a -> m q r b) -> m p r b
Unlike the ordinary monads (where m is a type constructor of one argument), here m is a type constructor of three type arguments, p, q and a. The argument a is the type of values produced by the monadic computation. The two other arguments describe the type of the computation state before and after the computation is executed. As in ordinary monad, gbind is required to be associative and gret to be the left and the right unit of gbind. It is clear that all ordinary monads are particular case of Monadish. Like the ordinary class monad, Monadish is implementable in Haskell98.

The need for such a type-state indexed `monad' has been observed on many occasions. For example, we can introduce monadish LIO p q a where p and q are either Locked or Unlocked, representing the state of a particular lock. Just by looking at the type of a computation, we can see if the computation acquires the lock (its (inferred) type is LIO Unlocked Locked a), acquires and releases the lock (its type is LIO Unlocked Unlocked a), or does not use the lock (its type LIO p p a and polymorphic over p). It becomes easy to statically ensure that the lock can be released only if it is being held. The locking problem can also be solved with the ordinary monad (by defining a function like with_lock which uses the monad in a contra-variant position). The latter solution is more cumbersome, and becomes increasingly cumbersome as we wish to represent more complex effects, such as control effects due to delimited control operators with answer-type modification.

The variable state, parameterized `monad' has been thoroughly investigated by Robert Atkey, MSFP2006. The message below is an independent discovery.

Version
The current version is 1.1, Dec 18, 2006.
References
VarStateM.hs [5K]
The complete Haskell98 code defining the parameterized monad and using it to implement a variable-state monad and the IO-like monad that statically enforces a locking protocol
The first part of the code was originally posted as Simple variable-state `monad' on the Haskell mailing list on Mon Dec 18 00:02:02 EST 2006

Robert Atkey: Parameterised Notions of Computation. MSFP2006
< http://homepages.inf.ed.ac.uk/ratkey/param-notions.pdf >

Lightweight static resources, for safe embedded and systems programming
RealTime.hs [8K]
Using Monadish to statically track ticks so to enforce timing and protocol restrictions when writing device drivers and their generators

Delimited continuations with effect typing, full soundness, answer-type modification and polymorphism
The genuine shift/reset control operators are implemented in terms of the parameterized monad.

Matthieu Sozeau: Type-safe printf using delimited continuations, in Coq
< http://lambda-the-ultimate.org/node/2626 >
The implementation of the parameterized `monad' (called GMonad) in Coq. The Coq code not only defines the operations gret and gbind but also states their laws, which Coq will verify for each GMonad instance.

Lightweight monadic regions
Section 6 of the paper describes a Haskell library for manual resource management, where deallocation is explicit and safety is assured by a form of linear types. We implement the linear typing in Haskell with the help of phantom types and a parameterized monad to statically track the type-state of resources.

Linear and affine lambda-calculi
The tagless-final encoding uses the variable-state `monad' to track resources associated with bound variables, to enforce the linearity of variable references.

Tracking dynamic values in types

 

Monte Carlo Monad: arithmetic of "probabilistic numbers"

The following article discusses a (sub)language of ``fuzzy'', probabilistic numbers. The language lets us write ordinarily-looking arithmetic expressions; variables in these expressions however denote random values rather than numbers. A user can specify the exact shape of the probability distribution curve for each random quantity. Arithmetic expressions over fuzzy numbers often arise in physics and statistics. Physical quantities often cannot be described by a single number; rather they are random values, due to measurement errors or the very nature of the corresponding physical process. We can use the language of fuzzy numbers to automate the error analysis and to estimate the resulting distribution.

The problem is more complex than it appears. An apparent solution is to represent fuzzy numbers as distribution functions. Operator + should be generalized to take two distribution functions as arguments and yield the distribution function of the sum. Other arithmetical operators and functions should be lifted as well. As Jerzy Karczmarczuk noted, this naive approach is fraught with problems. For example, fuzzy numbers cannot be an instance of the Num class as the latter requires its members to belong to the Eq class; comparing functions is in general undecidable. A more immediate problem is that the arithmetic of distributions is far more complex. Distributions are not linear: the distribution of a sum is a convolution of the distributions of its terms. Division is especially troublesome, if the denominator has a non-zero probability of being zero.

The following article develops a different approach. The key insight is that we do not need to ``symbolically'' manipulate distributions. We represent a random variable by a computation, which, when executed, generates one number. If executed many times, the computation generates many numbers -- a sample of its distribution. We can lift the standard arithmetical operators and functions (including comparisons) to such computations, and write ordinarily-looking arithmetical expressions over these random computations. We can then execute the resulting expression many times and obtain a sample distribution of the resulting quantity. The sample lets us estimate the mathematical expectation, the variance and other moments of the resulting quantity. Our method is thus a Monte Carlo estimation of a complex distribution.

As an example, we compute the center and the variance of sqrt( (Lw - 1/Cw)^2 + R^2) which is the impedance of an electric circuit, with an inductance being a normal variable (center 100, variance 1), frequency being uniformly distributed from 10 through 20 kHz. Resistance is also uniformly distributed from 10 through 50 kOm and the capacitance has the square root of the normal distribution. (The latter is just to make the example more interesting.)

In the follow-up, summarizing article, Jerzy Karczmarczuk designed a complementary approach, based on approximating a distribution by linear combinations of normal distributions. The arithmetic of normal distributions is well-understood.

Version
The current version is 1.1, Oct 31, 2001.
References
random-var-monad.txt [6K]
Re: Non-local arithmetic. The article with the source code and examples, posted on a newsgroup comp.lang.functional on Wed, 31 Oct 2001 17:48:33 -0800.

Jerzy Karczmarczuk's summary article.

HANSEI: Embedded domain-specific language for probabilistic models and (nested) inference

 

How to prove monad laws

When introducing a new monad, it is not enough to define a type constructor and the bind, return operations. One has to prove the three monad laws: return is the left and right unit of bind, and bind is associative. Proving the associativity law is less straightforward.

The following article demonstrates proving associativity for a particular Error monad. Filinski's `star' notation and a variable-free formulation of the associativity law turned out quite helpful.

Version
The current version is 1.1, Sep 2, 2003.
References
proving-monad-laws.txt [4K]
The article with the complete proof. It was originally posted as Re: proving the monad laws on the Haskell mailing list on Tue, 2 Sep 2003 19:26:39 -0700 (PDT)

 

Monadic reflection and reification

A brief essay on Andrzej Filinski's paper ``Representing Monads'' (POPL 1994), discussing the interpretation of the bind operator in terms of reflection and reification of monadic effects.
Version
The current version is 1.1, Aug 26, 2003.
References
monadic-reflection.txt [3K]
The article was originally posted as Re: monads and reflection [was: overloading] on the newsgroup comp.lang.scheme on Tue, 26 Aug 2003 12:00:45 -0700

Scheme's multiple values as an effect
Another discussion of monadic reflection and reification.

 

A serially-numbering monad

We want to build trees such that every node is tagged with a unique integer. Ideally every term/node has to have its id associated with it at construction time. As the original poster remarked, ``An obvious way to implement it in this way is to have a collection of state which is passed along all the time to every function. But this seems rather tedious.''

Is there a way to solve the problem purely functionally and elegantly? The article proposes one solution. It relies on monads to effectively hide the counter that uniquely tags every node. Building a tagged tree now looks just as simple as building an untagged one. The counter variable is well-hidden. And yet it is there, invisibly threading through all computations.

Version
The current version is 1.1, Oct 9, 2001.
References
numbered-monad.txt [4K]
The article with the source code. It was originally posted as Re: How to do this functionally? on the newsgroup comp.lang.functional on Tue, 9 Oct 2001 22:42:03 -0700
The discussion thread shows, in particular, an implementation of the serially-numbering monad in terms of GHC's State monad.


Last updated January 1, 2014

This site's top page is http://okmij.org/ftp/

oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML