\begin{code}
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE KindSignatures #-}
module Mar11 where
import Control.Applicative
\end{code}
Learning objectives:
\begin{itemize}
\item Typed Finally Tagless
\end{itemize}
\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}
liftRR2 :: (a -> b -> c) -> RR a -> RR b -> RR c
liftRR2 f = \x y -> RR $ f (unRR x) (unRR y)
liftRR3 :: (a -> b -> c -> d) -> RR a -> RR b -> RR c -> RR d
liftRR3 f = \x y z -> RR $ f (unRR x) (unRR y) (unRR z)
if’ :: Bool -> a -> a -> a
if’ b x y = if b then x else y
instance Symantics RR where
int = RR
bool = RR
add = liftRR2 (+)
mul = liftRR2 (*)
and_ = liftRR2 (&&)
or_ = liftRR2 (||)
— if_ (RR b) tc ec = if b then tc else ec
if_ = liftRR3 (if’)
leq = liftRR2 (<=) \end{code} Digression: \begin{itemize} \item newtype : a special kind of |data| with a single constructor. \item data : a new datatype with constructors. \item type: a synonym. |type foo = Either String Integer| \end{itemize} Do it again, but this time really digging into the patterns. \begin{code} newtype R a = R {unR :: a} instance Functor R where -- fmap f x = R $ f $ unR x fmap f = R . f . unR instance Applicative R where pure = R f <*> x = R $ (unR f) (unR x)
instance Symantics R where
int = pure
bool = pure
add = liftA2 (+)
mul = liftA2 (*)
and_ = liftA2 (&&)
or_ = liftA2 (||)
if_ = liftA3 (if’)
leq = liftA2 (<=)
\end{code}
And some examples
\begin{code}
ex1 :: Symantics rep => rep Bool
ex1 = if_ (leq (add (int 3) (int 5)) (int 9))
(and_ (bool True) (bool False))
(or_ (bool True) (bool False))
— This is a bad piece of code, for ALL INTERPRETATIONS
— ex2 :: Symantics rep => rep Integer
— ex2 = if_ (bool True) (int 5) (bool False)
ex3 :: Symantics rep => rep Integer
ex3 = let x = mul (int 4) (int 5)
y = mul (int (-3)) (int 134) in
mul (add x y) (mul y y)
\end{code}
Size interpreter for our language.
|a| here is called a \emph{phantom type}.
\begin{code}
newtype Sz a = Sz {unSz :: Int}
instance Functor Sz where
fmap _ x = Sz $ unSz x
instance Applicative Sz where
pure = const $ Sz 1
f <*> x = Sz $ unSz f + unSz x + 1
instance Symantics Sz where
int = pure
bool = pure
add = liftA2 (+)
mul = liftA2 (*)
and_ = liftA2 (&&)
or_ = liftA2 (||)
— note that this counts |if_| as size 2
if_ = liftA3 (if’)
leq = liftA2 (<=) \end{code}