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 Exp
We 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 rolls. 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 e2
The 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 stream newtype 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 continuation
the 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-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML