tail
of a functional streamforall a. ((a->a)->a->a)
is exactly the set
of encoded natural numbers. Polymorphic types become ``a system
of notation to describe data structures''. Furthermore, the encoding
commutes with operations on data types: it is an isomorphism. In
modern terms, they showed how to construct an initial algebra of a
strictly-positive functor using a set of System F terms as a carrier.
Boehm-Berarducci encoding is often confused with Church
encoding. First of all, Church encoding, which represents data types
in an untyped lambda-calculus, is not tight. Without types, it is
impossible to separate lambda-terms that encode some data type, from
those that represent no data type. The main distinction between the two
approaches is subtle. In a word, Church encoding only describes
introductions whereas Boehm-Berarducci also define elimination, or
pattern-matching, on encoded data types. For example, the list [1,2]
is represented in either encoding as a term \f x -> f 1 (f 2 x)
. It
is easy to write the head
function, which applied to the above
lambda-term returns 1
. It is much harder to write the tail
function, which applied to the above term returns \f x -> f 2 x
, the
encoding of [2]
. The reader may wish to pause and try writing tail
. The solution, which is the generalization of the predecessor
function on Church numerals, seems ad hoc. It is not clear how to
extend it to the encodings of various trees and to make it automatic.
Boehm and Berarducci were
the first to show `the trick', the systematic method of writing
pattern-matching functions on encodings of any algebraic data type.
Boehm-Berarducci's paper has many great insights. Alas, the generality of the presentation makes the paper very hard to understand. It has a Zen-like quality: it is incomprehensible unless you already know its results. I have understood the translation of pattern-matching because I have re-discovered `the trick' independently and was specifically looking for it in the paper. This article is an attempt to explain and illustrate the main ideas of the paper on a simple example.
Recall, Boehm-Berarducci encoding translates algebraic data types and the operations on them into System F, which contains only abstractions and applications and base type constants. The encoding applies only to what is now called `strictly positive' data types: there are no functions in the domain of constructors. (See Remark 1.1 (d) in Boehm-Berarducci's paper). For example, the encoding does not apply to the data type representing lambda-calculus terms in the higher-order abstract syntax. The encoding represents recursive (inductive, to be precise) data types as System F terms with non-recursive, but higher-rank types. Informally, the encoding replaces type-level primitive recursion with term-level primitive recursion and higher-rank type, of the order at most two. The encoding can be implemented in OCaml or Haskell, both of which support higher-rank types. As we shall see, the encoding has a severe performance problem due to the repeated decoding/re-encoding.
Philip Wadler: Recursive types in polymorphic lambda calculus
Message on the Types mailing list inquiring of the origin of the encoding, posted on Fri, 14 May 1999 15:24:32 -0400
< http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00138.html >
How to take a tail
of a functional stream
Application of Boehm-Berarducci encoding to co-inductive data types
Exp
data type
from the tagless-final lectures. The data type represents expressions of a
trivial `domain-specific language' of additions and negations of
integers.data Exp = Lit Int | Neg Exp | Add Exp ExpWe construct a sample term:
ti1 = Add (Lit 8) (Neg (Add (Lit 1) (Lit 2)))Our sample
Exp
consumer shows Exp
values as a string. The
function is structurally recursive, relying on
pattern-matching to deconstruct its Exp
argument. The
comments after ti1_view
show the result of viewing the sample
term.view:: Exp -> String view (Lit n) = show n view (Neg e) = "(-" ++ view e ++ ")" view (Add e1 e2) = "(" ++ view e1 ++ " + " ++ view e2 ++ ")" ti1_view = view ti1 -- "(8 + (-(1 + 2)))"
A sample term transformer pushes the negation down, converting terms to a `negative normal form', in which only literals can be negated, and only once. The code still uses pattern-matching, but it is not structurally recursive (see the last-but-one clause).
push_neg :: Exp -> Exp push_neg e@Lit{} = e push_neg e@(Neg (Lit _)) = e push_neg (Neg (Neg e)) = push_neg e push_neg (Neg (Add e1 e2)) = Add (push_neg (Neg e1)) (push_neg (Neg e2)) push_neg (Add e1 e2) = Add (push_neg e1) (push_neg e2)Here are a few sample transformations and their results (shown in comments).
ti1_norm = push_neg ti1 ti1_norm_view = view ti1_norm -- "(8 + ((-1) + (-2)))" -- Add an extra negation ti1n_norm_view = view (push_neg (Neg ti1)) -- "((-8) + (1 + 2))"
Exp
is defined in two
steps. First we clarify the signature of the Exp
algebra: the types
of the algebra constructors. A non-recursive Haskell record
well represents the signature:data ExpDict a = ExpDict{ dlit :: Int -> a, dneg :: a -> a, dadd :: a -> a -> a }A version of Boehm-Berarducci encoding could be just this:
type ExpBB1 = forall a. (ExpDict a -> a)Although we got rid of the type-level recursion replacing it with rank-2, we did not get rid of data types. The result ought to contain only (term and type) applications and abstractions. To this end, we curry the record argument:
newtype ExpBB = ExpBB{unExpBB :: forall a. ((Int -> a) -> (a -> a) -> (a -> a -> a) -> a)}
ExpBB
is the type of the encoded data type Exp
.
The newtype
wrapper lets us notate System F's type abstractions and
applications: the occurrences of the ExpBB
constructor
correspond to type abstractions, unExpBB
notates type applications.
A data type declaration defines a new type, data constructors
(introductions), deconstructors (elimination), and the induction
principle (fold). Likewise, we introduced the type ExpBB
of
the encoded Exp
values; the type immediately tells us the types of
the constructors, the signature. The constructors:
lit :: Int -> ExpBB lit x = ExpBB $ \dlit dneg dadd -> dlit x neg :: ExpBB -> ExpBB neg e = ExpBB $ \dlit dneg dadd -> dneg (unExpBB e dlit dneg dadd) add :: ExpBB -> ExpBB -> ExpBB add e1 e2 = ExpBB $ \dlit dneg dadd -> dadd (unExpBB e1 dlit dneg dadd) (unExpBB e2 dlit dneg dadd)make it clear that the values of
ExpBB
are the folds
over Exp
: the encoding of a value exp :: Exp
is the term
\lit neg add -> fold_Exp lit neg add exp :: ExpBB
where fold_Exp
is
the induction principle (fold) associated with the Exp
algebra.A sample term
tbb1 = add (lit 8) (neg (add (lit 1) (lit 2)))looks the same as the sample
Exp
term ti1
modulo the
capitalization of the constructors.
We can already write the view
-like consumer of the encoded values:
viewBB:: ExpBB -> String viewBB e = unExpBB e dlit dneg dadd where dlit n = show n dneg e = "(-" ++ e ++ ")" dadd e1 e2 = "(" ++ e1 ++ " + " ++ e2 ++ ")" tbb1v = viewBB tbb1 -- "(8 + (-(1 + 2)))"The function
view :: Exp -> String
was structurally recursive: it
was the instance of the fold over Exp
. Since Boehm-Berarducci
encoding of Exp
is the fold, viewBB
merely needs to instantiate
it. Unlike view
of Exp
, viewBB
is not recursive: the iteration
is driven by the input ExpBB
value itself. Boehm and Berarducci
call the functions like view
iterative (see Sec 2.1 in their paper).
For an iterative function f
on the algebraic data type, they give
a mechanical procedure of re-writing the definition of f
into the
definition of the corresponding function on the encoded data type: see
``program synthesis'' in Section 5. The code for viewBB
came from
the mechanical re-writing of the code for view
.
How to deal with Exp
functions that are not folds, that is, are not
structurally recursive? How to define a general deconstructor on
ExpBB
values, and so to write operations on ExpBB
using a sort of
`pattern-matching'? Boehm and Berarducci turns out to answer that
question too. Alas, that answer is only understandable after an
independent rediscovery. Hopefully the following is an
easier-to-understand explanation of the pattern-matching on ExpBB
.
To build intuition, we step back to the signature of the Exp
algebra,
ExpDict
, and specify it differently, in the form of a
strictly-positive functor (a functor built from constants,
sums and products):
data ExpF a = FLit Int | FNeg a | FAdd a a
Clearly ExpF
specifies the names and types of Exp
constructors
just as well as ExpDict
does. We then define two functions with
characteristic names:
roll :: ExpF ExpBB -> ExpBB roll (FLit n) = lit n roll (FNeg e) = neg e roll (FAdd e1 e2) = add e1 e2 unroll :: ExpBB -> ExpF ExpBB unroll e = unExpBB e dlit dneg dadd where dlit :: Int -> ExpF ExpBB dlit n = FLit n dneg :: ExpF ExpBB -> ExpF ExpBB dneg e = FNeg (roll e) dadd :: ExpF ExpBB -> ExpF ExpBB -> ExpF ExpBB dadd e1 e2 = FAdd (roll e1) (roll e2)The names
roll
and unroll
meant to evoke the witnesses of
the isomorphism between an iso-recursive type and its one-step unrolling.
These functions are present in the Boehm-Berarducci's paper, in a
somewhat hidden way. We may observe that roll
and unroll
, as befits
isomorphism witnesses, are inverses of each other. For example,
roll . unroll
is extensionally equivalent to the identity.
That is, for any concrete value x :: ExpBB
built by the constructors
lit
, neg
and add
, roll (unroll x)
is x
-- which can be proven
by induction on the construction of x
. In the paper,
the extensional equivalence of roll . unroll
and the identity
is essentially stated in Eq. (*) in Section 7. Clearly
roll . unroll
is not intensionally the identity,
since no sequence of beta- and eta- reductions can bring
\x -> roll (unroll x)
to be the same as \x -> x
. Yet these
two terms are contextually observationally equivalent. (Boehm and Berarducci
introduce the symbol ~=
for this equivalence, noting that
characterizing it is an open problem.)
The function unroll
that essentially exposes the `top-level' constructors
of an ExpBB
values tells us how to define the ExpBB
deconstructor,
systematically.
newtype ExpD = ExpD{unED :: forall w. (Int -> w) -> (ExpBB -> w) -> (ExpBB -> ExpBB -> w) -> w} decon :: ExpBB -> ExpD decon e = unExpBB e dlit dneg dadd where dlit n = ExpD $ \onlit onneg onadd -> onlit n dneg e = ExpD $ \onlit onneg onadd -> onneg (unED e lit neg add) dadd e1 e2 = ExpD $ \onlit onneg onadd -> onadd (unED e1 lit neg add) (unED e2 lit neg add)The higher-rank type
ExpD
, the return type of the deconstructor,
is subtly but crucially different from ExpBB
. Informally,
an ExpBB
value unfolds all the way whereas ExpD
unfolds only one
step.
As an illustration of the deconstructor, we re-write viewBB
with
`pattern-matching', or deconstruction:
viewBBd:: ExpBB -> String viewBBd e = unED (decon e) dlit dneg dadd where dlit n = show n dneg e = "(-" ++ viewBBd e ++ ")" dadd e1 e2 = "(" ++ viewBBd e1 ++ " + " ++ viewBBd e2 ++ ")"The code looks pretty much like the original
view
. The real payoff
of the deconstructor is being able to re-write the non-structurally recursive
push_neg
to operate on the encoded ExpBB
:push_negBB :: ExpBB -> ExpBB push_negBB e = unED (decon e) dlit dneg dadd where dlit _ = e dneg e2 = unED (decon e2) dlit2 dneg2 dadd2 where dlit2 n = e dneg2 e = push_negBB e dadd2 e1 e2 = add (push_negBB (neg e1)) (push_negBB (neg e2)) dadd e1 e2 = add (push_negBB e1) (push_negBB e2) tbb1_norm = push_negBB tbb1 tbb1_norm_viewBB = viewBBd tbb1_norm -- "(8 + ((-1) + (-2)))"The function
push_negBB
looks quite like the original push_neg
, down
to nested `pattern-matching'.
Meditation on roll
and unroll
reveals inefficiency:
unroll
-ing the value neg (neg (neg ... (lit 1)))
with N neg
constructors involves N
roll
s. A single deconstruction
of an ExpBB
value takes time proportional to the total size of the
value (the number of constructors used to build the value).
The function viewBBd
that does repeated deconstruction has the
quadratic complexity in the size of the value.
BoehmBerarducci.ml [4K]
The OCaml code for a similar example
roll
and unroll
particularly
elegant, helps us see the encoding as the initial
algebra, and connects the encodings with continuations and streams.
We have already mentioned that the signature of the Exp
algebra --
the names and the types of its constructors -- are equally well
specified by the data type ExpDict a
or by ExpF a
(beside the Exp
data type itself; Exp
is recursive however). The connection goes deeper:
ExpDict a
and ExpF a -> a
are isomorphic. Here are the witnesses.
sigma_dict :: (ExpF a -> a) -> ExpDict a sigma_dict sigma = ExpDict{ dlit = \n -> sigma (FLit n), dneg = \e -> sigma (FNeg e), dadd = \e1 e2 -> sigma (FAdd e1 e2) } dict_sigma :: ExpDict a -> (ExpF a -> a) dict_sigma dict (FLit n) = dlit dict n dict_sigma dict (FNeg e) = dneg dict e dict_sigma dict (FAdd e1 e2) = dadd dict e1 e2The operations of an
Exp
algebra with the carrier U
can be specified either as an ExpDict U
value,
or in the form of a function ExpF U -> U
. Earlier we have mentioned the
uncurried form of Boehm-Berarducci encoding:type ExpBB1 = forall a. (ExpDict a -> a)which gives rise to the following equivalent form of the encoding
newtype ExpC = ExpC{unExpC :: forall a. (ExpF a -> a) -> a}whose connections with continuations are hard to miss. Let us write the constructors explicitly:
sigma_expC :: ExpF ExpC -> ExpC sigma_expC (FLit n) = ExpC $ \f -> f (FLit n) sigma_expC (FNeg e) = ExpC $ \f -> f (FNeg (unExpC e f)) sigma_expC (FAdd e1 e2) = ExpC $ \f -> f (FAdd (unExpC e1 f) (unExpC e2 f))
The encoding ExpC
is fully equivalent to ExpBB
, and
inter-convertible. It is not mentioned in the Boehm-Berarducci's paper
since its definition contains the data type ExpF a
. Boehm and Berarducci's
program was to encode data types in lambda-terms only.
One advantage of ExpC
is giving to the functions roll
and unroll
a particularly elegant, revealing form:
rollC :: ExpF ExpC -> ExpC rollC = sigma_expC unrollC :: ExpC -> ExpF ExpC unrollC e = unExpC e (fmap sigma_expC)The definition of
unrollC
is well worth contemplating.
The algebra with the carrier ExpC
and the operations
sigma_ExpC
is the initial algebra of the functor ExpF
.
For an arbitrary ExpF
algebra with the carrier U
and the operations sigma :: ExpF U -> U
there exists
a unique homomorphism (hc sigma) :: ExpC -> U
, such that the
hc sigma . sigma_ExpC = sigma . fmap (hc sigma)
. A simple case
analysis indeed gives us the unique expression for hc
:
hc :: (ExpF a -> a) -> ExpC -> a hc sigma e = unExpC e sigma
The unique homomorphism is not only elegant but also practical. If we define
an ExpF
algebra with String
as the carrier and the following operations
sigma_view :: ExpF String -> String sigma_view (FLit n) = show n sigma_view (FNeg e) = "(-" ++ e ++ ")" sigma_view (FAdd e1 e2) = "(" ++ e1 ++ " + " ++ e2 ++ ")"we immediately obtain the function to view
ExpC
values:viewC :: ExpC -> String viewC = hc sigma_view
We have shown that the modified, and hence the original Boehm-Berarducci encoding is the initial algebra. The modification gave the operation of peeling off one level of `constructors' an insightful form. The modification paves way to connecting the encoding with co-algebras.
tail
of a functional streamnewtype FStream a = SFK (forall ans. SK a ans -> FK ans -> ans) type FK ans = () -> ans -- failure continuation type SK a ans = a -> FK ans -> ans -- success continuation newtype MFStream m a = MSFK (forall ans. MSK m a ans -> MFK m ans -> m ans) type MFK m ans = m ans -- failure continuation type MSK m a ans = a -> MFK m ans -> m ans -- success continuationthe question is obtaining several first elements of that stream. In general, the problem is to split a non-empty functional stream into the head element and the rest, which can be split again, etc. That rest must be a stream, of the type
MFStream m a
.
This is a far more difficult problem than it may appear. One
may think that we merely need to convert the functional stream to a
regular, nil
/lazyCons
stream, for example:mfstream_to_stream:: (Monad m) => MFStream m a -> m (Stream a) mfstream_to_stream mfstream = unMSFK mfstream sk fk where fk = return Nil sk a fk' = fk' >>= (\rest -> return (Cons a (\ () -> rest)))However, if the monad
m
is strict (i.e., the bind
operator >>=
forces its first argument -- as it is the
case for the IO
monad, for example), then we must fully
convert the functional stream to the regular stream before we can
examine the first few elements. If the source functional stream is
infinite, mfstream_to_stream
diverges.
The code below explains the problem and shows the general
solution, which underlies the LogicT
monad transformer.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML