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

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

Follow

@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