previous   next   up   top

Beyond Church encoding: Boehm-Berarducci isomorphism of algebraic data types and polymorphic lambda-terms

 


 

Introduction

In 1985, Corrado Boehm and Alessandro Berarducci published the encoding of strictly-positive algebraic data types in polymorphic lambda-calculus (System F). They showed how to systematically, automatically translate operations on data types -- construction and especially pattern-matching -- into the target language that has only applications and abstractions. They proved that the encoding is one-to-one and onto: it encodes all strictly-positive algebraic data types with no junk. For example, the set of all closed normal terms of the type forall 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.

Version
The current version is April 2012.
References
Corrado Boehm and Alessandro Berarducci: Automatic Synthesis of Typed Lambda-Programs on Term Algebras
Theoretical Computer Science, 1985, v39, pp. 135--154.

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

 

Baseline: operating on an algebraic data type

We start with a baseline, a typical example of defining an algebraic data type and constructing, deconstructing and transforming its values. Later on we re-write the example using Boehm-Berarducci encoding of the data type. Our running example is the 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))"
Version
The current version is April 2012.
References
BB_ADT.hs [2K]
The complete Haskell code for the example

 

Operating on the encoded algebraic data type

We re-write the algebraic data type baseline example using Boehm-Berarducci encoding to represent the data type as lambda-terms. The encoding of the data type 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.

Version
The current version is April 2012.
References
BB_LAM.hs [9K]
The complete Haskell code for the example

BoehmBerarducci.ml [4K]
The OCaml code for a similar example

 

The encoding as the initial algebra

A slight modification to the encoding gives a deep algebraic insight. This modification is not present in Boehm and Berarducci's paper, since it is a bit out of scope of their translation of data types to lambda-terms. The modified encoding however is isomorphic to the original one. The modification makes 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.

Version
The current version is April 2012.
References
BB_LAM.hs [9K]
The complete Haskell code for the example

 

How to take a tail of a functional stream

We show the application of Boehm-Berarducci encoding to a co-algebraic data type: stream. Boehm-Berarducci constructors cannot build an infinite stream without resorting to general recursion. However, Boehm-Berarducci deconstructors apply as they are to deconstructing/transforming the stream, even the infinite one. Given the following functional stream or its monadic version:
     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.

Version
The current version is 1.2, Jul 4, 2005.
References
car-fstream.lhs [6K]
Literate Haskell code with examples and explanation.

How to zip folds: A library of fold transformers (streams)

Fair and expressive backtracking monad transformer



Last updated April 5, 2012

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