Meta-programming in Haskell: A Closer Look at Splices and Quotations
Explore the world of meta-programming in Haskell through splices and quotations. Learn about successful extensions introduced by Simon Peyton Jones and Tim Sheard, including practical examples like generating source code using splices that are type-checked and compiled at compile time. Dive into concepts like mkPow, printf, and const to understand how Haskell's meta-programming capabilities enable advanced code manipulation and generation.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Simon Peyton Jones Tim Sheard Microsoft Resaerch 2016
An extremely successful meta-programming extension for Haskell Introduced in 2002, joint work with Tim Sheard (of MetaML fame). Widely used: over 900 (out of 8,200) packages on Hackage
cube :: Int -> Int cube = $(mkPow 3) You can write code (mkPow) that generates source Haskell that gets spliced in where you invoke it $(mkPow 3) \x -> x*x*x and then is typechecked and compiled just as if you d written that code in the first place
mkPow :: Int -> ExpQ -> ExpQ mkPow 1 e = e mkPow n e = [| $e * $(mkPow (n-1) e) |] mkPow :: Int -> ExpQ mkPow n = [| \x -> $(mkPow n [| x |]) |] [| |] is a quotation It generates a syntax tree of type ExpQ $( ) is a splice It takes a syntax tree of type ExpQ, and inserts it at that point
printf :: String -> ExpQ $(printf Name: %s; age: %d ) Fred 45 Splices are run at compile time only No runtime code generation (c.f. MetaML) A bit like cpp, but more civilised; e.g. no syntax errors in expanded code What about No x is not in scope errors? No Cannot match Int with Bool errors?
const :: ExpQ -> ExpQ -- In a library const e = [| \x -> $e |] f a b = $(const [| a+b |]) -- ---> f a b = \x -> a+b g x b = $(const [| x+b |]) -- ---> g x b = \x -> x+b -- Eeek!
const :: ExpQ -> ExpQ -- In a library const e = [| \x -> $e |] f a b = $(const [| a+b |]) -- ---> f a b = \x -> a+b g x b = $(const [| x+b |]) -- ---> g x b = \x0 -> x+b -- OK! Intuitively: the source code should determine the binding structure Anything else is fundamentally non-modular; may fail randomly
Not enough just to draw quoted binders from a different alphabet const :: ExpQ -> ExpQ -- In a library const e = [| \x -> $e |] f = [| \x -> $(const [| x+1 |]) |] -- $(f) ---> \x0 -> \x1 -> x0 + 1 Quoted binders must be fresh somehow
nList :: Int -> ExpQ -> ExpQ nList 0 e = [| [] |] nList n e = [| $e : $(nList (n-1) e) |] f x = $(nList 3 [| True |]) ---> f x = [True, True, True] g x = $(nList 3 [| x |]) ---> f x = [x, x, x]
f x = $(nList 3 [| True |]) ---> f x = [True, True, True] g x = $(nList 3 [| x |]) ---> f x = [x, x, x] h x = $(nList x [| True |]) ---> ??? The splice in h runs at compile time; but x is not available until run time. Staging error! Easy to fix: type environment carries stage index
f1 :: Int -> ExpQ f1 x = [| \y -> x + y |] -- OK f2 :: (Int,Int) -> ExpQ f2 x = [| \y -> fst x + y |] -- OK f3 :: [Int] -> ExpQ f3 xs = [| \g -> map g xs |] -- OK f4 :: (Int->Int) -> ExpQ f4 g = [| \ys -> map g ys |] -- Not OK
f1 :: Int -> ExpQ f1 x = [| \y -> x + y |] -- OK means (driven by the cross-stage info) f1 x = [| \y -> $(lift x) + y |] class Liftable a where lift :: a -> ExpQ instance Liftable Int where lift n = ...wait and see... instance (Liftable a, Liftable b) => Liftable (a,b) where lift (x,y) = [| ( $(lift x), $(lift y) ) |]
module M where nList :: Int -> ExpQ -> ExpQ nList 0 e = [| [] |] nList n e = [| $e : $(nList (n-1) e) |] foo = $(nList 3 True) We d need to compile nList (to bytecode or machine code) before even typechecking foo . That s awkward. Restriction: in a top-level splice you can only call imported top-level functions.
1. We want to generate only well-typed terms 2. We want to generate patterns, types, declarations; compile time reflection; analyse code, not just generate code I don t know how to achieve both at once So TH (now) does them separately
Horrible possibility: suppose not $(f True) generates an ill-typed expression, or one that does not have type Bool. Then error messages speak of the expanded code. Wanted: static guarantee of well-typed-ness
Well-established solution (MetaML) [|| e ||] :: TExpQ t if e :: t $$(e) :: t if e :: TExpQ t If v :: TExpQ t, then v is the syntax tree representing a well-typed term of type t f :: TExpQ Int -> TExpQ Int f x = [|| $$x + 1 ||] h y = $$(f [|| y ||])
Well-established solution (MetaML) [|| e ||] :: TExpQ t if e :: t $$(e) :: t if e :: TExpQ t f :: TExpQ Int -> TExpQ Int f x = [| $x + 1 |] h y = $(f [| y |]) Splices must run during typechecking, so that we can ensure that y :: TExpQ Int All is good!
nList :: Int -> TExpQ -> TExpQ nList n e | n == 0 = [|| [] |] | n > 0 = [|| $$e : $$(nList (n-1) e) ||] | otherwise = error Negative arg to nList Want a civilised error message with line number etc, not a compiler crash!
nList :: Int -> TExpQ -> TExpQ nList n e | n == 0 = [|| [] ||] | n > 0 = [|| $$e : $$(nList (n-1) e) ||] | otherwise = fail Negative arg to nList fail :: String -> Q a type TExpQ t = Q (TExp t) The quotation monad The syntax tree type Q can be an exception monad, supporting civilised failure
isExtEnabled :: Extension -> Q Bool extsEnabled :: Q [Extension] location :: Q Loc report :: Bool -> String -> Q recover :: Q a -> Q a -> Q a fail :: String -> Q a
runIO :: IO a -> Q a addDependentFile :: FilePath -> Q () addTopDecls :: [Dec] -> Q () addModFinalizer :: Q () -> Q () getQ :: Typeable a => Q (Maybe a) putQ :: Typeable a => a -> Q ()
Expressions we can generate but not type: $(f 2) --> \x1. \x2. True $(f 3) --> \x1. \x2. \x3. True So f :: Int -> TExpQ ??? $(sel 1 3) --> \x. case x of (a,b,c) -> a $(printf %d,%s ) --> \(x::Int) (y::String). show x ++ , ++ show y
Other splicable entities Patterns f $(selPat 3 1) = x --> f (x,_,_) = x Types f :: $(selType 3 1) --> f :: (a,b,c) -> a Declarations $(genSel 3 1) --> sel_3_1 (a,b,c) = a $(genEnum 3) --> data T3 = D1 | D2 | D3
The Wild West I'm just using a quotation as a convenient way to build a syntax tree. Please don't even try to typecheck it; just wait until it is finally spliced into a top-level splice
type ExpQ = Q Exp The syntax tree type data Exp = VarE Name | ConE Name | LitE Lit | AppE Exp Exp | LamE [Pat] Exp | etc Exp, Lit, Pat, etc are all algebraic data types representing Haskell source syntax Defined in Language.Haskell.Syntax
Quotations are just just syntactic sugar The syntax tree type [| $e : $(nList (n-1) e) |] means do { h <- e ; t <- nList (n-1) e ; return (ConE : h t) } And you are perfectly at liberty to write the do-notation form instead of the quasi-quote : is the TH Name of the (:) operator
newName :: String -> Q Name Generate a fresh name The syntax tree type [| \f -> map f $e |] means Use it in pattern do { fn <- newName f ; t <- e ; return (LamE [VarP fn] (AppE (AppE (VarE map) (VarE fn)) t)) } -- fn :: Name And in a term The Name of map
newName :: String -> Q Name The syntax tree type do { fn <- newName f -- fn :: Name ; t <- e ; return (LamE [VarP xn] (AppE (AppE (VarE map) (VarE fn)) t)) } Can mix convenient quasi-quote notation with do-notation can also be written like this do { fn <- newName f ; body <- [| map $(VarE fn) $e |] ; return (LamE [VarP xn] body) }
type ExpQ = Q Exp type PatQ = Q Pat type DecQ = Q Dec type TypQ = Q Typ type TExpQ t = Q (TExp t) The syntax tree type Plus quotation notation for decls [d| data T = T1 | T2 |] patterns [p| (x,y) |] types [t| Int -> Int |] No hope of typechecking quotes [d| f :: $(g True); f $(h) = $(j) |]
No hope of typechecking quotes [d| f :: $(g True); f $(h) = $(j) |] Splicing must happen in the renamer, to bring variables into scope let x = True in \$(blah) -> x Sadly: give up on guarantee that spliced-in terms or declarations are type-correct and fit their context. Instead, rely on typechecking after splicing
Unlike Scheme, we do rename/typecheck before running the splice. $(mlet x 3 (x+1)) $(mlet [| x |] [| 3 |] [| x+1 |]) -- Ditto -- Rejected So hygiene is still easy to enforce
module M where f x = ...no mention of h or g... $(blah) - Defines function h -- blah cannot mention h or g g y = ... mentions h... Can t really type, and then run, blah if it mentions g (which mentions stuff bound by blah ) So TH enforces a top-to-bottom discipline
data T = T1 Int T | T2 $(makeLens T) Want makeLens to Get hold of the definition of T (reification) Chew on it Spit out some T-related boilerplate definitions makeLens :: Name -> Q [Dec] makeLens n = do { d <- reify n ; case d of }
lookupName :: Bool -> String -> Q (Maybe Name) reify :: Name -> Q Info reifyFixity :: Name -> Q (Maybe Fixity) reifyInstances :: Name -> [Type] -> Q [InstanceDec] reifyRoles :: Name -> Q [Role] reifyAnnotations :: Data a => AnnLookup -> Q [a] reifyModule :: Module -> Q ModuleInfo reifyConStrictness :: Name -> Q [DecidedStrictness] data Info = VarI Name Type (Maybe Dec) | TyConI Dec | ClassI Dec [InstanceDec] | etc
newtype TExp t = TExp { unType :: Exp } -- unType :: TExp t -> Exp TExp is an abstract type, with a phantom t Can only be constructed using (typed) quotations [|| blah ||] Can only be decomposed by converting to Exp
f x = [p| blah |] means (confusingly) f x = $(quoteExp p blah ) data QuasiQuoter = QuasiQuoter { quoteExp :: String -> Q Exp, quotePat :: String -> Q Pat, quoteType :: String -> Q Type, quoteDec :: String -> Q [Dec] } User-written parsers, for totally different langauges
[pads| funny PADS stuff |] Works for declarations, patterns, types, as well as expressions (one parser for each) Depends crucially on generating untyped syntax trees A useful way of embedding completely different language in Haskell
THSyn vs HsSyn; keeping them in sync Pain of quotation. Other language (Scheme, Scala ) do implicit quotation. f e instead of f [| e |] Reification of an Id whose type is not yet settled f x = $(do { xinfo <- reify x; }) but this is ok (because of staging) x = blah; $(do { reify x; })
