{-# 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.
data ExpDict a = ExpDict{ dlit :: Int -> a,
dneg :: a -> a,
dadd :: a -> a -> a }
-- We can define (a version of) Boehm-Berarducci encoding as
type ExpBB1 = forall a. (ExpDict a -> a)
-- To use only applications and abstractions, we curry the record
-- argument ExpDict 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 $ \dlit dneg dadd -> dlit x
neg :: ExpBB -> ExpBB
neg e = ExpBB $ \dlit dneg dadd -> dneg (unExpBB e dlit dneg dadd)
add :: ExpBB -> ExpBB -> ExpBB
add e1 e2 = ExpBB $ \dlit dneg dadd ->
dadd (unExpBB e1 dlit dneg dadd) (unExpBB e2 dlit dneg dadd)
-- A sample expression: our first running example
tbb1 = add (lit 8) (neg (add (lit 1) (lit 2)))
-- A sample consumer
-- viewBB: can be implemented simply via the induction principle
-- It is not recursive!
viewBB:: ExpBB -> String
viewBB e = unExpBB e dlit dneg dadd
where
dlit n = show n
dneg e = "(-" ++ e ++ ")"
dadd e1 e2 = "(" ++ e1 ++ " + " ++ e2 ++ ")"
tbb1v = viewBB tbb1
-- "(8 + (-(1 + 2)))"
-- 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 dlit dneg dadd
where
dlit :: Int -> ExpF ExpBB
dlit n = FLit n
dneg :: ExpF ExpBB -> ExpF ExpBB
dneg e = FNeg (roll e)
dadd :: ExpF ExpBB -> ExpF ExpBB -> ExpF ExpBB
dadd 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}
decon :: ExpBB -> ExpD
decon e = unExpBB e dlit dneg dadd
where
dlit n = ExpD $ \onlit onneg onadd -> onlit n
dneg e = ExpD $ \onlit onneg onadd -> onneg (unED e lit neg add)
dadd e1 e2 = ExpD $ \onlit onneg onadd ->
onadd (unED e1 lit neg add) (unED e2 lit neg add)
-- We redo viewBB, using pattern-matching this time, and recursion
viewBBd:: ExpBB -> String
viewBBd e = unED (decon e) dlit dneg dadd
where
dlit n = show n
dneg e = "(-" ++ viewBBd e ++ ")"
dadd 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) dlit dneg dadd
where
dlit _ = e
dneg e2 = unED (decon e2) dlit2 dneg2 dadd2
where
dlit2 n = e
dneg2 e = push_negBB e
dadd2 e1 e2 = add (push_negBB (neg e1)) (push_negBB (neg e2))
dadd 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 ExpDict 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 ExpDict U,
-- or in the form of a function ExpF U -> U.
sigma_dict :: (ExpF a -> a) -> ExpDict a
sigma_dict sigma = ExpDict{ dlit = \n -> sigma (FLit n),
dneg = \e -> sigma (FNeg e),
dadd = \e1 e2 -> sigma (FAdd e1 e2) }
dict_sigma :: ExpDict a -> (ExpF a -> a)
dict_sigma dict (FLit n) = dlit dict n
dict_sigma dict (FNeg e) = dneg dict e
dict_sigma dict (FAdd e1 e2) = dadd dict 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 :: ExpDict a -> ExpBB -> a
h dict e = unExpBB e (dlit dict) (dneg dict) (dadd dict)
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 $ \dlit dneg dadd ->
unExpC e (dict_sigma (ExpDict dlit dneg dadd))
-- 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.
-- Define an ExpF algebra,
-- with Strings as the carrier and the following operations
sigma_view :: ExpF String -> String
sigma_view (FLit n) = show n
sigma_view (FNeg e) = "(-" ++ e ++ ")"
sigma_view (FAdd e1 e2) = "(" ++ e1 ++ " + " ++ e2 ++ ")"
-- 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)))"
-- (ExpBB, sigma_ExpBB) is also 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)