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 --------------------------------------------------------------------------------
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 (**) u => BiGArrow g (**) u 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 (**) u => GArrowInversePair g (**) u x y =
484 GArrowInversePair { forward :: g x y , backward :: g y x }
485 instance GArrow g (**) u => Category (GArrowInversePair g (**) u) 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 (**) u => GArrow (GArrowInversePair g (**) u) (**) u 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 (**) u => GArrowSwap (GArrowInversePair g (**) u) (**) u where
498 ga_swap = GArrowInversePair { forward = ga_swap , backward = ga_swap }
500 instance (GArrowDrop g (**) u, GArrowCopy g (**) u) => GArrowCopy (GArrowInversePair g (**) u) (**) u where
501 ga_copy = GArrowInversePair { forward = ga_copy , backward = ga_second ga_drop >>> ga_cancelr }
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
578 --------------------------------------------------------------------------------
579 -- An example generalized arrow
581 -- *** this will be finished and posted by 14-Mar-2011; the code
582 -- *** below is just a sketch ***
585 -- A verilog module is an SDoc (chunk of text) giving the module's
586 -- definition. The UniqueSupply avoids name clashes.
589 [VerilogModule] -- dependencies
590 String -> -- module name
591 (Tree String -> -- input port names
592 Tree String -> -- output port names
593 SDoc) -- raw verilog code for the body
596 instance Show VerilogModule where
597 show VerilogModule dep name body =
598 "module "++name++"(FIXME)"++(body FIXME FIXME)
600 data VerilogWrappedType a =
601 { vwt_rep :: String }
603 -- A "verilog garrow" from A to B is, concretely, the source code for a
604 -- verilog module having input ports of type A and output ports of type B;
605 -- the UniqueSupply lets us generate names.
606 data GArrowVerilog a b =
608 VerilogWrappedType a ->
609 VerilogWrappedType b ->
612 instance GArrow GArrowVerilog (,) where
613 ga_id = VerilogModule [] "ga_id" (\ inp outp -> zipTree ... "assign "++outp++" = "++inp)
614 ga_comp f g = VerilogModule [] "ga_comp"
615 ga_first :: g x y -> g (x ** z) (y ** z)
616 ga_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
617 ga_cancell f = VerilogModule [] "ga_cancell" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in2)
618 ga_cancelr f = VerilogModule [] "ga_cancelr" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in1)
619 ga_uncancell f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out1++"=1'b0;\n assign"++out2++"="++in1)
620 ga_uncancelr f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out2++"=1'b0;\n assign"++out1++"="++in1)
622 ga_unassoc :: g (x**(y**z)) ((x**y)**z)
624 instance GArrowDrop GArrowVerilog (,) where
627 instance GArrowCopy GArrowVerilog (,) where
630 instance GArrowSwap GArrowVerilog (,) where
633 instance GArrowLoop GArrowVerilog (,) where
636 instance GArrowLiteral GArrowVerilog (,) where
645 lambda calculus interpreter
651 This requires higher-order functions in the second level...
653 eval :: Exp -> a Env Val
654 eval (Var s) = <[ lookup s ]>
655 eval (Add e1 e2) = <[ let (Num v1) = ~(eval e1)
656 in let (Num v2) = ~(eval e2)
658 eval (If e1 e2 e3) = <[ let v1 = ~(eval e1) in
664 eval (Var s) = proc env ->
665 returnA -< fromJust (lookup s env)
666 eval (Add e1 e2) = proc env ->
667 (eval e1 -< env) `bind` \ ~(Num u) ->
668 (eval e2 -< env) `bind` \ ~(Num v) ->
669 returnA -< Num (u + v)
670 eval (If e1 e2 e3) = proc env ->
671 (eval e1 -< env) `bind` \ ~(Bl b) ->
672 if b then eval e2 -< env
674 eval (Lam x e) = proc env ->
675 returnA -< Fun (proc v -> eval e -< (x,v):env)
676 eval (App e1 e2) = proc env ->
677 (eval e1 -< env) `bind` \ ~(Fun f) ->
678 (eval e2 -< env) `bind` \ v ->
681 eval (Var s) = <[ \env -> fromJust (lookup s env) ]>
682 eval (Add e1 e2) = <[ \env -> (~(eval e1) env) + (~(eval e2) env) ]>
683 eval (If e1 e2 e3) = <[ \env -> if ~(eval e1) env
686 eval (Lam x e) = <[ \env -> Fun (\v -> ~(eval e) ((x,v):env)) ]>
687 eval (App e1 e2) = <[ \env -> case ~(eval e1) env of
688 (Fun f) -> f (~(eval e2) env) ]>
689 eval (Var s) <[env]> = <[ fromJust (lookup s env) ]>
690 eval (Add e1 e2) <[env]> = <[ (~(eval e1) env) + (~(eval e2) env) ]>
698 immutable heap with cycles
700 -- an immutable heap; maps Int->(Int,Int)
702 alloc :: A (Int,Int) Int
703 lookup :: A Int (Int,Int)
705 onetwocycle :: A (Int,Int) (Int,Int)
714 alloc :: <[ (Int,Int) -> Int ]>
715 lookup :: <[ Int -> (Int,Int) ]>
717 onetwocycle :: <[ (Int,Int) ]> -> <[ (Int,Int) ]>
719 let x' = ~alloc (1,~y)
720 in let y' = ~alloc (2,~x)
724 onetwocycle' :: <[ (Int,Int) -> (Int,Int) ]>
725 onetwocycle' = back2 onetwocycle
733 The example may seem a little contrived, but its purpose is to
734 illustrate the be- haviour when the argument of mapC refers both to
735 its parameter and a free vari- able (n).
738 -- we can use mapA rather than mapC (from page 100)
740 mapA f = proc xs -> case xs of
741 [] -> returnA -< [] x:xs’ -> do y <- f -< x
742 ys’ <- mapA f -< xs’ returnA -< y:ys
746 ~(mapA <[ \x-> (~(delay 0) n, x) ]> )
751 ~(mapA <[ \x-> (~(delay 0) n, x) ]> ) xs ]>
764 (arr id *** (delaysA >>> delay []) >>>
767 nor :: SF (Bool,Bool) Bool
768 nor = arr (not.uncurry (||))
773 b <- delay False -< a
774 returnA -< a && not b
777 proc (reset,set) -> do
778 rec c <- delay False -< nor
779 reset d d <- delay True -< nor set c
782 halfAdd :: Arrow arr => arr (Bool,Bool) (Bool,Bool)
784 proc (x,y) -> returnA -< (x&&y, x/=y)
787 Arrow arr => arr (Bool,Bool,Bool) (Bool,Bool)
790 (c1,s1) <- halfAdd -< (x,y)
791 (c2,s2) <- halfAdd -< (s1,c)
792 returnA -< (c1||c2,s2)
794 Here is the appendix of Hughes04:
795 module Circuits where
796 import Control.Arrow import List
797 class ArrowLoop a => ArrowCircuit a where delay :: b -> a b b
798 nor :: Arrow a => a (Bool,Bool) Bool nor = arr (not.uncurry (||))
799 flipflop :: ArrowCircuit a => a (Bool,Bool) (Bool,Bool) flipflop = loop (arr (\((a,b),~(c,d)) -> ((a,d),(b,c))) >>>
800 nor *** nor >>> delay (False,True) >>> arr id &&& arr id)
801 class Signal a where showSignal :: [a] -> String
802 instance Signal Bool where showSignal bs = concat top++"\n"++concat bot++"\n"
803 where (top,bot) = unzip (zipWith sh (False:bs) bs) sh True True = ("__"," ") sh True False = (" ","|_") sh False True = (" _","| ")
804 sh False False = (" ","__")
805 instance (Signal a,Signal b) => Signal showSignal xys = showSignal (map fst showSignal (map snd
806 instance Signal a => Signal [a] where showSignal = concat . map showSignal
807 sig = concat . map (uncurry replicate)
808 (a,b) where xys) ++ xys)
810 flipflopInput = sig [(5,(False,False)),(2,(False,True)),(5,(False,False)),
811 (2,(True,False)),(5,(False,False)),(2,(True,True)), (6,(False,False))]
817 -- from Hughes' "programming with Arrows"
819 mapC :: ArrowChoice arr => arr (env,a) b -> arr (env,[a]) [b] mapC c = proc (env,xs) ->
820 case xs of [] -> returnA -< [] x:xs’ -> do y <- c -< (env,x)
821 ys <- mapC c -< (env,xs’) returnA -< y:ys
823 example2 = proc (n,xs) -> (| mapC (\x-> do delay 0 -< n
824 &&& do returnA -< x) |) xs