1 {-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -XFlexibleContexts -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs #-}
6 import GHC.HetMet.CodeTypes hiding ((-))
7 import GHC.HetMet.GArrow
8 import Control.Category
10 import Prelude hiding ( id, (.) )
12 -- The best way to understand heterogeneous metaprogramming and
13 -- generalized arrows is to play around with this file, poking at the
14 -- examples until they fail to typecheck -- you'll learn a lot that
17 -- Once you've built the modified compiler, you can compile this file
20 -- $ inplace/bin/ghc-stage2 tutorial.hs
23 -- -XModalTypes adds a new syntactical expression, "code brackets":
24 code_fst = <[ \(x,y) -> x ]>
26 -- This new expression is the introduction form for modal types:
27 code_fst :: forall a b g. <[ (a,b) -> a ]>@g
29 -- Think of <[T]>@g as being the type of programs written in language
30 -- "g" which, when "executed", return a value of type "T". I mention
31 -- "language g" because the *heterogeneous* aspect of HetMet means
32 -- that we can limit the sorts of constructs allowed inside the code
33 -- brackets, permitting only a subset of Haskell (you have to use
34 -- Haskell syntax, though).
36 -- There is a second new expression form, "~~", called "escape":
38 code_fst_fst = <[ \z -> ~~code_fst (~~code_fst z) ]>
40 -- Note that ~~ binds more tightly than any other operator. There is
41 -- an alternate version, "~~$", which binds more weakly than any other
42 -- operator (this is really handy sometimes!). To demonstrate this,
43 -- the next two expressions differ only in superficial syntax:
45 example1 foo bar = <[ ~~$ foo bar ]>
46 example2 foo bar = <[ ~~( foo bar) ]>
47 -- example3 foo bar = <[ ~~ foo bar ]>
49 -- ... but the third one is completely different (and in fact, doesn't
50 -- even parse, but we'll get to that in a moment)
52 -- The escape operation must appear within code brackets. In truth,
53 -- it is really a "hole" punched in the code brackets -- the thing to
54 -- which the escape operator gets applied is typed as if it were
55 -- *outside* the code brackets. It must have type <[T]>, and the
56 -- escape operator allows it to be used *inside* code brackets as if
59 -- So, the escape operator is basically a way of pasting code
60 -- fragments into each other.
62 -- This is where those type variables after the "@" sign come in: if
63 -- you paste two pieces of code into a third, all three must be
64 -- written in the same language. We express this by unifying their
67 compose_code :: forall g a b c. <[a->b]>@g -> <[b->c]>@g -> <[a->c]>@g
68 compose_code x y = <[ \z -> ~~y (~~x z) ]>
70 -- Now, try commenting out the type ascription above and uncommenting
71 -- any of these three:
73 -- compose_code :: forall g h a b c. <[a->b]>@h -> <[b->c]>@g -> <[a->c]>@g
74 -- compose_code :: forall g h a b c. <[a->b]>@g -> <[b->c]>@h -> <[a->c]>@g
75 -- compose_code :: forall g h a b c. <[a->b]>@g -> <[b->c]>@g -> <[a->c]>@h
78 -- The typechecker won't let you get away with that -- you're trying
79 -- to force a type which is "too polymorphic" onto paste2. If the
80 -- compiler allowed that, the resulting metaprogram might try to
81 -- splice together programs written in different languages, resulting
84 -- NEW SCOPING RULES: The syntactical depth (or just "depth") of an
85 -- expression is the number of surrounding code-brackets minus the
86 -- number of surrounding escapes (this is strictly a syntax concept
87 -- and has NOTHING to do with the type system!). It is very important
88 -- to keep in mind that the scope of a bound variable extends only to
89 -- expressions at the same depth! To demonstrate, the following
90 -- expression will fail to parse:
92 -- badness = \x -> <[ x ]>
94 -- ...and in the following expression, the occurrence of "x" is bound
95 -- by the first (outer) lambda, not the second one:
97 no_shadowing_here = \x -> <[ \x -> ~~x ]>
99 -- Lastly, you can wrap code-brackets around an identifier in a
100 -- top-level, let, or where binding. Notice how GHC doesn't complain
101 -- here about defining an identifier twice!
104 <[ foo ]> = <[ \(x::Bool) -> x ]>
106 -- Now you can use foo (the second one!) inside code-brackets:
108 bar x = <[ foo ~~x ]>
110 bar :: forall g. <[Bool]>@g -> <[Bool]>@g
112 -- In fact, the identifiers have completely unrelated types. Which
113 -- brings up another important point: types are ALWAYS assigned
114 -- "relative to" depth zero. So although we imagine "foo" existing at
115 -- depth-one, its type is quite firmly established as <[ Bool -> Bool ]>
117 -- It has to be this way -- to see why, consider a term which is more
118 -- polymorphic than "foo":
120 <[ foo' ]> = <[ \x -> x ]>
124 <[ foo' ]> :: forall a g . <[ a -> a ]>@g
126 -- ...and there's no way to express the g-polymorphism entirely from
127 -- within the brackets.
129 -- So why does all of this matter? Mainly so that we can continue to use . We'd like
130 -- the "+" operator to work "as expected" -- in other words, we'd like
131 -- people to be able to write things like
133 increment_at_level1 = <[ \x -> x + 1 ]>
135 -- However, in unmodified haskell an identifier like (+) may have only
136 -- one type. In this case that type is:
138 -- (+) :: Num a => a -> a -> a
140 -- Now, we could simply decree that when (+) appears inside code
141 -- brackets, an "implicit ~~" is inserted, so the desugared expression
144 -- increment_at_level1 = <[ \x -> ~~(+) x 1 ]>
146 -- unfortunately this isn't going to work for guest languages that
147 -- don't have higher-order functions. Haskell uses curried arguments
148 -- because it has higher-order functions, but in a first-order guest
149 -- language a more sensible type for (+) would be:
151 -- (+) :: Num a => (a,a) -> a
153 -- ... or even something less polymorphic, like
155 -- (+) :: (Int,Int) -> Int
157 -- so to maintain flexibility, we allow an identifier to have
158 -- different types at different syntactic depths; this way type
159 -- choices made for Haskell don't get imposed on guest languages that
160 -- are missing some of its features.
162 -- In hindsight, what we REALLY want is for increment_at_level1 to
163 -- be desugared like this (much like the Arrow (|...|) syntax):
165 -- increment_at_level1 = <[ \x -> ~~( <[x]> + <[1]> ) ]>
167 -- ... because then we can declare
169 -- instance Num a => Num <[a]> where ...
173 -- instance Num <[Int]> where ...
175 -- unfortunately there's a major problem: knowing how to do this sort
176 -- of desugaring requires knowing the *arity* of a function. For
177 -- symbols we can kludge it by checking Haskell's parsing rules (there
178 -- are only a handful of unary symbols; all others are binary), but
179 -- this is crude and won't work at all for non-symbol identifiers.
180 -- And we can look at a type like x->y->z and say "oh, that's a
181 -- two-argument function", but sometimes GHC doesn't know the complete
182 -- type of an identifier in the midst of unification (i.e. "x has type
183 -- Int->a for some a, where a could be Int or Int->Int"), so guessing
184 -- the arity from the type cannot be done during parsing, which is
185 -- when we need to do this.
187 -- Okay, I think that's more or less a brain dump of why I changed the
188 -- scoping rules and the problems with the other solutions I tried.
190 -- I am very interested in hearing any suggestions on better ways of
191 -- dealing with this, so long as you can still use operators like (+)
192 -- in guest languages without higher-order functions.
200 -- The rest of this file contains a bunch of example programs:
201 -- exponentiation, dot-product, a bunch of classic MetaML idioms, and
202 -- a translation of Nanevski+Pfenning's two-stage regex matcher.
209 --------------------------------------------------------------------------------
210 -- Ye Olde and Most Venerable "pow" Function
215 else <[ \x -> x * ~~(pow (n - 1)) x ]>
218 -- a more efficient two-level pow
219 pow' 0 = <[ \x -> 1 ]>
220 pow' 1 = <[ \x -> x ]>
221 pow' n = if n `mod` 2==0
222 then <[ \x -> (\y -> y*y) (~~(pow' $ n `shiftR` 2) x) ]>
223 else <[ \x -> x * ~~(pow' $ n-1) x ]>
235 --------------------------------------------------------------------------------
238 -- This shows how to build a two-level program one step at a time by
239 -- slowly rearranging it until the brackets can be inserted.
242 -- a one-level function to compute the dot product of two vectors
243 dotproduct :: [Int] -> [Int] -> Int
250 (a*b)+(dotproduct ax bx)
252 -- A slightly modified version of the dot product: note that we
253 -- check for zeroes and ones to avoid multiplying. In a one-level
254 -- program this yields no advantage, however!
255 dotproduct' :: [Int] -> [Int] -> Int
261 (b:bx) -> (dotproduct' ax bx)
264 (b:bx) -> b+(dotproduct' ax bx)
268 (a*b)+(dotproduct' ax bx)
270 -- A two-level version of the dot product. Note how we ask for the first
271 -- vector, then produce a program which is optimized for multiplying
272 -- by that particular vector. If there are zeroes or ones in the
273 -- original vector, we will emit code which is faster than a one-level
276 --dotproduct'' :: forall g.
277 -- GuestLanguageAdd g Int =>
278 -- GuestLanguageMult g Int =>
279 -- GuestLanguageFromInteger g Int =>
280 -- [Int] -> <[ [Int] -> Int ]>@g
284 (0:ax) -> <[ \v2 -> case v2 of
286 (b:bx) -> ~~(dotproduct'' ax) bx ]>
287 (1:ax) -> <[ \v2 -> case v2 of
289 (b:bx) -> b + ~~(dotproduct'' ax) bx ]>
291 (a:ax) -> <[ \v2 -> case v2 of
293 (b:bx) -> ~~(guestIntegerLiteral a) * b + ~~(dotproduct'' ax) bx ]>
300 --------------------------------------------------------------------------------
301 -- Taha-Sheard "isomorphism for code types"
303 back :: forall a b c. (<[b]>@a -> <[c]>@a) -> <[ b->c ]>@a
304 back = \f -> <[ \x -> ~~(f <[x]>) ]>
306 forth :: forall a b c. <[b->c]>@a -> (<[b]>@a -> <[c]>@a)
307 forth = \f -> \x -> <[ ~~f ~~x ]>
311 --------------------------------------------------------------------------------
312 -- Examples of "running" code; these examples illustrate the sorts of
313 -- scoping problems that the Taha-Nielsen environment classifiers look
314 -- for in the context of HOMOGENEOUS metaprogramming. You can't
315 -- actually define these functions for ALL generalized arrows -- only
316 -- those for which you've defined some sort of interpretation in Haskell.
318 run :: forall a. (forall b. <[a]>@b) -> a
321 -- the typchecker correctly rejects this bogosity if you uncomment it:
322 -- bogus = <[ \x -> ~~( run <[ x ]> ) ]>
324 -- The Calcano-Moggi-Taha paper on environment classifier inference
325 -- had a special type for closed code and two special expressions
326 -- "close" and "open". These are unnecessary in SystemFC1 where we
327 -- can use higher-rank polymorphism to get the same result (although
328 -- in truth it's cheating a bit since their type inference is
329 -- decidable with no annotations, whereas Rank-N inference is not):
331 data ClosedCode a = ClosedCode (forall b. <[a]>@b)
333 open :: forall a b. ClosedCode a -> <[a]>@b
334 open (ClosedCode x) = x
336 close :: (forall b. <[a]>@b) -> ClosedCode a
337 close x = ClosedCode x
339 run_closed :: ClosedCode a -> a
340 run_closed = undefined
344 --------------------------------------------------------------------------------
345 -- A two-level Regular Expression matcher, adapted from Nanevski+Pfenning, Figure 6
358 -- a continuation-passing-style matcher
360 accept :: Stream s => Regex -> (s -> Bool) -> s -> Bool
365 accept (Plus e1 e2) k s =
366 (accept e1 k s) || (accept e2 k s)
368 accept (Times e1 e2) k s =
369 (accept e1 (accept e2 k)) s
371 accept (Star e) k s =
372 (k s) || (accept e (\s' -> accept (Star e) k s') s)
373 -- FIXME: this will loop forever if you give it (Star x) where x can
374 -- match the empty string
376 accept (Const c) k s =
379 else (s_head s) == c && k (s_tail s)
381 class GuestStream g a where
382 <[ gs_empty ]> :: <[ a -> Bool ]>@g
383 <[ gs_head ]> :: <[ a -> Char ]>@g
384 <[ gs_tail ]> :: <[ a -> a ]>@g
386 class GuestEqChar g where
387 <[ (==) ]> :: <[ Char -> Char -> Bool ]>@g
393 GuestCharLiteral c =>
394 GuestLanguageBool c =>
399 staged_accept Empty k =
400 <[ \s -> gs_empty s ]>
402 -- note that code for "k" gets duplicated here
403 staged_accept (Plus e1 e2) k =
404 <[ \s -> (~~(staged_accept e1 k) s) || (~~(staged_accept e2 k) s) ]>
406 staged_accept (Times e1 e2) k =
407 <[ \s -> ~~(staged_accept e1 (staged_accept e2 k)) s ]>
409 staged_accept (Star e) k =
412 -- loop :: <[s -> Bool]>@g
413 loop = <[ \s -> ~~k s || ~~(staged_accept e loop) s ]>
414 -- note that loop is not (forall c s. <[s -> Bool]>@c)
415 -- because "k" is free in loop; it is analogous to the free
416 -- environment variable in Nanevski's example
418 staged_accept (Const c) k =
419 <[ \s -> if gs_empty s
421 else (gs_head s) == ~~(guestCharLiteral c) && ~~k (gs_tail s) ]>
423 -- this type won't work unless the case for (Star e) is commented out;
427 -- GuestStream c s =>
428 -- GuestLanguageBool c =>
432 -- GuestStream c s =>
433 -- GuestLanguageBool c =>
440 --------------------------------------------------------------------------------
443 -- This more or less "undoes" the flatten function. People often ask
444 -- me how you "translate generalized arrows back into multi-level
445 -- terms".. I'm not sure why you'd want to do that, but this is how:
446 newtype Code x y = Code { unCode :: forall a. <[ x -> y ]>@a }
448 instance Category Code where
449 id = Code <[ \x -> x ]>
450 f . g = Code <[ \x -> ~~(unCode f) (~~(unCode g) x) ]>
452 instance GArrow Code (,) where
453 ga_first f = Code <[ \(x,y) -> ((~~(unCode f) x),y) ]>
454 ga_second f = Code <[ \(x,y) -> (x ,(~~(unCode f) y)) ]>
455 ga_cancell = Code <[ \(_,x) -> x ]>
456 ga_cancelr = Code <[ \(x,_) -> x ]>
457 ga_uncancell = Code <[ \x -> (%%(),x) ]>
458 ga_uncancelr = Code <[ \x -> (x,%%()) ]>
459 ga_assoc = Code <[ \((x,y),z) -> (x,(y,z)) ]>
460 ga_unassoc = Code <[ \(x,(y,z)) -> ((x,y),z) ]>
465 --------------------------------------------------------------------------------
468 class GArrow g (**) => BiGArrow g (**) where
469 -- Note that we trust the user's pair of functions actually are
470 -- mutually inverse; confirming this in the type system would
471 -- require very powerful dependent types (such as Coq's). However,
472 -- the consequences of failure here are much more mild than failures
473 -- in BiArrow.inv: if the functions below are not mutually inverse,
474 -- the LoggingBiGArrow will simply compute the wrong result rather
475 -- than fail in some manner outside the language's semantics.
476 biga_arr :: (x -> y) -> (y -> x) -> g x y
477 biga_inv :: g x y -> g y x
479 -- For any GArrow instance, its mutually inverse pairs form a BiGArrow
480 data GArrow g (**) => GArrowInversePair g (**) x y =
481 GArrowInversePair { forward :: g x y , backward :: g y x }
482 instance GArrow g (**) => Category (GArrowInversePair g (**)) where
483 id = GArrowInversePair { forward = id , backward = id }
484 f . g = GArrowInversePair { forward = (forward f) . (forward g) , backward = (backward g) . (backward f) }
485 instance GArrow g (**) => GArrow (GArrowInversePair g (**)) (**) where
486 ga_first f = GArrowInversePair { forward = ga_first (forward f), backward = ga_first (backward f) }
487 ga_second f = GArrowInversePair { forward = ga_second (forward f), backward = ga_second (backward f) }
488 ga_cancell = GArrowInversePair { forward = ga_cancell , backward = ga_uncancell }
489 ga_cancelr = GArrowInversePair { forward = ga_cancelr , backward = ga_uncancelr }
490 ga_uncancell = GArrowInversePair { forward = ga_uncancell , backward = ga_cancell }
491 ga_uncancelr = GArrowInversePair { forward = ga_uncancelr , backward = ga_cancelr }
492 ga_assoc = GArrowInversePair { forward = ga_assoc , backward = ga_unassoc }
493 ga_unassoc = GArrowInversePair { forward = ga_unassoc , backward = ga_assoc }
494 instance GArrowSwap g (**) => GArrowSwap (GArrowInversePair g (**)) (**) where
495 ga_swap = GArrowInversePair { forward = ga_swap , backward = ga_swap }
496 instance (GArrowDrop g (**), GArrowCopy g (**)) => GArrowCopy (GArrowInversePair g (**)) (**) where
497 ga_copy = GArrowInversePair { forward = ga_copy , backward = ga_second ga_drop >>> ga_cancelr }
498 -- but notice that we can't (in general) get
499 -- instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...
502 -- For that, we need PreLenses, which "log the history" where necessary.
503 -- I call this a "PreLens" because it consists of the data required
504 -- for a Lens (as in BCPierce's Lenses) but does not necessarily
505 -- satisfy the putget/getput laws. Specifically, the "extra stuff" we
506 -- store is the inversion function.
507 newtype PreLens x y = PreLens { preLens :: x -> (y , y->x) }
509 instance Category PreLens where
510 id = PreLens { preLens = \x -> (x, (\x -> x)) }
511 f . g = PreLens { preLens = \x -> let (gx,g') = (preLens g) x in let (fgx,f') = (preLens f) gx in (fgx , \q -> g' (f' q)) }
513 instance GArrow PreLens (,) where
514 ga_first f = PreLens { preLens = \(x,z) -> let (y,f') = (preLens f) x in ((y,z),(\(q1,q2) -> (f' q1,q2))) }
515 ga_second f = PreLens { preLens = \(z,x) -> let (y,f') = (preLens f) x in ((z,y),(\(q1,q2) -> (q1,f' q2))) }
516 ga_cancell = PreLens { preLens = \(_,x) -> (x, (\x -> ((),x))) }
517 ga_cancelr = PreLens { preLens = \(x,_) -> (x, (\x -> (x,()))) }
518 ga_uncancell = PreLens { preLens = \x -> (((),x), (\(_,x) -> x)) }
519 ga_uncancelr = PreLens { preLens = \x -> ((x,()), (\(x,_) -> x)) }
520 ga_assoc = PreLens { preLens = \((x,y),z) -> ( (x,(y,z)) , (\(x,(y,z)) -> ((x,y),z)) ) }
521 ga_unassoc = PreLens { preLens = \(x,(y,z)) -> ( ((x,y),z) , (\((x,y),z) -> (x,(y,z))) ) }
523 instance GArrowDrop PreLens (,) where
524 ga_drop = PreLens { preLens = \x -> (() , (\() -> x)) }
525 instance GArrowCopy PreLens (,) where
526 ga_copy = PreLens { preLens = \x -> ((x,x) , fst) }
527 instance GArrowSwap PreLens (,) where
528 ga_swap = PreLens { preLens = \(x,y) -> ((y,x) , (\(z,q) -> (q,z))) }
533 Lens :: forall x y c1 c2 . ((x,c1)->(y,c2)) -> ((y,c2)->(x,c1)) -> Lens x y
535 -- can we make lenses out of GArrows other than (->)?
536 instance Category Lens where
537 id = Lens (\x -> x) (\x -> x)
538 (Lens g1 g2) . (Lens f1 f2) = Lens (\(x,(c1,c2)) -> let (y,fc) = f1 (x,c1) in let (z,gc) = g1 (y,c2) in (z,(fc,gc)))
539 (\(z,(c1,c2)) -> let (y,gc) = g2 (z,c2) in let (x,fc) = f2 (y,c1) in (x,(fc,gc)))
541 instance GArrow Lens (,) where
542 ga_first (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x1,c) in ((y,x2),c'))
543 (\((x1,x2),c) -> let (y,c') = f2 (x1,c) in ((y,x2),c'))
544 ga_second (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x2,c) in ((x1,y),c'))
545 (\((x1,x2),c) -> let (y,c') = f2 (x2,c) in ((x1,y),c'))
546 ga_cancell = Lens (\(((),x),()) -> ( x ,()))
547 (\( x ,()) -> (((),x),()))
548 ga_uncancell = Lens (\( x ,()) -> (((),x),()))
549 (\(((),x),()) -> ( x ,()))
550 ga_cancelr = Lens (\((x,()),()) -> ( x ,()))
551 (\( x ,()) -> ((x,()),()))
552 ga_uncancelr = Lens (\( x ,()) -> ((x,()),()))
553 (\((x,()),()) -> ( x ,()))
554 ga_assoc = Lens (\(((x,y),z),()) -> ((x,(y,z)),()))
555 (\((x,(y,z)),()) -> (((x,y),z),()))
556 ga_unassoc = Lens (\((x,(y,z)),()) -> (((x,y),z),()))
557 (\(((x,y),z),()) -> ((x,(y,z)),()))
559 instance GArrowDrop Lens (,) where
560 ga_drop = Lens (\(x,()) -> ((),x)) (\((),x) -> (x,()))
561 instance GArrowCopy Lens (,) where
562 ga_copy = Lens (\(x,()) -> ((x,x),())) (\((x,_),()) -> (x,()))
563 instance GArrowSwap Lens (,) where
564 ga_swap = Lens (\((x,y),()) -> ((y,x),())) (\((x,y),()) -> ((y,x),()))
566 instance BiGArrow Lens (,) where
567 biga_arr f f' = Lens (\(x,()) -> ((f x),())) (\(x,()) -> ((f' x),()))
568 biga_inv (Lens f1 f2) = Lens f2 f1
573 --------------------------------------------------------------------------------
574 -- An example generalized arrow
576 -- *** this will be finished and posted by 14-Mar-2011; the code
577 -- *** below is just a sketch ***
580 -- A verilog module is an SDoc (chunk of text) giving the module's
581 -- definition. The UniqueSupply avoids name clashes.
584 [VerilogModule] -- dependencies
585 String -> -- module name
586 (Tree String -> -- input port names
587 Tree String -> -- output port names
588 SDoc) -- raw verilog code for the body
591 instance Show VerilogModule where
592 show VerilogModule dep name body =
593 "module "++name++"(FIXME)"++(body FIXME FIXME)
595 data VerilogWrappedType a =
596 { vwt_rep :: String }
598 -- A "verilog garrow" from A to B is, concretely, the source code for a
599 -- verilog module having input ports of type A and output ports of type B;
600 -- the UniqueSupply lets us generate names.
601 data GArrowVerilog a b =
603 VerilogWrappedType a ->
604 VerilogWrappedType b ->
607 instance GArrow GArrowVerilog (,) where
608 ga_id = VerilogModule [] "ga_id" (\ inp outp -> zipTree ... "assign "++outp++" = "++inp)
609 ga_comp f g = VerilogModule [] "ga_comp"
610 ga_first :: g x y -> g (x ** z) (y ** z)
611 ga_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
612 ga_cancell f = VerilogModule [] "ga_cancell" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in2)
613 ga_cancelr f = VerilogModule [] "ga_cancelr" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in1)
614 ga_uncancell f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out1++"=1'b0;\n assign"++out2++"="++in1)
615 ga_uncancelr f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out2++"=1'b0;\n assign"++out1++"="++in1)
617 ga_unassoc :: g (x**(y**z)) ((x**y)**z)
619 instance GArrowDrop GArrowVerilog (,) where
622 instance GArrowCopy GArrowVerilog (,) where
625 instance GArrowSwap GArrowVerilog (,) where
628 instance GArrowLoop GArrowVerilog (,) where
631 instance GArrowLiteral GArrowVerilog (,) where
640 lambda calculus interpreter
646 This requires higher-order functions in the second level...
648 eval :: Exp -> a Env Val
649 eval (Var s) = <[ lookup s ]>
650 eval (Add e1 e2) = <[ let (Num v1) = ~(eval e1)
651 in let (Num v2) = ~(eval e2)
653 eval (If e1 e2 e3) = <[ let v1 = ~(eval e1) in
659 eval (Var s) = proc env ->
660 returnA -< fromJust (lookup s env)
661 eval (Add e1 e2) = proc env ->
662 (eval e1 -< env) `bind` \ ~(Num u) ->
663 (eval e2 -< env) `bind` \ ~(Num v) ->
664 returnA -< Num (u + v)
665 eval (If e1 e2 e3) = proc env ->
666 (eval e1 -< env) `bind` \ ~(Bl b) ->
667 if b then eval e2 -< env
669 eval (Lam x e) = proc env ->
670 returnA -< Fun (proc v -> eval e -< (x,v):env)
671 eval (App e1 e2) = proc env ->
672 (eval e1 -< env) `bind` \ ~(Fun f) ->
673 (eval e2 -< env) `bind` \ v ->
676 eval (Var s) = <[ \env -> fromJust (lookup s env) ]>
677 eval (Add e1 e2) = <[ \env -> (~(eval e1) env) + (~(eval e2) env) ]>
678 eval (If e1 e2 e3) = <[ \env -> if ~(eval e1) env
681 eval (Lam x e) = <[ \env -> Fun (\v -> ~(eval e) ((x,v):env)) ]>
682 eval (App e1 e2) = <[ \env -> case ~(eval e1) env of
683 (Fun f) -> f (~(eval e2) env) ]>
684 eval (Var s) <[env]> = <[ fromJust (lookup s env) ]>
685 eval (Add e1 e2) <[env]> = <[ (~(eval e1) env) + (~(eval e2) env) ]>
693 immutable heap with cycles
695 -- an immutable heap; maps Int->(Int,Int)
697 alloc :: A (Int,Int) Int
698 lookup :: A Int (Int,Int)
700 onetwocycle :: A (Int,Int) (Int,Int)
709 alloc :: <[ (Int,Int) -> Int ]>
710 lookup :: <[ Int -> (Int,Int) ]>
712 onetwocycle :: <[ (Int,Int) ]> -> <[ (Int,Int) ]>
714 let x' = ~alloc (1,~y)
715 in let y' = ~alloc (2,~x)
719 onetwocycle' :: <[ (Int,Int) -> (Int,Int) ]>
720 onetwocycle' = back2 onetwocycle
728 The example may seem a little contrived, but its purpose is to
729 illustrate the be- haviour when the argument of mapC refers both to
730 its parameter and a free vari- able (n).
733 -- we can use mapA rather than mapC (from page 100)
735 mapA f = proc xs -> case xs of
736 [] -> returnA -< [] x:xs’ -> do y <- f -< x
737 ys’ <- mapA f -< xs’ returnA -< y:ys
741 ~(mapA <[ \x-> (~(delay 0) n, x) ]> )
746 ~(mapA <[ \x-> (~(delay 0) n, x) ]> ) xs ]>
759 (arr id *** (delaysA >>> delay []) >>>
762 nor :: SF (Bool,Bool) Bool
763 nor = arr (not.uncurry (||))
768 b <- delay False -< a
769 returnA -< a && not b
772 proc (reset,set) -> do
773 rec c <- delay False -< nor
774 reset d d <- delay True -< nor set c
777 halfAdd :: Arrow arr => arr (Bool,Bool) (Bool,Bool)
779 proc (x,y) -> returnA -< (x&&y, x/=y)
782 Arrow arr => arr (Bool,Bool,Bool) (Bool,Bool)
785 (c1,s1) <- halfAdd -< (x,y)
786 (c2,s2) <- halfAdd -< (s1,c)
787 returnA -< (c1||c2,s2)
789 Here is the appendix of Hughes04:
790 module Circuits where
791 import Control.Arrow import List
792 class ArrowLoop a => ArrowCircuit a where delay :: b -> a b b
793 nor :: Arrow a => a (Bool,Bool) Bool nor = arr (not.uncurry (||))
794 flipflop :: ArrowCircuit a => a (Bool,Bool) (Bool,Bool) flipflop = loop (arr (\((a,b),~(c,d)) -> ((a,d),(b,c))) >>>
795 nor *** nor >>> delay (False,True) >>> arr id &&& arr id)
796 class Signal a where showSignal :: [a] -> String
797 instance Signal Bool where showSignal bs = concat top++"\n"++concat bot++"\n"
798 where (top,bot) = unzip (zipWith sh (False:bs) bs) sh True True = ("__"," ") sh True False = (" ","|_") sh False True = (" _","| ")
799 sh False False = (" ","__")
800 instance (Signal a,Signal b) => Signal showSignal xys = showSignal (map fst showSignal (map snd
801 instance Signal a => Signal [a] where showSignal = concat . map showSignal
802 sig = concat . map (uncurry replicate)
803 (a,b) where xys) ++ xys)
805 flipflopInput = sig [(5,(False,False)),(2,(False,True)),(5,(False,False)),
806 (2,(True,False)),(5,(False,False)),(2,(True,True)), (6,(False,False))]
812 -- from Hughes' "programming with Arrows"
814 mapC :: ArrowChoice arr => arr (env,a) b -> arr (env,[a]) [b] mapC c = proc (env,xs) ->
815 case xs of [] -> returnA -< [] x:xs’ -> do y <- c -< (env,x)
816 ys <- mapC c -< (env,xs’) returnA -< y:ys
818 example2 = proc (n,xs) -> (| mapC (\x-> do delay 0 -< n
819 &&& do returnA -< x) |) xs