LogicT - backtracking monad transformer with fair
operations and pruningMonadIO
do-notation for OCaml
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 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.
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 [15K]
The 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. 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.
The archive also includes the delimited continuation monad
transformer library by Amr Sabry, R. Kent Dybvig, Simon L. Peyton-Jones.
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.
The present code is an implementation of MonadPlus
and MonadPlus transformer with fair conjunctions and
disjunctions and with distinct good termination properties. For one
thing, this implementation terminates when more conventional MonadPlus realizations (e.g., the
List monad) diverge. For example, we can write:
pythagorean_triples :: MonadPlus m => m (Int,Int,Int)
pythagorean_triples =
let number = (return 0) `mplus` (number >>= (return . (+1))) in
do
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 must stress that i, j, and k are all infinite streams of numbers. If we use this
example with the standard List monad or with list
comprehensions, divergence is imminent, because 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.
This monad is far less capable than the LogicT
monad. It does a lot of tagging, which is eliminated in the
continuation-passing 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
of runM as a multi-set rather than a list. This issue is
discussed in the LogicT paper.
FBackTrack.hs [3K]
The complete Haskell source code for the plain monad, and an
example.
FBackTrackT.hs [5K]
The corresponding monadic transformer (in Haskell98), with
examples.
The Scheme implementation, as another evaluator for mini-Kanren. See testsi.scm in the same project directory for extensive tests.
LogicT - backtracking monad transformer with fair
operations and pruningCartwright and Felleisen have described a technique for composing interpreters that is an alternative to monad transformers. One particular advantage of their technique (hereafter, EDLS) is that the order of composing interpreters, where it is irrelevant, does not have to be specified at all. In fact, unlike monad transformers, we do not have to commit to a single, statically determined order of sub-interpreters. More importantly, object programs are written in the `direct' rather than the monadic (that is, barely hidden continuation-passing) style. Continuation-passing style has many known usability and performance problems. Cartwright and Felleisen's approach also has a theoretical advantage of providing so-called `stable denotations' for expressions (please see their paper for the precise definition). The abstract and page 2 of EDLS paper are particularly insightful.
Cartwright and Felleisen's paper appeared just a bit prior to Liang, Hudak and Jones' ``Monad Transformers and Modular interpreters'' that introduced monad transformers. In fact, the monad transformers paper mentions Cartwright and Felleisen's direct approach in footnote 1. Perhaps because Cartwright and Felleisen demonstrate their approach in an obscure dialect of Scheme, their work did not receive nearly as much attention as it vastly deserves.
We implement the enhanced EDLS in Haskell and add delimited control. To be precise, we implement the Base interpreter (whose sole operations are Loop and Error) and the following extensions: CBV lambda-calculus, Arithmetic, Storage, Control. The extensions can be added to the Base interpreter in any order and in any combination.
Our implementation has the following advantages over EDLS:
Our main departure from EDLS is is the removal of the `central authority'. There is no semantic `admin' function. Rather, admin is part of the source language and can be used at any place in the code. The `central authority' of EDLS must be an extensible function, requiring meta-language facilities to implement (such as quite non-standard Scheme modules). We do not have central authority. Rather, we have bureaucracy: each specific effect handler interprets its own effects as it can, throwing the rest `upstairs' for higher-level bureaucrats to deal with. Extensibility arises automatically.
We take the meaning of a program to be the union of Values and (unfulfilled) Actions. If the meaning of the program is a (non-bottom) value, the program is terminating. If the meaning of the program is an Action -- the program finished with an error, such as an action to access a non-existing storage cell, or shift without reset, or a user-raised error.
EDLS says, at the very top of p. 3, that the handle in the effect message ``is roughly a conventional continuation.'' Because the admin of EDLS is `outside' of the program (at the point of infinity, so to speak), its continuation indeed appears undelimited. By making our `admin' part of the source language, we recognize the handle in the effect message for what it is: a delimited continuation.
Robert Cartwright, Matthias Felleisen: Extensible Denotational Language Specifications
Symposium on Theoretical Aspects of Computer Software, 1994. LNCS 789, pp. 244-272.
<http://citeseer.ist.psu.edu/69837.html>
ExtensibleDS.hs [17K]
The complete code in Haskell98 (plus pattern guards), including several examples.
This code is not written in idiomatic Haskell and does not take
advantage of types at all. The ubiquitous projections from the
universal domain tantamount to ``dynamic typing.'' The code is
intentionally written to be close to the EDLS paper, emphasizing
denotational semantics, whose domains are untyped. One can certainly
do better, for example, employ user-defined datatypes for tagged
values, avoiding the ugly string-tagged values.
[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.
lazy-nondet.pdf [192K]
In Proceedings of the international conference on functional
programming, ICFP09, pp. 11-22, 2009.
GitHub/Hackage package of explicit sharing of monadic effects
<http://sebfisch.github.com/explicit-sharing/>
<http://hackage.haskell.org/cgi-bin/hackage-scripts/package/explicit-sharing>
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 ICFP paper.
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 arithmetics 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 paper 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. I admit, the latter is just to make the example more interesting.
In a follow-up, summarizing article, Jerzy Karczmarczuk designed a complementary approach, based on approximating a distribution by linear combinations of normal distributions. The arithmetics of normal distributions is well-understood.
Re: Non-local arithmetic. [plain text file]
The article with the source code and examples, posted on a newsgroup comp.lang.functionalon Wed, 31 Oct 2001 17:48:33 -0800.
Jerzy Karczmarczuk's summary article.
HANSEI: Embedded domain-specific language for probabilistic models and (nested) inference
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.
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.
When introducing a new monad, it is not enough to define a type
constructor and 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.
bind
operator in terms of reflection and reification of monadic
effects.The article [plain text file]
It was originally posted as Re: monads and reflection [was: overloading] on a 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.
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.
The article with the source code. [plain text file]
The article itself. It was originally posted as Re:
How to do this functionally? on a newsgroup comp.lang.functional on Tue, 9 Oct 2001 22:42:03 -0700
Google's article discussion thread shows, in particular, an
implementation of the serially-numbering monad in terms of a State monad. The latter is a part of a MonadState module
distributed with GHC.
This site's top page is http://pobox.com/~oleg/ftp/
Converted from SXML by SXML->HTML