"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."
(okmij.org/ftp/tagless-final/co)

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

Show thread

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.

Show thread

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

Show thread

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.

Show thread

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.

Show thread
@wim_v12e So does that mean that the intuition behind Bœhm-Berarducci's encoding is «data not for themselves but to be used» ? A boolean as something to be tested on, a pair as something to be projected, etc. ?

@alice Yes, that's it. It's the basic idea used to make types etc starting from the lambda calculus.

@wim_v12e I had never seen the name before but the ideas look very familiar, I'm sure I have already seen somewhere else booleans encoded as a function to choose between the «then» and the «else» value.

@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.

@wim_v12e

I'd like to read such blog.
I like the idea a lot in particular because it does NOT play well with typeclasses.

BTW, you should also add an example of interpretation.

@alice

Follow

@Shamar @alice Just FYI, I finally wrote that blog post (in two parts) about Boehm-Berarducci encoding of algebraic data types in Raku.

wimvanderbauwhede.github.io/ar

· · Web · 0 · 2 · 1
Sign in to participate in the conversation
Octodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!