LogicT- backtracking monad transformer with fair operations and pruning
do-notation for OCaml
LogicT- backtracking monad transformer with fair operations and pruning
MonadPlusinterface, 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
destroy, internally using regular list constructors to split a
However, the present function
significantly more general: it has nothing to do with Haskell lists
and never uses any lists constructors, even internally. The functions
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
generalized list constructors
(>>=) 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
abort playing the role of
the role of
The Haskell code accompanying the paper
The code includes two implementations of
based on the two-continuation model of streams, and the direct-style
implementation with first-class delimited continuations, using
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.
MonadPlustransformer with fair conjunctions and disjunctions and with distinct good termination properties. This implementation terminates whereas more conventional
MonadPlusrealizations (e.g., the
Listmonad) 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_triplesWe stress that
kare all infinite streams of numbers. If we run this example with the standard
Listmonad 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>0guards and make
numberto be left-recursive. See the example at the end of the source code.
runM :: Maybe Int -> Stream a -> [a]
of our monad takes an extra argument:
runM (Just n) m
runs the computation
m for at most
``backtracking'' steps. This limit is another way to improve
This monad is less capable than the
monad. It does a lot of tagging, which is eliminated in the
LogicT. On the other hand, this fair
stream monad is rather simple. Also, in the present monad the laws are
satisfied modulo the order of the answers: we should treat the result
runM as a multi-set rather than a list. This issue is
discussed in the LogicT paper.
The corresponding monadic transformer (in Haskell98), with examples.
LogicT - backtracking monad transformer with fair operations and pruning
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.
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.
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.
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.
class Monadish m where gret :: a -> m p p a gbind :: m p q a -> (a -> m q r b) -> m p r bUnlike the ordinary monads (where
mis a type constructor of one argument), here
mis a type constructor of three type arguments,
a. The argument
ais 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,
gbindis required to be associative and
gretto 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
q are either
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
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
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.
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
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
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
The problem is more complex than it appears. An apparent
solution is to represent fuzzy numbers as distribution
+ 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.
Jerzy Karczmarczuk's summary article.
HANSEI: Embedded domain-specific language for probabilistic models and (nested) inference
returnoperations. One has to prove the three monad laws:
returnis the left and right unit of
bindis 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.
bindoperator in terms of reflection and reification of monadic effects.
Scheme's multiple values as an effect
Another discussion of monadic reflection and reification.
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.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML