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
212 pow :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer -> <[ Integer -> Integer ]>@c
216 else <[ \x -> x * ~~(pow (n - 1)) x ]>
219 -- a more efficient two-level pow
220 pow' :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer -> <[ Integer -> Integer ]>@c
221 pow' 0 = <[ \x -> 1 ]>
222 pow' 1 = <[ \x -> x ]>
223 pow' n = if n `mod` 2==0
224 then <[ \x -> (\y -> y*y) (~~(pow' $ n `shiftR` 2) x) ]>
225 else <[ \x -> x * ~~(pow' $ n-1) x ]>
236 --------------------------------------------------------------------------------
239 -- This shows how to build a two-level program one step at a time by
240 -- slowly rearranging it until the brackets can be inserted.
243 -- a one-level function to compute the dot product of two vectors
244 dotproduct :: [Int] -> [Int] -> Int
251 (a*b)+(dotproduct ax bx)
253 -- A slightly modified version of the dot product: note that we
254 -- check for zeroes and ones to avoid multiplying. In a one-level
255 -- program this yields no advantage, however!
256 dotproduct' :: [Int] -> [Int] -> Int
262 (b:bx) -> (dotproduct' ax bx)
265 (b:bx) -> b+(dotproduct' ax bx)
269 (a*b)+(dotproduct' ax bx)
271 -- A two-level version of the dot product. Note how we ask for the first
272 -- vector, then produce a program which is optimized for multiplying
273 -- by that particular vector. If there are zeroes or ones in the
274 -- original vector, we will emit code which is faster than a one-level
277 dotproduct'' :: forall g.
278 GuestLanguageAdd g Integer =>
279 GuestLanguageMult g Integer =>
280 GuestIntegerLiteral g =>
281 [Integer] -> <[ [Integer] -> Integer ]>@g
285 (0:ax) -> <[ \v2 -> case v2 of
287 (b:bx) -> ~~(dotproduct'' ax) bx ]>
288 (1:ax) -> <[ \v2 -> case v2 of
290 (b:bx) -> b + ~~(dotproduct'' ax) bx ]>
292 (a:ax) -> <[ \v2 -> case v2 of
294 (b:bx) -> ~~(guestIntegerLiteral a) * b + ~~(dotproduct'' ax) bx ]>
299 --------------------------------------------------------------------------------
300 -- Taha-Sheard "isomorphism for code types"
302 back :: forall a b c. (<[b]>@a -> <[c]>@a) -> <[ b->c ]>@a
303 back = \f -> <[ \x -> ~~(f <[x]>) ]>
305 forth :: forall a b c. <[b->c]>@a -> (<[b]>@a -> <[c]>@a)
306 forth = \f -> \x -> <[ ~~f ~~x ]>
310 --------------------------------------------------------------------------------
311 -- Examples of "running" code; these examples illustrate the sorts of
312 -- scoping problems that the Taha-Nielsen environment classifiers look
313 -- for in the context of HOMOGENEOUS metaprogramming. You can't
314 -- actually define these functions for ALL generalized arrows -- only
315 -- those for which you've defined some sort of interpretation in Haskell.
317 run :: forall a. (forall b. <[a]>@b) -> a
320 -- the typchecker correctly rejects this bogosity if you uncomment it:
321 -- bogus = <[ \x -> ~~( run <[ x ]> ) ]>
323 -- The Calcano-Moggi-Taha paper on environment classifier inference
324 -- had a special type for closed code and two special expressions
325 -- "close" and "open". These are unnecessary in SystemFC1 where we
326 -- can use higher-rank polymorphism to get the same result (although
327 -- in truth it's cheating a bit since their type inference is
328 -- decidable with no annotations, whereas Rank-N inference is not):
330 data ClosedCode a = ClosedCode (forall b. <[a]>@b)
332 open :: forall a b. ClosedCode a -> <[a]>@b
333 open (ClosedCode x) = x
335 close :: (forall b. <[a]>@b) -> ClosedCode a
336 close x = ClosedCode x
338 run_closed :: ClosedCode a -> a
339 run_closed = undefined
343 --------------------------------------------------------------------------------
344 -- A two-level Regular Expression matcher, adapted from Nanevski+Pfenning, Figure 6
357 -- a continuation-passing-style matcher
359 accept :: Stream s => Regex -> (s -> Bool) -> s -> Bool
364 accept (Plus e1 e2) k s =
365 (accept e1 k s) || (accept e2 k s)
367 accept (Times e1 e2) k s =
368 (accept e1 (accept e2 k)) s
370 accept (Star e) k s =
371 (k s) || (accept e (\s' -> accept (Star e) k s') s)
372 -- FIXME: this will loop forever if you give it (Star x) where x can
373 -- match the empty string
375 accept (Const c) k s =
378 else (s_head s) == c && k (s_tail s)
380 class GuestStream g a where
381 <[ gs_empty ]> :: <[ a -> Bool ]>@g
382 <[ gs_head ]> :: <[ a -> Char ]>@g
383 <[ gs_tail ]> :: <[ a -> a ]>@g
385 class GuestEqChar g where
386 <[ (==) ]> :: <[ Char -> Char -> Bool ]>@g
392 GuestCharLiteral c =>
393 GuestLanguageBool c =>
398 staged_accept Empty k =
399 <[ \s -> gs_empty s ]>
401 -- note that code for "k" gets duplicated here
402 staged_accept (Plus e1 e2) k =
403 <[ \s -> (~~(staged_accept e1 k) s) || (~~(staged_accept e2 k) s) ]>
405 staged_accept (Times e1 e2) k =
406 <[ \s -> ~~(staged_accept e1 (staged_accept e2 k)) s ]>
408 staged_accept (Star e) k =
411 -- loop :: <[s -> Bool]>@g
412 loop = <[ \s -> ~~k s || ~~(staged_accept e loop) s ]>
413 -- note that loop is not (forall c s. <[s -> Bool]>@c)
414 -- because "k" is free in loop; it is analogous to the free
415 -- 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) ]>
424 -- this type won't work unless the case for (Star e) is commented out;
428 -- GuestStream c s =>
429 -- GuestLanguageBool c =>
433 -- GuestStream c s =>
434 -- GuestLanguageBool c =>
441 --------------------------------------------------------------------------------
445 -- This more or less "undoes" the flatten function. People often ask
446 -- me how you "translate generalized arrows back into multi-level
447 -- terms".. I'm not sure why you'd want to do that, but this is how:
448 newtype Code x y = Code { unCode :: forall a. <[ x -> y ]>@a }
450 instance Category Code where
451 id = Code <[ \x -> x ]>
452 f . g = Code <[ \x -> ~~(unCode f) (~~(unCode g) x) ]>
454 instance GArrow Code (,) where
455 ga_first f = Code <[ \(x,y) -> ((~~(unCode f) x),y) ]>
456 ga_second f = Code <[ \(x,y) -> (x ,(~~(unCode f) y)) ]>
457 ga_cancell = Code <[ \(_,x) -> x ]>
459 ga_cancelr = Code <[ \(x,_) -> x ]>
460 ga_uncancell = Code <[ \x -> (%%(),x) ]>
461 ga_uncancelr = Code <[ \x -> (x,%%()) ]>
462 ga_assoc = Code <[ \((x,y),z) -> (x,(y,z)) ]>
463 ga_unassoc = Code <[ \(x,(y,z)) -> ((x,y),z) ]>
468 --------------------------------------------------------------------------------
471 class GArrow g (**) => BiGArrow g (**) where
472 -- Note that we trust the user's pair of functions actually are
473 -- mutually inverse; confirming this in the type system would
474 -- require very powerful dependent types (such as Coq's). However,
475 -- the consequences of failure here are much more mild than failures
476 -- in BiArrow.inv: if the functions below are not mutually inverse,
477 -- the LoggingBiGArrow will simply compute the wrong result rather
478 -- than fail in some manner outside the language's semantics.
479 biga_arr :: (x -> y) -> (y -> x) -> g x y
480 biga_inv :: g x y -> g y x
482 -- For any GArrow instance, its mutually inverse pairs form a BiGArrow
483 data GArrow g (**) => GArrowInversePair g (**) x y =
484 GArrowInversePair { forward :: g x y , backward :: g y x }
485 instance GArrow g (**) => Category (GArrowInversePair g (**)) where
486 id = GArrowInversePair { forward = id , backward = id }
487 f . g = GArrowInversePair { forward = (forward f) . (forward g) , backward = (backward g) . (backward f) }
488 instance GArrow g (**) => GArrow (GArrowInversePair g (**)) (**) where
489 ga_first f = GArrowInversePair { forward = ga_first (forward f), backward = ga_first (backward f) }
490 ga_second f = GArrowInversePair { forward = ga_second (forward f), backward = ga_second (backward f) }
491 ga_cancell = GArrowInversePair { forward = ga_cancell , backward = ga_uncancell }
492 ga_cancelr = GArrowInversePair { forward = ga_cancelr , backward = ga_uncancelr }
493 ga_uncancell = GArrowInversePair { forward = ga_uncancell , backward = ga_cancell }
494 ga_uncancelr = GArrowInversePair { forward = ga_uncancelr , backward = ga_cancelr }
495 ga_assoc = GArrowInversePair { forward = ga_assoc , backward = ga_unassoc }
496 ga_unassoc = GArrowInversePair { forward = ga_unassoc , backward = ga_assoc }
497 instance GArrowSwap g (**) => GArrowSwap (GArrowInversePair g (**)) (**) where
498 ga_swap = GArrowInversePair { forward = ga_swap , backward = ga_swap }
499 instance (GArrowDrop g (**), GArrowCopy g (**)) => GArrowCopy (GArrowInversePair g (**)) (**) where
500 ga_copy = GArrowInversePair { forward = ga_copy , backward = ga_second ga_drop >>> ga_cancelr }
501 -- but notice that we can't (in general) get
502 -- instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...
505 -- For that, we need PreLenses, which "log the history" where necessary.
506 -- I call this a "PreLens" because it consists of the data required
507 -- for a Lens (as in BCPierce's Lenses) but does not necessarily
508 -- satisfy the putget/getput laws. Specifically, the "extra stuff" we
509 -- store is the inversion function.
510 newtype PreLens x y = PreLens { preLens :: x -> (y , y->x) }
512 instance Category PreLens where
513 id = PreLens { preLens = \x -> (x, (\x -> x)) }
514 f . g = PreLens { preLens = \x -> let (gx,g') = (preLens g) x in let (fgx,f') = (preLens f) gx in (fgx , \q -> g' (f' q)) }
516 instance GArrow PreLens (,) where
517 ga_first f = PreLens { preLens = \(x,z) -> let (y,f') = (preLens f) x in ((y,z),(\(q1,q2) -> (f' q1,q2))) }
518 ga_second f = PreLens { preLens = \(z,x) -> let (y,f') = (preLens f) x in ((z,y),(\(q1,q2) -> (q1,f' q2))) }
519 ga_cancell = PreLens { preLens = \(_,x) -> (x, (\x -> ((),x))) }
520 ga_cancelr = PreLens { preLens = \(x,_) -> (x, (\x -> (x,()))) }
521 ga_uncancell = PreLens { preLens = \x -> (((),x), (\(_,x) -> x)) }
522 ga_uncancelr = PreLens { preLens = \x -> ((x,()), (\(x,_) -> x)) }
523 ga_assoc = PreLens { preLens = \((x,y),z) -> ( (x,(y,z)) , (\(x,(y,z)) -> ((x,y),z)) ) }
524 ga_unassoc = PreLens { preLens = \(x,(y,z)) -> ( ((x,y),z) , (\((x,y),z) -> (x,(y,z))) ) }
526 instance GArrowDrop PreLens (,) where
527 ga_drop = PreLens { preLens = \x -> (() , (\() -> x)) }
528 instance GArrowCopy PreLens (,) where
529 ga_copy = PreLens { preLens = \x -> ((x,x) , fst) }
530 instance GArrowSwap PreLens (,) where
531 ga_swap = PreLens { preLens = \(x,y) -> ((y,x) , (\(z,q) -> (q,z))) }
536 Lens :: forall x y c1 c2 . ((x,c1)->(y,c2)) -> ((y,c2)->(x,c1)) -> Lens x y
538 -- can we make lenses out of GArrows other than (->)?
539 instance Category Lens where
540 id = Lens (\x -> x) (\x -> x)
541 (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)))
542 (\(z,(c1,c2)) -> let (y,gc) = g2 (z,c2) in let (x,fc) = f2 (y,c1) in (x,(fc,gc)))
544 instance GArrow Lens (,) where
545 ga_first (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x1,c) in ((y,x2),c'))
546 (\((x1,x2),c) -> let (y,c') = f2 (x1,c) in ((y,x2),c'))
547 ga_second (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x2,c) in ((x1,y),c'))
548 (\((x1,x2),c) -> let (y,c') = f2 (x2,c) in ((x1,y),c'))
549 ga_cancell = Lens (\(((),x),()) -> ( x ,()))
550 (\( x ,()) -> (((),x),()))
551 ga_uncancell = Lens (\( x ,()) -> (((),x),()))
552 (\(((),x),()) -> ( x ,()))
553 ga_cancelr = Lens (\((x,()),()) -> ( x ,()))
554 (\( x ,()) -> ((x,()),()))
555 ga_uncancelr = Lens (\( x ,()) -> ((x,()),()))
556 (\((x,()),()) -> ( x ,()))
557 ga_assoc = Lens (\(((x,y),z),()) -> ((x,(y,z)),()))
558 (\((x,(y,z)),()) -> (((x,y),z),()))
559 ga_unassoc = Lens (\((x,(y,z)),()) -> (((x,y),z),()))
560 (\(((x,y),z),()) -> ((x,(y,z)),()))
562 instance GArrowDrop Lens (,) where
563 ga_drop = Lens (\(x,()) -> ((),x)) (\((),x) -> (x,()))
564 instance GArrowCopy Lens (,) where
565 ga_copy = Lens (\(x,()) -> ((x,x),())) (\((x,_),()) -> (x,()))
566 instance GArrowSwap Lens (,) where
567 ga_swap = Lens (\((x,y),()) -> ((y,x),())) (\((x,y),()) -> ((y,x),()))
569 instance BiGArrow Lens (,) where
570 biga_arr f f' = Lens (\(x,()) -> ((f x),())) (\(x,()) -> ((f' x),()))
571 biga_inv (Lens f1 f2) = Lens f2 f1
576 --------------------------------------------------------------------------------
577 -- An example generalized arrow
579 -- *** this will be finished and posted by 14-Mar-2011; the code
580 -- *** below is just a sketch ***
583 -- A verilog module is an SDoc (chunk of text) giving the module's
584 -- definition. The UniqueSupply avoids name clashes.
587 [VerilogModule] -- dependencies
588 String -> -- module name
589 (Tree String -> -- input port names
590 Tree String -> -- output port names
591 SDoc) -- raw verilog code for the body
594 instance Show VerilogModule where
595 show VerilogModule dep name body =
596 "module "++name++"(FIXME)"++(body FIXME FIXME)
598 data VerilogWrappedType a =
599 { vwt_rep :: String }
601 -- A "verilog garrow" from A to B is, concretely, the source code for a
602 -- verilog module having input ports of type A and output ports of type B;
603 -- the UniqueSupply lets us generate names.
604 data GArrowVerilog a b =
606 VerilogWrappedType a ->
607 VerilogWrappedType b ->
610 instance GArrow GArrowVerilog (,) where
611 ga_id = VerilogModule [] "ga_id" (\ inp outp -> zipTree ... "assign "++outp++" = "++inp)
612 ga_comp f g = VerilogModule [] "ga_comp"
613 ga_first :: g x y -> g (x ** z) (y ** z)
614 ga_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
615 ga_cancell f = VerilogModule [] "ga_cancell" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in2)
616 ga_cancelr f = VerilogModule [] "ga_cancelr" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in1)
617 ga_uncancell f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out1++"=1'b0;\n assign"++out2++"="++in1)
618 ga_uncancelr f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out2++"=1'b0;\n assign"++out1++"="++in1)
620 ga_unassoc :: g (x**(y**z)) ((x**y)**z)
622 instance GArrowDrop GArrowVerilog (,) where
625 instance GArrowCopy GArrowVerilog (,) where
628 instance GArrowSwap GArrowVerilog (,) where
631 instance GArrowLoop GArrowVerilog (,) where
634 instance GArrowLiteral GArrowVerilog (,) where
643 lambda calculus interpreter
649 This requires higher-order functions in the second level...
651 eval :: Exp -> a Env Val
652 eval (Var s) = <[ lookup s ]>
653 eval (Add e1 e2) = <[ let (Num v1) = ~(eval e1)
654 in let (Num v2) = ~(eval e2)
656 eval (If e1 e2 e3) = <[ let v1 = ~(eval e1) in
662 eval (Var s) = proc env ->
663 returnA -< fromJust (lookup s env)
664 eval (Add e1 e2) = proc env ->
665 (eval e1 -< env) `bind` \ ~(Num u) ->
666 (eval e2 -< env) `bind` \ ~(Num v) ->
667 returnA -< Num (u + v)
668 eval (If e1 e2 e3) = proc env ->
669 (eval e1 -< env) `bind` \ ~(Bl b) ->
670 if b then eval e2 -< env
672 eval (Lam x e) = proc env ->
673 returnA -< Fun (proc v -> eval e -< (x,v):env)
674 eval (App e1 e2) = proc env ->
675 (eval e1 -< env) `bind` \ ~(Fun f) ->
676 (eval e2 -< env) `bind` \ v ->
679 eval (Var s) = <[ \env -> fromJust (lookup s env) ]>
680 eval (Add e1 e2) = <[ \env -> (~(eval e1) env) + (~(eval e2) env) ]>
681 eval (If e1 e2 e3) = <[ \env -> if ~(eval e1) env
684 eval (Lam x e) = <[ \env -> Fun (\v -> ~(eval e) ((x,v):env)) ]>
685 eval (App e1 e2) = <[ \env -> case ~(eval e1) env of
686 (Fun f) -> f (~(eval e2) env) ]>
687 eval (Var s) <[env]> = <[ fromJust (lookup s env) ]>
688 eval (Add e1 e2) <[env]> = <[ (~(eval e1) env) + (~(eval e2) env) ]>
696 immutable heap with cycles
698 -- an immutable heap; maps Int->(Int,Int)
700 alloc :: A (Int,Int) Int
701 lookup :: A Int (Int,Int)
703 onetwocycle :: A (Int,Int) (Int,Int)
712 alloc :: <[ (Int,Int) -> Int ]>
713 lookup :: <[ Int -> (Int,Int) ]>
715 onetwocycle :: <[ (Int,Int) ]> -> <[ (Int,Int) ]>
717 let x' = ~alloc (1,~y)
718 in let y' = ~alloc (2,~x)
722 onetwocycle' :: <[ (Int,Int) -> (Int,Int) ]>
723 onetwocycle' = back2 onetwocycle
731 The example may seem a little contrived, but its purpose is to
732 illustrate the be- haviour when the argument of mapC refers both to
733 its parameter and a free vari- able (n).
736 -- we can use mapA rather than mapC (from page 100)
738 mapA f = proc xs -> case xs of
739 [] -> returnA -< [] x:xs’ -> do y <- f -< x
740 ys’ <- mapA f -< xs’ returnA -< y:ys
744 ~(mapA <[ \x-> (~(delay 0) n, x) ]> )
749 ~(mapA <[ \x-> (~(delay 0) n, x) ]> ) xs ]>
762 (arr id *** (delaysA >>> delay []) >>>
765 nor :: SF (Bool,Bool) Bool
766 nor = arr (not.uncurry (||))
771 b <- delay False -< a
772 returnA -< a && not b
775 proc (reset,set) -> do
776 rec c <- delay False -< nor
777 reset d d <- delay True -< nor set c
780 halfAdd :: Arrow arr => arr (Bool,Bool) (Bool,Bool)
782 proc (x,y) -> returnA -< (x&&y, x/=y)
785 Arrow arr => arr (Bool,Bool,Bool) (Bool,Bool)
788 (c1,s1) <- halfAdd -< (x,y)
789 (c2,s2) <- halfAdd -< (s1,c)
790 returnA -< (c1||c2,s2)
792 Here is the appendix of Hughes04:
793 module Circuits where
794 import Control.Arrow import List
795 class ArrowLoop a => ArrowCircuit a where delay :: b -> a b b
796 nor :: Arrow a => a (Bool,Bool) Bool nor = arr (not.uncurry (||))
797 flipflop :: ArrowCircuit a => a (Bool,Bool) (Bool,Bool) flipflop = loop (arr (\((a,b),~(c,d)) -> ((a,d),(b,c))) >>>
798 nor *** nor >>> delay (False,True) >>> arr id &&& arr id)
799 class Signal a where showSignal :: [a] -> String
800 instance Signal Bool where showSignal bs = concat top++"\n"++concat bot++"\n"
801 where (top,bot) = unzip (zipWith sh (False:bs) bs) sh True True = ("__"," ") sh True False = (" ","|_") sh False True = (" _","| ")
802 sh False False = (" ","__")
803 instance (Signal a,Signal b) => Signal showSignal xys = showSignal (map fst showSignal (map snd
804 instance Signal a => Signal [a] where showSignal = concat . map showSignal
805 sig = concat . map (uncurry replicate)
806 (a,b) where xys) ++ xys)
808 flipflopInput = sig [(5,(False,False)),(2,(False,True)),(5,(False,False)),
809 (2,(True,False)),(5,(False,False)),(2,(True,True)), (6,(False,False))]
815 -- from Hughes' "programming with Arrows"
817 mapC :: ArrowChoice arr => arr (env,a) b -> arr (env,[a]) [b] mapC c = proc (env,xs) ->
818 case xs of [] -> returnA -< [] x:xs’ -> do y <- c -< (env,x)
819 ys <- mapC c -< (env,xs’) returnA -< y:ys
821 example2 = proc (n,xs) -> (| mapC (\x-> do delay 0 -< n
822 &&& do returnA -< x) |) xs