\begin{code}
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Mar09 where
import Mar08
\end{code}
Learning objectives:
\begin{itemize}
\item DSL encodings
\item Finally Tagless
\end{itemize}
Deep version
\begin{code}
data BExpr = BLit Bool | BExpr :&&: BExpr | BExpr :||: BExpr | Not BExpr
deriving Show
evalB :: BExpr -> Bool
evalB (BLit b) = b
evalB (b1 :&&: b2) = evalB b1 && evalB b2
evalB (b1 :||: b2) = evalB b1 || evalB b2
evalB (Not b) = not $ evalB b
\end{code}
Skip shallow version, not interesting, still.
\begin{code}
class BExprSy e where
blit :: Bool -> e
band :: e -> e -> e
bor :: e -> e -> e
bnot :: e -> e
\end{code}
other naming convention: use a trailing underscore.
Give an implementation:
\begin{code}
newtype B = B {unB :: Bool}
liftB1 :: (Bool -> Bool) -> (B -> B)
liftB1 f = \x -> B $ f (unB x)
liftB2 :: (Bool -> Bool -> Bool) -> (B -> B -> B)
liftB2 f = \x y -> B $ f (unB x) (unB y)
instance BExprSy B where
— the more interesting implementation:
blit = B
band = liftB2 (&&)
bor = liftB2 (||)
bnot = liftB1 (not)
\end{code}
Let us now try to combine them:
\begin{code}
data BorI = Bool Bool | Int Integer
deriving Show
\end{code}
Notice the PUN: |Bool| is used as a constructor (on the left) and as a
type (on the right); the right uses |Int| for |Integer|.
\begin{code}
data Lang3 = BExpr BExpr | IExpr Expr | If_ BExpr Lang3 Lang3
deriving Show
eval3 :: Lang3 -> BorI
eval3 (BExpr be) = Bool $ evalB be
eval3 (IExpr ie) = Int $ eval ie
eval3 (If_ b thene elsee) = if b’ then eval3 thene else eval3 elsee
where
b’ = evalB b
ex4 :: Lang3
ex4 = If_ (BLit True :||: BLit False) (BExpr $ BLit True) (IExpr $ LInt 3)
ex5 :: Bool -> Lang3
ex5 b = If_ (BLit b) (BExpr $ BLit True) (IExpr $ LInt 3)
\end{code}
And the same for the class version. If we try to do something in that
direction, things spin out of control.
\begin{spec}
class (BExprSy b, ExprSy i) => Lang3Sy b i e where
bool3 :: b -> e
int3 :: i -> e
if_ :: b -> e -> e -> e
\end{spec}
Another problem: |Lang3| is ‘untyped’. Can we do better?
First do a typed version using classes. Then back to a Deep embedding.
Also, for now, do a big language. Portemanteau: Sy(ntax) + (Se)mantics
rep short for ‘representation’. Note that here rep :: * -> *.
\begin{code}
class Symantics rep where
int :: Integer -> rep Integer
add :: rep Integer -> rep Integer -> rep Integer
mul :: rep Integer -> rep Integer -> rep Integer
bool :: Bool -> rep Bool
and_ :: rep Bool -> rep Bool -> rep Bool
or_ :: rep Bool -> rep Bool -> rep Bool
if_ :: rep Bool -> rep a -> rep a -> rep a
leq :: rep Integer -> rep Integer -> rep Bool
\end{code}
How to do an instance?
\begin{code}
newtype RR a = RR {unRR :: a}
instance Symantics RR where
int = RR
bool = RR
add (RR x) (RR y) = RR $ x + y
mul (RR x) (RR y) = RR $ x * y
and_ (RR x) (RR y) = RR $ x && y
or_ (RR x) (RR y) = RR $ x || y
if_ (RR b) tc ec = if b then tc else ec
leq (RR x) (RR y) = RR $ x <= y \end{code}