"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."
(http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html)
#haskell
With that warning, here is my implementation of a Maybe type in Boehm-Berarducci encoding:
newtype MayBB b = MayBB {
unMayBB :: forall a .
(b -> a)
-> a
-> a
}
and I think it's beautiful.
With these little helpers:
just x = \j' n' -> j' x
nothing = \j' n' -> n'
we get the following:
-- Plain Maybe
mb :: Maybe Int
mb = Just 42
mbn :: Maybe Int
mbn = Nothing
-- BB Maybe
mbb:: MayBB Int
mbb = MayBB $ just 42
mbbn :: MayBB Int
mbbn = MayBB nothing
And why do I think this is nice? Because I have encoded a sum type:
data Maybe b = Just b | Nothing
as a single function type which, if anything, is more like a product type. The record type syntax is just to provide a label for easy access to the function.
There are other reasons why the Boehm-Berarducci encoding, but first I'd like to give another example: the encoding of the Boolean type
data Bool = True | False
is
newtype BoolBB =
BoolBB (forall a . a -> a -> a)
So this is a function of two arguments that returns something of the same type. With two selectors very similar to those for Maybe:
true = \t f -> t
false = \t f -> f
we can write
trueBB = BoolBB true
falseBB = BoolBB false
We can also encode product types in this way:
newtype PairBB t1 t2 =
PairBB {
unPairBB :: forall a .
(t1 -> t2 -> a) -> a
}
fst p = unPairBB p (\x y -> x)
snd p = unPairBB p (\x y -> y)
bbp = PairBB $ \p -> p 42 "forty-two"
That means that the BB encoding provides a way to represent algebraic data types as polymorphic functions.
Now you probably wonder, what good is all this anyway? Yu're thinking, "I'm a very busy man, I have other cases besides this one."
There are many uses for this encoding but what we are using it for is to compose interpreters. Essentially, if your algebraic data type represents an abstract syntax tree, then the BB encoding of it is a universal interpreter. Every particular implementation of the function is an interpreter, and they are composable.
@alice Yes, that's it. It's the basic idea used to make types etc starting from the lambda calculus.
@alice That's right. BB encoding is a generalisation of the approach to define things like conditionals, pairs, lists etc via the lambda calculus. I wrote something about this, "In a Functional Language, There are Only Functions", I'll put it on my blog if you're interested. But the BB encoding goes a bit further because it allows pattern matching, thanks to the `unBB` function and the forall-quantified type.
@Shamar @alice Here's my "Everything is a function" article:
https://wimvanderbauwhede.github.io/articles/everything-is-a-function/
#haskell
@Shamar
I just asked because I realised my remark to Alice was a bit unclear. I wrote an article to illustrate that in a functional language you can reduce all building blocks to lambda functions. That is the one I am going to post soon.
I have not yet written anything on BB encoding but the things I posted here might be a good start so I think I'll do that too when I have some time.
@alice