1 {-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -XFlexibleContexts -XMultiParamTypeClasses -ddump-types #-}
5 import GHC.HetMet.CodeTypes hiding ((-))
6 import Prelude (undefined, ($), (==), fromInteger, Bool(..), Int, (-), negate, mod, (*), (+), Char, (||), (&&))
8 -- The best way to understand heterogeneous metaprogramming and
9 -- generalized arrows is to play around with this file, poking at the
10 -- examples until they fail to typecheck -- you'll learn a lot that
13 -- Once you've built the modified compiler, you can compile this file
16 -- $ inplace/bin/ghc-stage2 tutorial.hs
19 -- -XModalTypes adds a new syntactical expression, "code brackets":
20 code_fst = <[ \(x,y) -> x ]>
22 -- This new expression is the introduction form for modal types:
23 code_fst :: forall a b g. <[ (a,b) -> a ]>@g
25 -- Think of <[T]>@g as being the type of programs written in language
26 -- "g" which, when "executed", return a value of type "T". I mention
27 -- "language g" because the *heterogeneous* aspect of HetMet means
28 -- that we can limit the sorts of constructs allowed inside the code
29 -- brackets, permitting only a subset of Haskell (you have to use
30 -- Haskell syntax, though).
32 -- There is a second new expression form, "~~", called "escape":
34 code_fst_fst = <[ \z -> ~~code_fst (~~code_fst z) ]>
36 -- Note that ~~ binds more tightly than any other operator. There is
37 -- an alternate version, "~~$", which binds more weakly than any other
38 -- operator (this is really handy sometimes!). To demonstrate this,
39 -- the next two expressions differ only in superficial syntax:
41 example1 foo bar = <[ ~~$ foo bar ]>
42 example2 foo bar = <[ ~~( foo bar) ]>
43 -- example3 foo bar = <[ ~~ foo bar ]>
45 -- ... but the third one is completely different (and in fact, doesn't
46 -- even parse, but we'll get to that in a moment)
48 -- The escape operation must appear within code brackets. In truth,
49 -- it is really a "hole" punched in the code brackets -- the thing to
50 -- which the escape operator gets applied is typed as if it were
51 -- *outside* the code brackets. It must have type <[T]>, and the
52 -- escape operator allows it to be used *inside* code brackets as if
55 -- So, the escape operator is basically a way of pasting code
56 -- fragments into each other.
58 -- This is where those type variables after the "@" sign come in: if
59 -- you paste two pieces of code into a third, all three must be
60 -- written in the same language. We express this by unifying their
63 compose_code :: forall g a b c. <[a->b]>@g -> <[b->c]>@g -> <[a->c]>@g
64 compose_code x y = <[ \z -> ~~y (~~x z) ]>
66 -- Now, try commenting out the type ascription above and uncommenting
67 -- any of these three:
69 -- compose_code :: forall g h a b c. <[a->b]>@h -> <[b->c]>@g -> <[a->c]>@g
70 -- compose_code :: forall g h a b c. <[a->b]>@g -> <[b->c]>@h -> <[a->c]>@g
71 -- compose_code :: forall g h a b c. <[a->b]>@g -> <[b->c]>@g -> <[a->c]>@h
74 -- The typechecker won't let you get away with that -- you're trying
75 -- to force a type which is "too polymorphic" onto paste2. If the
76 -- compiler allowed that, the resulting metaprogram might try to
77 -- splice together programs written in different languages, resulting
80 -- NEW SCOPING RULES: The syntactical depth (or just "depth") of an
81 -- expression is the number of surrounding code-brackets minus the
82 -- number of surrounding escapes (this is strictly a syntax concept
83 -- and has NOTHING to do with the type system!). It is very important
84 -- to keep in mind that the scope of a bound variable extends only to
85 -- expressions at the same depth! To demonstrate, the following
86 -- expression will fail to parse:
88 -- badness = \x -> <[ x ]>
90 -- ...and in the following expression, the occurrence of "x" is bound
91 -- by the first (outer) lambda, not the second one:
93 no_shadowing_here = \x -> <[ \x -> ~~x ]>
95 -- the rest of this file contains a bunch of example programs:
96 -- exponentiation, dot-product, a bunch of classic MetaML idioms, and
97 -- a translation of Nanevski+Pfenning's two-stage regex matcher.
104 --------------------------------------------------------------------------------
105 -- Ye Olde and Most Venerable "pow" Function
110 else <[ \x -> x * ~~(pow (n - 1)) x ]>
113 -- a more efficient two-level pow
114 pow' 0 = <[ \x -> 1 ]>
115 pow' 1 = <[ \x -> x ]>
116 pow' n = if n `mod` 2==0
117 then <[ \x -> (\y -> y*y) (~~(pow' $ n `shiftR` 2) x) ]>
118 else <[ \x -> x * ~~(pow' $ n-1) x ]>
130 --------------------------------------------------------------------------------
133 -- This shows how to build a two-level program one step at a time by
134 -- slowly rearranging it until the brackets can be inserted.
137 -- a one-level function to compute the dot product of two vectors
138 dotproduct :: [Int] -> [Int] -> Int
145 (a*b)+(dotproduct ax bx)
147 -- A slightly modified version of the dot product: note that we
148 -- check for zeroes and ones to avoid multiplying. In a one-level
149 -- program this yields no advantage, however!
150 dotproduct' :: [Int] -> [Int] -> Int
156 (b:bx) -> (dotproduct' ax bx)
159 (b:bx) -> b+(dotproduct' ax bx)
163 (a*b)+(dotproduct' ax bx)
165 -- A two-level version of the dot product. Note how we ask for the first
166 -- vector, then produce a program which is optimized for multiplying
167 -- by that particular vector. If there are zeroes or ones in the
168 -- original vector, we will emit code which is faster than a one-level
170 dotproduct'' :: forall g.
171 GuestLanguageAdd g Int =>
172 GuestLanguageMult g Int =>
173 GuestLanguageFromInteger g Int =>
174 [Int] -> <[ [Int] -> Int ]>@g
178 (0:ax) -> <[ \v2 -> case v2 of
180 (b:bx) -> ~~(dotproduct'' ax) bx ]>
181 (1:ax) -> <[ \v2 -> case v2 of
183 (b:bx) -> b + ~~(dotproduct'' ax) bx ]>
184 (a:ax) -> <[ \v2 -> case v2 of
186 (b:bx) -> %%a * b + ~~(dotproduct'' ax) bx ]>
193 --------------------------------------------------------------------------------
194 -- Taha-Sheard "isomorphism for code types"
196 back :: forall a b c. (<[b]>@a -> <[c]>@a) -> <[ b->c ]>@a
197 back = \f -> <[ \x -> ~~(f <[x]>) ]>
199 forth :: forall a b c. <[b->c]>@a -> (<[b]>@a -> <[c]>@a)
200 forth = \f -> \x -> <[ ~~f ~~x ]>
204 --------------------------------------------------------------------------------
205 -- Examples of "running" code; these examples illustrate the sorts of
206 -- scoping problems that the Taha-Nielsen environment classifiers look
207 -- for in the context of HOMOGENEOUS metaprogramming. You can't
208 -- actually define these functions for ALL generalized arrows -- only
209 -- those for which you've defined some sort of interpretation in Haskell.
211 run :: forall a. (forall b. <[a]>@b) -> a
214 -- the typchecker correctly rejects this bogosity if you uncomment it:
215 -- bogus = <[ \x -> ~~( run <[ x ]> ) ]>
217 -- The Calcano-Moggi-Taha paper on environment classifier inference
218 -- had a special type for closed code and two special expressions
219 -- "close" and "open". These are unnecessary in SystemFC1 where we
220 -- can use higher-rank polymorphism to get the same result (although
221 -- in truth it's cheating a bit since their type inference is
222 -- decidable with no annotations, whereas Rank-N inference is not):
224 data ClosedCode a = ClosedCode (forall b. <[a]>@b)
226 open :: forall a b. ClosedCode a -> <[a]>@b
227 open (ClosedCode x) = x
229 close :: (forall b. <[a]>@b) -> ClosedCode a
230 close x = ClosedCode x
232 run_closed :: ClosedCode a -> a
233 run_closed = undefined
238 --------------------------------------------------------------------------------
239 -- A two-level Regular Expression matcher, adapted from Nanevski+Pfenning, Figure 6
252 -- a continuation-passing-style matcher
254 accept :: Stream s => Regex -> (s -> Bool) -> s -> Bool
259 accept (Plus e1 e2) k s =
260 (accept e1 k s) || (accept e2 k s)
262 accept (Times e1 e2) k s =
263 (accept e1 (accept e2 k)) s
265 accept (Star e) k s =
266 (k s) || (accept e (\s' -> accept (Star e) k s') s)
267 -- FIXME: this will loop forever if you give it (Star x) where x can
268 -- match the empty string
270 accept (Const c) k s =
273 else (s_head s) == c && k (s_tail s)
275 class GuestStream g a where
276 <[ gs_empty ]> :: <[ a -> Bool ]>@g
277 <[ gs_head ]> :: <[ a -> Char ]>@g
278 <[ gs_tail ]> :: <[ a -> a ]>@g
280 class GuestEqChar g where
281 <[ (==) ]> :: <[ Char -> Char -> Bool ]>@g
287 GuestLanguageBool c =>
292 staged_accept Empty k =
293 <[ \s -> gs_empty s ]>
295 -- note that code for "k" gets duplicated here
296 staged_accept (Plus e1 e2) k =
297 <[ \s -> (~~(staged_accept e1 k) s) || (~~(staged_accept e2 k) s) ]>
299 staged_accept (Times e1 e2) k =
300 <[ \s -> ~~(staged_accept e1 (staged_accept e2 k)) s ]>
302 staged_accept (Star e) k =
305 -- loop :: <[s -> Bool]>@g
306 loop = <[ \s -> ~~k s || ~~(staged_accept e loop) s ]>
307 -- note that loop is not (forall c s. <[s -> Bool]>@c)
308 -- because "k" is free in loop; it is analogous to the free
309 -- environment variable in Nanevski's example
311 staged_accept (Const c) k =
312 <[ \s -> if gs_empty s
314 else (gs_head s) == %%c && ~~k (gs_tail s) ]>
316 this type won't work unless the case for (Star e) is commented out;
321 GuestLanguageBool c =>
326 GuestLanguageBool c =>
333 --------------------------------------------------------------------------------
334 -- An example generalized arrow
336 -- *** this will be finished and posted by 14-Mar-2011; the code
337 -- *** below is just a sketch ***
340 -- A verilog module is an SDoc (chunk of text) giving the module's
341 -- definition. The UniqueSupply avoids name clashes.
344 [VerilogModule] -- dependencies
345 String -> -- module name
346 (Tree String -> -- input port names
347 Tree String -> -- output port names
348 SDoc) -- raw verilog code for the body
351 instance Show VerilogModule where
352 show VerilogModule dep name body =
353 "module "++name++"(FIXME)"++(body FIXME FIXME)
355 data VerilogWrappedType a =
356 { vwt_rep :: String }
358 -- A "verilog garrow" from A to B is, concretely, the source code for a
359 -- verilog module having input ports of type A and output ports of type B;
360 -- the UniqueSupply lets us generate names.
361 data GArrowVerilog a b =
363 VerilogWrappedType a ->
364 VerilogWrappedType b ->
367 instance GArrow GArrowVerilog (,) where
368 ga_id = VerilogModule [] "ga_id" (\ inp outp -> zipTree ... "assign "++outp++" = "++inp)
369 ga_comp f g = VerilogModule [] "ga_comp"
370 ga_first :: g x y -> g (x ** z) (y ** z)
371 ga_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
372 ga_cancell f = VerilogModule [] "ga_cancell" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in2)
373 ga_cancelr f = VerilogModule [] "ga_cancelr" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in1)
374 ga_uncancell f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out1++"=1'b0;\n assign"++out2++"="++in1)
375 ga_uncancelr f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out2++"=1'b0;\n assign"++out1++"="++in1)
377 ga_unassoc :: g (x**(y**z)) ((x**y)**z)
379 instance GArrowDrop GArrowVerilog (,) where
382 instance GArrowCopy GArrowVerilog (,) where
385 instance GArrowSwap GArrowVerilog (,) where
388 instance GArrowLoop GArrowVerilog (,) where
391 instance GArrowLiteral GArrowVerilog (,) where
398 -- is there an official place to import this from so I don't have to write it myself?
400 ifThenElse True a _ = a
401 ifThenElse False _ b = b