1 {-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -XFlexibleContexts -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs -XUndecidableInstances #-}
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 --------------------------------------------------------------------------------
444 -- The current implementation has problems with literals at level>0;
445 -- there are special-purpose hacks for Int and Char, but none for
446 -- unit. So I use this instead as a placeholder for <[ () ]>
448 <[ u ]> = Prelude.error "FIXME"
450 -- This more or less "undoes" the flatten function. People often ask
451 -- me how you "translate generalized arrows back into multi-level
452 -- terms".. I'm not sure why you'd want to do that, but this is how:
453 newtype Code x y = Code { unCode :: forall a. <[ x -> y ]>@a }
455 instance Category Code where
456 id = Code <[ \x -> x ]>
457 f . g = Code <[ \x -> ~~(unCode f) (~~(unCode g) x) ]>
459 instance GArrow Code (,) () where
460 ga_first f = Code <[ \(x,y) -> ((~~(unCode f) x),y) ]>
461 ga_second f = Code <[ \(x,y) -> (x ,(~~(unCode f) y)) ]>
462 ga_cancell = Code <[ \(_,x) -> x ]>
464 ga_cancelr = Code <[ \(x,_) -> x ]>
465 ga_uncancell = Code <[ \x -> (u,x) ]>
466 ga_uncancelr = Code <[ \x -> (x,u) ]>
467 ga_assoc = Code <[ \((x,y),z) -> (x,(y,z)) ]>
468 ga_unassoc = Code <[ \(x,(y,z)) -> ((x,y),z) ]>
472 --------------------------------------------------------------------------------
475 class GArrow g (**) u => BiGArrow g (**) u where
476 -- Note that we trust the user's pair of functions actually are
477 -- mutually inverse; confirming this in the type system would
478 -- require very powerful dependent types (such as Coq's). However,
479 -- the consequences of failure here are much more mild than failures
480 -- in BiArrow.inv: if the functions below are not mutually inverse,
481 -- the LoggingBiGArrow will simply compute the wrong result rather
482 -- than fail in some manner outside the language's semantics.
483 biga_arr :: (x -> y) -> (y -> x) -> g x y
484 biga_inv :: g x y -> g y x
486 -- For any GArrow instance, its mutually inverse pairs form a BiGArrow
487 data GArrow g (**) u => GArrowInversePair g (**) u x y =
488 GArrowInversePair { forward :: g x y , backward :: g y x }
489 instance GArrow g (**) u => Category (GArrowInversePair g (**) u) where
490 id = GArrowInversePair { forward = id , backward = id }
491 f . g = GArrowInversePair { forward = (forward f) . (forward g) , backward = (backward g) . (backward f) }
492 instance GArrow g (**) u => GArrow (GArrowInversePair g (**) u) (**) u where
493 ga_first f = GArrowInversePair { forward = ga_first (forward f), backward = ga_first (backward f) }
494 ga_second f = GArrowInversePair { forward = ga_second (forward f), backward = ga_second (backward f) }
495 ga_cancell = GArrowInversePair { forward = ga_cancell , backward = ga_uncancell }
496 ga_cancelr = GArrowInversePair { forward = ga_cancelr , backward = ga_uncancelr }
497 ga_uncancell = GArrowInversePair { forward = ga_uncancell , backward = ga_cancell }
498 ga_uncancelr = GArrowInversePair { forward = ga_uncancelr , backward = ga_cancelr }
499 ga_assoc = GArrowInversePair { forward = ga_assoc , backward = ga_unassoc }
500 ga_unassoc = GArrowInversePair { forward = ga_unassoc , backward = ga_assoc }
501 instance GArrowSwap g (**) u => GArrowSwap (GArrowInversePair g (**) u) (**) u where
502 ga_swap = GArrowInversePair { forward = ga_swap , backward = ga_swap }
503 -- but notice that we can't (in general) get
504 -- instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...
507 -- For that, we need PreLenses, which "log the history" where necessary.
508 -- I call this a "PreLens" because it consists of the data required
509 -- for a Lens (as in BCPierce's Lenses) but does not necessarily
510 -- satisfy the putget/getput laws. Specifically, the "extra stuff" we
511 -- store is the inversion function.
512 newtype PreLens x y = PreLens { preLens :: x -> (y , y->x) }
514 instance Category PreLens where
515 id = PreLens { preLens = \x -> (x, (\x -> x)) }
516 f . g = PreLens { preLens = \x -> let (gx,g') = (preLens g) x in let (fgx,f') = (preLens f) gx in (fgx , \q -> g' (f' q)) }
518 instance GArrow PreLens (,) () where
519 ga_first f = PreLens { preLens = \(x,z) -> let (y,f') = (preLens f) x in ((y,z),(\(q1,q2) -> (f' q1,q2))) }
520 ga_second f = PreLens { preLens = \(z,x) -> let (y,f') = (preLens f) x in ((z,y),(\(q1,q2) -> (q1,f' q2))) }
521 ga_cancell = PreLens { preLens = \(_,x) -> (x, (\x -> ((),x))) }
522 ga_cancelr = PreLens { preLens = \(x,_) -> (x, (\x -> (x,()))) }
523 ga_uncancell = PreLens { preLens = \x -> (((),x), (\(_,x) -> x)) }
524 ga_uncancelr = PreLens { preLens = \x -> ((x,()), (\(x,_) -> x)) }
525 ga_assoc = PreLens { preLens = \((x,y),z) -> ( (x,(y,z)) , (\(x,(y,z)) -> ((x,y),z)) ) }
526 ga_unassoc = PreLens { preLens = \(x,(y,z)) -> ( ((x,y),z) , (\((x,y),z) -> (x,(y,z))) ) }
528 instance GArrowDrop PreLens (,) () where
529 ga_drop = PreLens { preLens = \x -> (() , (\() -> x)) }
530 instance GArrowCopy PreLens (,) () where
531 ga_copy = PreLens { preLens = \x -> ((x,x) , fst) }
532 instance GArrowSwap PreLens (,) () where
533 ga_swap = PreLens { preLens = \(x,y) -> ((y,x) , (\(z,q) -> (q,z))) }
538 Lens :: forall x y c1 c2 . ((x,c1)->(y,c2)) -> ((y,c2)->(x,c1)) -> Lens x y
540 -- can we make lenses out of GArrows other than (->)?
541 instance Category Lens where
542 id = Lens (\x -> x) (\x -> x)
543 (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)))
544 (\(z,(c1,c2)) -> let (y,gc) = g2 (z,c2) in let (x,fc) = f2 (y,c1) in (x,(fc,gc)))
546 instance GArrow Lens (,) () where
547 ga_first (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x1,c) in ((y,x2),c'))
548 (\((x1,x2),c) -> let (y,c') = f2 (x1,c) in ((y,x2),c'))
549 ga_second (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x2,c) in ((x1,y),c'))
550 (\((x1,x2),c) -> let (y,c') = f2 (x2,c) in ((x1,y),c'))
551 ga_cancell = Lens (\(((),x),()) -> ( x ,()))
552 (\( x ,()) -> (((),x),()))
553 ga_uncancell = Lens (\( x ,()) -> (((),x),()))
554 (\(((),x),()) -> ( x ,()))
555 ga_cancelr = Lens (\((x,()),()) -> ( x ,()))
556 (\( x ,()) -> ((x,()),()))
557 ga_uncancelr = Lens (\( x ,()) -> ((x,()),()))
558 (\((x,()),()) -> ( x ,()))
559 ga_assoc = Lens (\(((x,y),z),()) -> ((x,(y,z)),()))
560 (\((x,(y,z)),()) -> (((x,y),z),()))
561 ga_unassoc = Lens (\((x,(y,z)),()) -> (((x,y),z),()))
562 (\(((x,y),z),()) -> ((x,(y,z)),()))
564 instance GArrowDrop Lens (,) () where
565 ga_drop = Lens (\(x,()) -> ((),x)) (\((),x) -> (x,()))
566 instance GArrowCopy Lens (,) () where
567 ga_copy = Lens (\(x,()) -> ((x,x),())) (\((x,_),()) -> (x,()))
568 instance GArrowSwap Lens (,) () where
569 ga_swap = Lens (\((x,y),()) -> ((y,x),())) (\((x,y),()) -> ((y,x),()))
571 instance BiGArrow Lens (,) () where
572 biga_arr f f' = Lens (\(x,()) -> ((f x),())) (\(x,()) -> ((f' x),()))
573 biga_inv (Lens f1 f2) = Lens f2 f1
577 --------------------------------------------------------------------------------
578 -- An example generalized arrow
580 -- *** this will be finished and posted by 14-Mar-2011; the code
581 -- *** below is just a sketch ***
584 -- A verilog module is an SDoc (chunk of text) giving the module's
585 -- definition. The UniqueSupply avoids name clashes.
588 [VerilogModule] -- dependencies
589 String -> -- module name
590 (Tree String -> -- input port names
591 Tree String -> -- output port names
592 SDoc) -- raw verilog code for the body
595 instance Show VerilogModule where
596 show VerilogModule dep name body =
597 "module "++name++"(FIXME)"++(body FIXME FIXME)
599 data VerilogWrappedType a =
600 { vwt_rep :: String }
602 -- A "verilog garrow" from A to B is, concretely, the source code for a
603 -- verilog module having input ports of type A and output ports of type B;
604 -- the UniqueSupply lets us generate names.
605 data GArrowVerilog a b =
607 VerilogWrappedType a ->
608 VerilogWrappedType b ->
611 instance GArrow GArrowVerilog (,) where
612 ga_id = VerilogModule [] "ga_id" (\ inp outp -> zipTree ... "assign "++outp++" = "++inp)
613 ga_comp f g = VerilogModule [] "ga_comp"
614 ga_first :: g x y -> g (x ** z) (y ** z)
615 ga_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
616 ga_cancell f = VerilogModule [] "ga_cancell" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in2)
617 ga_cancelr f = VerilogModule [] "ga_cancelr" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in1)
618 ga_uncancell f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out1++"=1'b0;\n assign"++out2++"="++in1)
619 ga_uncancelr f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out2++"=1'b0;\n assign"++out1++"="++in1)
621 ga_unassoc :: g (x**(y**z)) ((x**y)**z)
623 instance GArrowDrop GArrowVerilog (,) where
626 instance GArrowCopy GArrowVerilog (,) where
629 instance GArrowSwap GArrowVerilog (,) where
632 instance GArrowLoop GArrowVerilog (,) where
635 instance GArrowLiteral GArrowVerilog (,) where
644 lambda calculus interpreter
650 This requires higher-order functions in the second level...
652 eval :: Exp -> a Env Val
653 eval (Var s) = <[ lookup s ]>
654 eval (Add e1 e2) = <[ let (Num v1) = ~(eval e1)
655 in let (Num v2) = ~(eval e2)
657 eval (If e1 e2 e3) = <[ let v1 = ~(eval e1) in
663 eval (Var s) = proc env ->
664 returnA -< fromJust (lookup s env)
665 eval (Add e1 e2) = proc env ->
666 (eval e1 -< env) `bind` \ ~(Num u) ->
667 (eval e2 -< env) `bind` \ ~(Num v) ->
668 returnA -< Num (u + v)
669 eval (If e1 e2 e3) = proc env ->
670 (eval e1 -< env) `bind` \ ~(Bl b) ->
671 if b then eval e2 -< env
673 eval (Lam x e) = proc env ->
674 returnA -< Fun (proc v -> eval e -< (x,v):env)
675 eval (App e1 e2) = proc env ->
676 (eval e1 -< env) `bind` \ ~(Fun f) ->
677 (eval e2 -< env) `bind` \ v ->
680 eval (Var s) = <[ \env -> fromJust (lookup s env) ]>
681 eval (Add e1 e2) = <[ \env -> (~(eval e1) env) + (~(eval e2) env) ]>
682 eval (If e1 e2 e3) = <[ \env -> if ~(eval e1) env
685 eval (Lam x e) = <[ \env -> Fun (\v -> ~(eval e) ((x,v):env)) ]>
686 eval (App e1 e2) = <[ \env -> case ~(eval e1) env of
687 (Fun f) -> f (~(eval e2) env) ]>
688 eval (Var s) <[env]> = <[ fromJust (lookup s env) ]>
689 eval (Add e1 e2) <[env]> = <[ (~(eval e1) env) + (~(eval e2) env) ]>
697 immutable heap with cycles
699 -- an immutable heap; maps Int->(Int,Int)
701 alloc :: A (Int,Int) Int
702 lookup :: A Int (Int,Int)
704 onetwocycle :: A (Int,Int) (Int,Int)
713 alloc :: <[ (Int,Int) -> Int ]>
714 lookup :: <[ Int -> (Int,Int) ]>
716 onetwocycle :: <[ (Int,Int) ]> -> <[ (Int,Int) ]>
718 let x' = ~alloc (1,~y)
719 in let y' = ~alloc (2,~x)
723 onetwocycle' :: <[ (Int,Int) -> (Int,Int) ]>
724 onetwocycle' = back2 onetwocycle
732 The example may seem a little contrived, but its purpose is to
733 illustrate the be- haviour when the argument of mapC refers both to
734 its parameter and a free vari- able (n).
737 -- we can use mapA rather than mapC (from page 100)
739 mapA f = proc xs -> case xs of
740 [] -> returnA -< [] x:xs’ -> do y <- f -< x
741 ys’ <- mapA f -< xs’ returnA -< y:ys
745 ~(mapA <[ \x-> (~(delay 0) n, x) ]> )
750 ~(mapA <[ \x-> (~(delay 0) n, x) ]> ) xs ]>
763 (arr id *** (delaysA >>> delay []) >>>
766 nor :: SF (Bool,Bool) Bool
767 nor = arr (not.uncurry (||))
772 b <- delay False -< a
773 returnA -< a && not b
776 proc (reset,set) -> do
777 rec c <- delay False -< nor
778 reset d d <- delay True -< nor set c
781 halfAdd :: Arrow arr => arr (Bool,Bool) (Bool,Bool)
783 proc (x,y) -> returnA -< (x&&y, x/=y)
786 Arrow arr => arr (Bool,Bool,Bool) (Bool,Bool)
789 (c1,s1) <- halfAdd -< (x,y)
790 (c2,s2) <- halfAdd -< (s1,c)
791 returnA -< (c1||c2,s2)
793 Here is the appendix of Hughes04:
794 module Circuits where
795 import Control.Arrow import List
796 class ArrowLoop a => ArrowCircuit a where delay :: b -> a b b
797 nor :: Arrow a => a (Bool,Bool) Bool nor = arr (not.uncurry (||))
798 flipflop :: ArrowCircuit a => a (Bool,Bool) (Bool,Bool) flipflop = loop (arr (\((a,b),~(c,d)) -> ((a,d),(b,c))) >>>
799 nor *** nor >>> delay (False,True) >>> arr id &&& arr id)
800 class Signal a where showSignal :: [a] -> String
801 instance Signal Bool where showSignal bs = concat top++"\n"++concat bot++"\n"
802 where (top,bot) = unzip (zipWith sh (False:bs) bs) sh True True = ("__"," ") sh True False = (" ","|_") sh False True = (" _","| ")
803 sh False False = (" ","__")
804 instance (Signal a,Signal b) => Signal showSignal xys = showSignal (map fst showSignal (map snd
805 instance Signal a => Signal [a] where showSignal = concat . map showSignal
806 sig = concat . map (uncurry replicate)
807 (a,b) where xys) ++ xys)
809 flipflopInput = sig [(5,(False,False)),(2,(False,True)),(5,(False,False)),
810 (2,(True,False)),(5,(False,False)),(2,(True,True)), (6,(False,False))]
816 -- from Hughes' "programming with Arrows"
818 mapC :: ArrowChoice arr => arr (env,a) b -> arr (env,[a]) [b] mapC c = proc (env,xs) ->
819 case xs of [] -> returnA -< [] x:xs’ -> do y <- c -< (env,x)
820 ys <- mapC c -< (env,xs’) returnA -< y:ys
822 example2 = proc (n,xs) -> (| mapC (\x-> do delay 0 -< n
823 &&& do returnA -< x) |) xs