"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)
#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

#haskell

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.

#haskell

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

@Shamar

Do you mean an article about BB encoding, or about lambda calculus?

@alice

Follow

@wim_v12e

Well... actually lambda calculus AND bb encoding. But I'm quite familiar with lambda calculus and I see that BB encoding can enhance what you can do with it.

@alice

@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

Sign in to participate in the conversation
Qoto Mastodon

QOTO: Question Others to Teach Ourselves
An inclusive, Academic Freedom, instance
All cultures welcome.
Hate speech and harassment strictly forbidden.