\begin{code}
{-# OPTIONS_GHC -Wall #-}
module Apr1 where
import Language.Haskell.TH.Syntax (Lift)
import Mar18 hiding (if’)
— import Mar23
import Mar30
\end{code}
Learning objectives:
\begin{itemize}
\item Partial evaluation, i.e. optimizing compiler
\end{itemize}
Today’s content is slightly different: mostly to be read, not reproduced.
Partial evaluation ~ running parts of the program at compile time.
Usually: program given some “static” inputs and “dynamic” inputs.
static ~ known now, at compile time
dynamic ~ not known until run-time
classical “use”: power x n to compute x\^n when x dynamic, n static
i.e. compute x\^37.
\begin{code}
class Ints2 rep where
int’ :: Integer -> rep Integer Integer
neg’ :: rep Integer Integer -> rep Integer Integer
add’ :: rep Integer Integer -> rep Integer Integer -> rep Integer Integer
mult’ :: rep Integer Integer -> rep Integer Integer -> rep Integer Integer
class Boolean2 rep where
bool’ :: Bool -> rep Bool Bool
not’ :: rep Bool Bool -> rep Bool Bool
and’ :: rep Bool Bool -> rep Bool Bool -> rep Bool Bool
or’ :: rep Bool Bool -> rep Bool Bool -> rep Bool Bool
class IntOrder2 rep where
leq’ :: rep Integer Integer -> rep Integer Integer -> rep Bool Bool
class Conditional2 rep where
if’ :: rep Bool Bool -> rep s d -> rep s d -> rep s d
class Pairs2 rep where
pair’ :: rep sa da -> rep sb db -> rep (sa, sb) (da, db)
fst’ :: Lift a => rep (a, b) (a, b) -> rep a a
snd’ :: Lift b => rep (a, b) (a, b) -> rep b b
class Equality2 rep where
eq’ :: Eq a => rep a a -> rep a a -> rep Bool Bool
class Plus2 rep where
left’ :: rep sa da -> rep (Either sa sb) (Either da db)
right’ :: rep sb db -> rep (Either sa sb) (Either da db)
either’ :: (Lift a, Lift b) =>
rep (rep a a -> rep c c) (a -> c) -> rep (rep b b -> rep c c) (b -> c) -> rep (Either a b) (Either a b) -> rep c c
class Lambda2 rep where
lam’ :: (rep sa da -> rep sb db) -> rep (rep sa da -> rep sb db) (da -> db)
app’ :: rep (rep sa da -> rep sb db) (da -> db) -> rep sa da -> rep sb db
class Fix2 rep where
fix’ :: (rep (sa -> sb) (da -> db) -> rep (sa -> sb) (da -> db)) -> rep (sa -> sb) (da -> db)
data P static dynamic =
P { dynamic :: C dynamic, static :: Maybe static }
stat :: (static -> C dynamic) -> static -> P static dynamic
stat f b = P (f b) (Just b)
dyna :: C dynamic -> P static dynamic
dyna d = P d Nothing
liftP1 :: (b -> C b) -> (a -> b) -> (C a -> C b) -> P a a -> P b b
liftP1 l f _ (P _ (Just x)) = stat l (f x)
liftP1 _ _ g (P y _ ) = dyna $ g y
liftP2 :: (c -> C c) -> (a -> b -> c) -> (C a -> C b -> C c) -> P a a -> P b b -> P c c
liftP2 l f _ (P _ (Just x)) (P _ (Just y)) = P (l $ f x y) (Just $ f x y)
liftP2 _ _ g (P x _ ) (P y _ ) = dyna $ g x y
— some things are Monoids, have units
unital :: Eq static => (static -> C dynamic) ->
(static -> static -> static) ->
(C dynamic -> C dynamic -> C dynamic) ->
static ->
(P static dynamic -> P static dynamic -> P static dynamic)
unital l f _ _ (P _ (Just a)) (P _ (Just b)) = stat l (f a b)
unital _ _ _ u (P _ (Just a)) b | a == u = b
unital _ _ _ u a (P _ (Just b)) | b == u = a
unital _ _ g _ (P a _) (P b _) = dyna (g a b)
instance Boolean2 P where
bool’ = stat bool
not’ = liftP1 bool not not_
and’ = unital bool (&&) and_ True
or’ = unital bool (||) or_ False
instance Ints2 P where
int’ = stat int
neg’ = liftP1 int negate (\x -> sub (int 0) x)
add’ = unital int (+) add 0
mult’ = unital int (*) mul 1
\end{code}
Some test programs
\begin{code}
prog_1′ :: (Lambda2 rep, Boolean2 rep) => () -> rep Bool Bool
prog_1′ () = app’ (lam’ (\x -> x)) (bool’ True)
— readable version: (\x -> x) $ True
prog_11′ :: (Ints2 rep, Lambda2 rep) => () -> rep Integer Integer
prog_11′ () = neg’ $ app’ (lam’ (\x -> (mult’ x x))) (int’ 2)
— readable version: – ((\x -> x * x) $ 2)
testpowfix’ :: (Lambda2 rep, Fix2 rep, Conditional2 rep, IntOrder2 rep, Ints2 rep) =>
() -> rep (rep Integer Integer -> rep (rep Integer Integer -> rep Integer Integer) (Integer -> Integer)) (Integer -> Integer -> Integer)
testpowfix’ () = lam’ (\x ->
fix’ (\self -> lam’ (\n ->
if’ (leq’ n (int’ 0)) (int’ 1)
(mult’ x (app’ self (add’ n (int’ (-1))))))))
— readable version: (\x -> fix (\self (\n -> if (n <= 0 ) then 1 else x * self $ (n + (-1)))
pow :: (Ord x, Num x, Num n) => n -> x -> n
pow x = \n -> if (n <= 0) then 1 else x * pow x (n - 1)
\end{code}