{-# LANGUAGE Rank2Types #-}
-- The illustration of the Boehm-Berarducci encoding
-- We re-write an Algebraic Data Type example in BB_ADT.hs
-- using Boehm-Berarducci encoding to represent the
-- data type with lambda-terms.
-- Boehm-Berarducci encoding represents an inductive data type
-- as a non-recursive but higher-rank data type
module BB_LAM where
import BB_ADT (Exp(..))
-- We define the Boehm-Berarducci encoding of the data type
-- Exp from BB_ADT.hs in two steps.
-- First we clarify the signature of the Exp algebra: the
-- types of the algebra constructors. We represent the signature
-- as a Haskell record. It is NOT recursive.
-- (We have seen this record already, in BB_ADT.hs)
data ExpOps a = ExpOps{ olit :: Int -> a,
oneg :: a -> a,
oadd :: a -> a -> a }
-- On particular Exp algebra, with String as a carrier
view_ops :: ExpOps String
view_ops = ExpOps {
olit=show,
oneg = \e -> "(-" ++ e ++ ")",
oadd = \e1 e2 -> "(" ++ e1 ++ " + " ++ e2 ++ ")"}
-- We can define (a version of) Boehm-Berarducci encoding as
type ExpBB1 = forall a. (ExpOps a -> a)
-- To use only applications and abstractions, we curry the record
-- argument ExpOps a.
-- The wrapper newtype is needed for the first-class polymorphism
-- (actually we can go some way without newtype wrapper but eventually
-- GHC becomes confused. After all, the source language of GHC is not
-- system F.)
newtype ExpBB
= ExpBB{unExpBB :: forall a. ((Int -> a) -> (a -> a) -> (a -> a -> a) -> a)}
-- A data type declaration defines type, constructors, deconstructors
-- and the induction principle (fold). We already have a new type ExpBB,
-- which represents fold, as will become clear soon. We need constructors:
lit :: Int -> ExpBB
lit x = ExpBB $ \onlit onneg onadd -> onlit x
neg :: ExpBB -> ExpBB
neg e = ExpBB $ \onlit onneg onadd -> onneg (unExpBB e onlit onneg onadd)
add :: ExpBB -> ExpBB -> ExpBB
add e1 e2 = ExpBB $ \onlit onneg onadd ->
onadd (unExpBB e1 onlit onneg onadd) (unExpBB e2 onlit onneg onadd)
-- A sample expression: our first running example
tbb1 = add (lit 8) (neg (add (lit 1) (lit 2)))
-- Incidentally, we can group lit, neg and add into the ExpOps record
-- which shows that it is an Exp algebra, with the carrier ExpBB
bb_ops :: ExpOps ExpBB
bb_ops = ExpOps {olit = lit, oneg = neg, oadd = add}
-- A sample consumer
-- viewBB: can be implemented simply via the induction principle
-- It is not recursive!
-- Compare with BB_ADT.view'
viewBB:: ExpBB -> String
viewBB e = unExpBB e (olit view_ops) (oneg view_ops) (oadd view_ops)
tbb1v = viewBB tbb1
-- "(8 + (-(1 + 2)))"
-- Since bb_ops is also an algebra, we can use that too
-- For any term e, unExpBB e lit neg add === e
-- That is the famous equation (*) of the Boehm-Berarducci's paper
-- As a spot-check
tbb1v' = viewBB (unExpBB tbb1 (olit bb_ops) (oneg bb_ops) (oadd bb_ops))
-- How to define a deconstructor?
-- To give an intuition, we define the following functions roll and unroll.
-- The names meant to invoke terms witnessing the isomorphism between an
-- iso-recursive type and its one-step unrolling.
-- The deconstructor will use a form of these functions.
{- The following shows that we can replace type-level induction
(in BB_ADT.Exp) with a term-level induction.
The following definitions of roll and unroll are actually present
in Boehm-Berarducci's paper -- but in a very indirect way.
The crucial part is Defn 7.1: sort of self-interpreter: v cons nil ~= v
Informally, it shows that roll . unroll should be equivalent to the
identity. The equivalence relation (~=) is strictly speaking not
the equality; in modern terms, (~=) is contextual equivalence.
-}
-- First we re-write the signature of the Exp algebra, ExpDic,
-- in the form of a strictly-positive functor
data ExpF a = FLit Int
| FNeg a
| FAdd a a
instance Functor ExpF where
fmap f (FLit n) = FLit n
fmap f (FNeg e) = FNeg (f e)
fmap f (FAdd e1 e2) = FAdd (f e1) (f e2)
roll :: ExpF ExpBB -> ExpBB
roll (FLit n) = lit n
roll (FNeg e) = neg e
roll (FAdd e1 e2) = add e1 e2
-- The occurrence of roll below is the source of major inefficiency
-- as we do repeated pattern-matching.
unroll :: ExpBB -> ExpF ExpBB
unroll e = unExpBB e onlit onneg onadd
where
onlit :: Int -> ExpF ExpBB
onlit n = FLit n
onneg :: ExpF ExpBB -> ExpF ExpBB
onneg e = FNeg (roll e)
onadd :: ExpF ExpBB -> ExpF ExpBB -> ExpF ExpBB
onadd e1 e2 = FAdd (roll e1) (roll e2)
-- Compare with the signature for ExpBB!
-- Informally, ExpBB unfolds all the way whereas ExpD unfolds only one step
newtype ExpD =
ExpD{unED ::
forall w. (Int -> w) -> (ExpBB -> w) -> (ExpBB -> ExpBB -> w) -> w}
-- One may call ExpD a companion, deconstructing encoding. ExpD also represents
-- Exp values. ExpD values can be constructed just like ExpBB values,
-- as shown below.
-- The code for the following dlit, dneg and dadd looks very similar
-- to that for lit, neg, and add: but look closely!
dlit :: Int -> ExpD
dlit x = ExpD $ \onlit onneg onadd -> onlit x
dneg :: ExpD -> ExpD
dneg e = ExpD $ \onlit onneg onadd -> onneg (unED e lit neg add)
dadd :: ExpD -> ExpD -> ExpD
dadd e1 e2 = ExpD $ \onlit onneg onadd ->
onadd (unED e1 lit neg add) (unED e2 lit neg add)
-- The bonus is that ExpD values can be constructed mechanically, from
-- ExpBB values. Indeed, ExpBB embodies structural recursion (induction)
-- principle of the Exp data type. ExpD values are constructed
-- inductively, hence ExpBB can construct them
decon :: ExpBB -> ExpD
decon e = unExpBB e dlit dneg dadd
-- That transformation from ExpBB to ExpD is the deconstructor,
-- exposing the top-level constructor of Exp
-- We redo viewBB, using pattern-matching this time, and recursion
viewBBd:: ExpBB -> String
viewBBd e = unED (decon e) onlit onneg onadd
where
onlit n = show n
onneg e = "(-" ++ viewBBd e ++ ")"
onadd e1 e2 = "(" ++ viewBBd e1 ++ " + " ++ viewBBd e2 ++ ")"
tbb1vd = viewBBd tbb1
-- "(8 + (-(1 + 2)))"
-- So, we can do any pattern-matching!
-- And do non-structurally--recursive processing on ExpBB
{-
push_neg :: Exp -> Exp
push_neg e@Lit{} = e
push_neg e@(Neg (Lit _)) = e
push_neg (Neg (Neg e)) = push_neg e
push_neg (Neg (Add e1 e2)) = Add (push_neg (Neg e1)) (push_neg (Neg e2))
push_neg (Add e1 e2) = Add (push_neg e1) (push_neg e2)
-}
push_negBB :: ExpBB -> ExpBB
push_negBB e = unED (decon e) onlit onneg onadd
where
onlit _ = e
onneg e2 = unED (decon e2) onlit2 onneg2 onadd2
where
onlit2 n = e
onneg2 e = push_negBB e
onadd2 e1 e2 = add (push_negBB (neg e1)) (push_negBB (neg e2))
onadd e1 e2 = add (push_negBB e1) (push_negBB e2)
tbb1_norm = push_negBB tbb1
tbb1_norm_viewBB = viewBBd tbb1_norm
-- "(8 + ((-1) + (-2)))"
-- Add an extra negation
tbb1n_norm_viewBB = viewBBd (push_negBB (neg tbb1))
-- "((-8) + (1 + 2))"
-- ------------------------------------------------------------------------
-- A bit of algebra
-- The types (ExpF a -> a) and ExpOps a are isomorphic.
-- Hence, the operations of an Exp algebra with the carrier U
-- could be specified either in the form of a value of the type ExpOps U,
-- or in the form of a function ExpF U -> U.
sigma_dict :: (ExpF a -> a) -> ExpOps a
sigma_dict sigma = ExpOps{ olit = \n -> sigma (FLit n),
oneg = \e -> sigma (FNeg e),
oadd = \e1 e2 -> sigma (FAdd e1 e2) }
dict_sigma :: ExpOps a -> (ExpF a -> a)
dict_sigma ops (FLit n) = olit ops n
dict_sigma ops (FNeg e) = oneg ops e
dict_sigma ops (FAdd e1 e2) = oadd ops e1 e2
-- Recall ExpBB1 as an uncurried form of the Boehm-Berarducci encoding.
-- It follows then the encoding can be written in the equivalent form
newtype ExpC = ExpC{unExpC :: forall a. (ExpF a -> a) -> a}
-- ExpC is indeed fully equivalent to ExpBB, and inter-convertible
h :: ExpOps a -> ExpBB -> a
h ops e = unExpBB e (olit ops) (oneg ops) (oadd ops)
exp_BB_C :: ExpBB -> ExpC
exp_BB_C e = ExpC $ \f -> h (sigma_dict f) e
exp_C_BB :: ExpC -> ExpBB
exp_C_BB e = ExpBB $ \olit oneg oadd ->
unExpC e (dict_sigma (ExpOps olit oneg oadd))
-- Let us write the constructors explicitly:
sigma_expC :: ExpF ExpC -> ExpC
sigma_expC (FLit n) = ExpC $ \f -> f (FLit n)
sigma_expC (FNeg e) = ExpC $ \f -> f (FNeg (unExpC e f))
sigma_expC (FAdd e1 e2) = ExpC $ \f -> f (FAdd (unExpC e1 f) (unExpC e2 f))
-- Sample term
t1c = exp_BB_C tbb1
-- The advantage of ExpC is that functions roll and unroll take
-- a particularly elegant form
rollC :: ExpF ExpC -> ExpC
rollC = sigma_expC
unrollC :: ExpC -> ExpF ExpC
unrollC e = unExpC e (fmap sigma_expC)
-- (ExpC, sigma_ExpC) is the initial algebra of the functor ExpF.
-- (the same holds for ExpBB since it is isomorphic to ExpC)
-- Indeed, consider an arbitrary ExpF algebra with the carrier U
-- and the operations sigma :: ExpF U -> U.
-- We show that there exists a unique homomorphism
-- (hc sigma) :: ExpC -> U such that the following holds
-- hc sigma . sigma_ExpC = sigma . fmap (hc sigma)
-- Consider x = FLit n :: ExpF ExpC.
-- Then (sigma . fmap (hc sigma)) x = sigma (FLit n)
-- Thus we obtain
-- hc sigma (ExpC $ \f -> f (FLit n)) = sigma (FLit n)
-- from which we get
-- hc sigma e = unExpC e sigma
-- Consider x = FNeg e :: ExpF ExpC.
-- Then (sigma . fmap (hc sigma)) x = sigma (FNeg (hc sigma e))
-- Thus we obtain
-- hc sigma (ExpC $ \f -> f (FNeg (unExpC e f))) = sigma (FNeg (hc sigma e))
-- Again, the only way to satisfy the equality for all sigma and e is to set
-- hc sigma e = unExpC e sigma
-- The case of x = FAdd e1 e2 :: ExpF ExpC is similar.
-- Thus we get the unique morphism from (ExpC, sigma_ExpC) to
-- any other ExpF algebra.
hc :: (ExpF a -> a) -> ExpC -> a
hc sigma e = unExpC e sigma
-- Here is the illustration of the morphism.
-- Recall the view_ops algebra, with String as the carrier set
-- We can recast it in the equivalent functorial view:
sigma_view :: ExpF String -> String
sigma_view = dict_sigma view_ops
-- We immediately get the function to view the values of ExpC type:
viewC :: ExpC -> String
viewC = hc sigma_view
t1c_view = viewC t1c
-- "(8 + (-(1 + 2)))"
-- bb_ops is also an initial algebra: there is a unique
-- homomorphism from it to any other Exp algebra. Here is this morphism
-- h dict . roll = (dict_sigma dict) . fmap (h dict)