\begin{code}
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TemplateHaskell #-}
module Mar30 where
import Language.Haskell.TH
import Mar18
\end{code}
Learning objectives:
\begin{itemize}
\item meta-programming, Template Haskell (TH)
\item adding TH instances to Symantics
\end{itemize}
\begin{verbatim}
$ ghci -XTemplateHaskell
GHCi, version 8.6.5: http://www.haskell.org/ghc/ 😕 for help
Prelude> :m + Language.Haskell.TH
Prelude Language.Haskell.TH> runQ [| \x -> x || True |]
LamE [VarP x_0] (InfixE (Just (VarE x_0)) (VarE GHC.Classes.||) (Just (ConE GHC.
Types.True)))
Prelude Language.Haskell.TH> runQ [| \x y -> x || y |]
LamE [VarP x_1,VarP y_2] (InfixE (Just (VarE x_1)) (VarE GHC.Classes.||) (Just (
VarE y_2)))
Prelude Language.Haskell.TH> let e = [|| \x y -> x || y ||]
Prelude Language.Haskell.TH> :t e
e :: Q (TExp (Bool -> Bool -> Bool))
Prelude Language.Haskell.TH> ee <- runQ e
Prelude Language.Haskell.TH> :t ee
ee :: TExp (Bool -> Bool -> Bool)
Prelude Language.Haskell.TH> unType ee
LamE [VarP x_3,VarP y_4] (InfixE (Just (VarE x_3)) (VarE GHC.Classes.||) (Just (
VarE y_4)))
Prelude Language.Haskell.TH> pprint $ unType ee
“\\x_0 y_1 -> x_0 GHC.Classes.|| y_1”
Prelude Language.Haskell.TH>
\end{verbatim}
\begin{spec}
newtype U a = U {unU :: Q Exp}
instance IntSy U where
int n = U [| True |]
\end{spec}
\begin{code}
newtype C a = C {unC :: Q (TExp a)}
liftC1 :: Q (TExp (t1 -> a)) -> C t1 -> C a
liftC1 f = \x -> C [|| $$f $$(unC x) ||]
liftC2 :: Q (TExp (t1 -> t2 -> a)) -> C t1 -> C t2 -> C a
liftC2 f = \x y -> C [|| $$f $$(unC x) $$(unC y) ||]
liftC3 :: Q (TExp (t1 -> t2 -> t3 -> a)) -> C t1 -> C t2 -> C t3 -> C a
liftC3 f = \x y z -> C [|| $$f $$(unC x) $$(unC y) $$(unC z) ||]
instance IntSy C where
int n = C [|| n ||]
add = liftC2 [|| (+) ||]
sub = liftC2 [|| (-) ||]
mul = liftC2 [|| (*) ||]
instance BoolSy C where
bool = \b -> C [|| b ||]
and_ = liftC2 [|| (&&) ||]
or_ = liftC2 [|| (||) ||]
if_ = \(C b) (C tb) (C eb) -> C [|| if $$b then $$tb else $$eb ||]
not_ = liftC1 [|| not ||]
instance OrderSy C where
leq = liftC2 [|| (<=) ||]
instance PairSy C where
pair = liftC2 [|| (,) ||] -- introduction rule
fst_ = liftC1 [|| fst ||] -- elimination rule
snd_ = liftC1 [|| snd ||] -- elimination rule
instance SumSy C where
left = liftC1 [|| Left ||] -- introduction rule
right = liftC1 [|| Right ||] -- introduction rule
either_ = liftC3 [|| either ||] -- elimination rule
instance FunctionSy C where
app = liftC2 [|| ($) ||] -- elimination rule
lam f = C [|| \x -> $$(unC . f . C $ [|| x ||]) ||]
instance FixSy C where
fix_ f = C [||
let self n = $$(unC . f . C $ [|| self ||]) n in self ||]
instance EqSy C where
eq = liftC2 [|| (==) ||]
\end{code}