"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.
@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
@Shamar @alice Here's my "Everything is a function" article:
https://wimvanderbauwhede.github.io/articles/everything-is-a-function/
#haskell
@Shamar @alice Just FYI, I finally wrote that blog post (in two parts) about Boehm-Berarducci encoding of algebraic data types in Raku.
https://wimvanderbauwhede.github.io/articles/universal-interpreter-part-1/
#rakulang
#functionalprogramming
@Shamar
Do you mean an article about BB encoding, or about lambda calculus?
@alice