{-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -XFlexibleContexts -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs -XUndecidableInstances #-} module GArrowsTutorial where import Data.Bits import Data.Bool (not) import GHC.HetMet.CodeTypes hiding ((-)) import GHC.HetMet.GArrow import Control.Category import Control.Arrow import Prelude hiding ( id, (.) ) -- The best way to understand heterogeneous metaprogramming and -- generalized arrows is to play around with this file, poking at the -- examples until they fail to typecheck -- you'll learn a lot that -- way! -- Once you've built the modified compiler, you can compile this file -- with: -- -- $ inplace/bin/ghc-stage2 tutorial.hs -- -- -XModalTypes adds a new syntactical expression, "code brackets": code_fst = <[ \(x,y) -> x ]> -- This new expression is the introduction form for modal types: code_fst :: forall a b g. <[ (a,b) -> a ]>@g -- Think of <[T]>@g as being the type of programs written in language -- "g" which, when "executed", return a value of type "T". I mention -- "language g" because the *heterogeneous* aspect of HetMet means -- that we can limit the sorts of constructs allowed inside the code -- brackets, permitting only a subset of Haskell (you have to use -- Haskell syntax, though). -- There is a second new expression form, "~~", called "escape": code_fst_fst = <[ \z -> ~~code_fst (~~code_fst z) ]> -- Note that ~~ binds more tightly than any other operator. There is -- an alternate version, "~~$", which binds more weakly than any other -- operator (this is really handy sometimes!). To demonstrate this, -- the next two expressions differ only in superficial syntax: example1 foo bar = <[ ~~$ foo bar ]> example2 foo bar = <[ ~~( foo bar) ]> -- example3 foo bar = <[ ~~ foo bar ]> -- ... but the third one is completely different (and in fact, doesn't -- even parse, but we'll get to that in a moment) -- The escape operation must appear within code brackets. In truth, -- it is really a "hole" punched in the code brackets -- the thing to -- which the escape operator gets applied is typed as if it were -- *outside* the code brackets. It must have type <[T]>, and the -- escape operator allows it to be used *inside* code brackets as if -- it had type "T". -- So, the escape operator is basically a way of pasting code -- fragments into each other. -- This is where those type variables after the "@" sign come in: if -- you paste two pieces of code into a third, all three must be -- written in the same language. We express this by unifying their -- tyvars: compose_code :: forall g a b c. <[a->b]>@g -> <[b->c]>@g -> <[a->c]>@g compose_code x y = <[ \z -> ~~y (~~x z) ]> -- Now, try commenting out the type ascription above and uncommenting -- any of these three: -- -- compose_code :: forall g h a b c. <[a->b]>@h -> <[b->c]>@g -> <[a->c]>@g -- compose_code :: forall g h a b c. <[a->b]>@g -> <[b->c]>@h -> <[a->c]>@g -- compose_code :: forall g h a b c. <[a->b]>@g -> <[b->c]>@g -> <[a->c]>@h -- -- The typechecker won't let you get away with that -- you're trying -- to force a type which is "too polymorphic" onto paste2. If the -- compiler allowed that, the resulting metaprogram might try to -- splice together programs written in different languages, resulting -- in mayhem. -- NEW SCOPING RULES: The syntactical depth (or just "depth") of an -- expression is the number of surrounding code-brackets minus the -- number of surrounding escapes (this is strictly a syntax concept -- and has NOTHING to do with the type system!). It is very important -- to keep in mind that the scope of a bound variable extends only to -- expressions at the same depth! To demonstrate, the following -- expression will fail to parse: -- badness = \x -> <[ x ]> -- ...and in the following expression, the occurrence of "x" is bound -- by the first (outer) lambda, not the second one: no_shadowing_here = \x -> <[ \x -> ~~x ]> -- Lastly, you can wrap code-brackets around an identifier in a -- top-level, let, or where binding. Notice how GHC doesn't complain -- here about defining an identifier twice! foo = \x -> x+1 <[ foo ]> = <[ \(x::Bool) -> x ]> -- Now you can use foo (the second one!) inside code-brackets: bar x = <[ foo ~~x ]> bar :: forall g. <[Bool]>@g -> <[Bool]>@g -- In fact, the identifiers have completely unrelated types. Which -- brings up another important point: types are ALWAYS assigned -- "relative to" depth zero. So although we imagine "foo" existing at -- depth-one, its type is quite firmly established as <[ Bool -> Bool ]> -- It has to be this way -- to see why, consider a term which is more -- polymorphic than "foo": <[ foo' ]> = <[ \x -> x ]> -- Its type is: <[ foo' ]> :: forall a g . <[ a -> a ]>@g -- ...and there's no way to express the g-polymorphism entirely from -- within the brackets. -- So why does all of this matter? Mainly so that we can continue to use . We'd like -- the "+" operator to work "as expected" -- in other words, we'd like -- people to be able to write things like increment_at_level1 = <[ \x -> x + 1 ]> -- However, in unmodified haskell an identifier like (+) may have only -- one type. In this case that type is: -- -- (+) :: Num a => a -> a -> a -- -- Now, we could simply decree that when (+) appears inside code -- brackets, an "implicit ~~" is inserted, so the desugared expression -- is: -- -- increment_at_level1 = <[ \x -> ~~(+) x 1 ]> -- -- unfortunately this isn't going to work for guest languages that -- don't have higher-order functions. Haskell uses curried arguments -- because it has higher-order functions, but in a first-order guest -- language a more sensible type for (+) would be: -- -- (+) :: Num a => (a,a) -> a -- -- ... or even something less polymorphic, like -- -- (+) :: (Int,Int) -> Int -- -- so to maintain flexibility, we allow an identifier to have -- different types at different syntactic depths; this way type -- choices made for Haskell don't get imposed on guest languages that -- are missing some of its features. -- -- In hindsight, what we REALLY want is for increment_at_level1 to -- be desugared like this (much like the Arrow (|...|) syntax): -- -- increment_at_level1 = <[ \x -> ~~( <[x]> + <[1]> ) ]> -- -- ... because then we can declare -- -- instance Num a => Num <[a]> where ... -- -- or just -- -- instance Num <[Int]> where ... -- -- unfortunately there's a major problem: knowing how to do this sort -- of desugaring requires knowing the *arity* of a function. For -- symbols we can kludge it by checking Haskell's parsing rules (there -- are only a handful of unary symbols; all others are binary), but -- this is crude and won't work at all for non-symbol identifiers. -- And we can look at a type like x->y->z and say "oh, that's a -- two-argument function", but sometimes GHC doesn't know the complete -- type of an identifier in the midst of unification (i.e. "x has type -- Int->a for some a, where a could be Int or Int->Int"), so guessing -- the arity from the type cannot be done during parsing, which is -- when we need to do this. -- -- Okay, I think that's more or less a brain dump of why I changed the -- scoping rules and the problems with the other solutions I tried. -- -- I am very interested in hearing any suggestions on better ways of -- dealing with this, so long as you can still use operators like (+) -- in guest languages without higher-order functions. -- -- The rest of this file contains a bunch of example programs: -- exponentiation, dot-product, a bunch of classic MetaML idioms, and -- a translation of Nanevski+Pfenning's two-stage regex matcher. -------------------------------------------------------------------------------- -- Ye Olde and Most Venerable "pow" Function pow :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer -> <[ Integer -> Integer ]>@c pow n = if n==0 then <[ \x -> 1 ]> else <[ \x -> x * ~~(pow (n - 1)) x ]> -- a more efficient two-level pow pow' :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer -> <[ Integer -> Integer ]>@c pow' 0 = <[ \x -> 1 ]> pow' 1 = <[ \x -> x ]> pow' n = if n `mod` 2==0 then <[ \x -> (\y -> y*y) (~~(pow' $ n `shiftR` 2) x) ]> else <[ \x -> x * ~~(pow' $ n-1) x ]> -------------------------------------------------------------------------------- -- Dot Product -- -- This shows how to build a two-level program one step at a time by -- slowly rearranging it until the brackets can be inserted. -- -- a one-level function to compute the dot product of two vectors dotproduct :: [Int] -> [Int] -> Int dotproduct v1 v2 = case v1 of [] -> 0 (a:ax) -> case v2 of [] -> 0 (b:bx) -> (a*b)+(dotproduct ax bx) -- A slightly modified version of the dot product: note that we -- check for zeroes and ones to avoid multiplying. In a one-level -- program this yields no advantage, however! dotproduct' :: [Int] -> [Int] -> Int dotproduct' v1 v2 = case v1 of [] -> 0 (0:ax) -> case v2 of [] -> 0 (b:bx) -> (dotproduct' ax bx) (1:ax) -> case v2 of [] -> 0 (b:bx) -> b+(dotproduct' ax bx) (a:ax) -> case v2 of [] -> 0 (b:bx) -> (a*b)+(dotproduct' ax bx) -- A two-level version of the dot product. Note how we ask for the first -- vector, then produce a program which is optimized for multiplying -- by that particular vector. If there are zeroes or ones in the -- original vector, we will emit code which is faster than a one-level -- dot product. dotproduct'' :: forall g. GuestLanguageAdd g Integer => GuestLanguageMult g Integer => GuestIntegerLiteral g => [Integer] -> <[ [Integer] -> Integer ]>@g dotproduct'' v1 = case v1 of [] -> <[ \v2 -> 0 ]> (0:ax) -> <[ \v2 -> case v2 of [] -> 0 (b:bx) -> ~~(dotproduct'' ax) bx ]> (1:ax) -> <[ \v2 -> case v2 of [] -> 0 (b:bx) -> b + ~~(dotproduct'' ax) bx ]> (a:ax) -> <[ \v2 -> case v2 of [] -> 0 (b:bx) -> ~~(guestIntegerLiteral a) * b + ~~(dotproduct'' ax) bx ]> -------------------------------------------------------------------------------- -- Taha-Sheard "isomorphism for code types" back :: forall a b c. (<[b]>@a -> <[c]>@a) -> <[ b->c ]>@a back = \f -> <[ \x -> ~~(f <[x]>) ]> forth :: forall a b c. <[b->c]>@a -> (<[b]>@a -> <[c]>@a) forth = \f -> \x -> <[ ~~f ~~x ]> -------------------------------------------------------------------------------- -- Examples of "running" code; these examples illustrate the sorts of -- scoping problems that the Taha-Nielsen environment classifiers look -- for in the context of HOMOGENEOUS metaprogramming. You can't -- actually define these functions for ALL generalized arrows -- only -- those for which you've defined some sort of interpretation in Haskell. run :: forall a. (forall b. <[a]>@b) -> a run = undefined -- the typchecker correctly rejects this bogosity if you uncomment it: -- bogus = <[ \x -> ~~( run <[ x ]> ) ]> -- The Calcano-Moggi-Taha paper on environment classifier inference -- had a special type for closed code and two special expressions -- "close" and "open". These are unnecessary in SystemFC1 where we -- can use higher-rank polymorphism to get the same result (although -- in truth it's cheating a bit since their type inference is -- decidable with no annotations, whereas Rank-N inference is not): data ClosedCode a = ClosedCode (forall b. <[a]>@b) open :: forall a b. ClosedCode a -> <[a]>@b open (ClosedCode x) = x close :: (forall b. <[a]>@b) -> ClosedCode a close x = ClosedCode x run_closed :: ClosedCode a -> a run_closed = undefined -------------------------------------------------------------------------------- -- A two-level Regular Expression matcher, adapted from Nanevski+Pfenning, Figure 6 data Regex = Empty | Plus Regex Regex | Times Regex Regex | Star Regex | Const Char class Stream a where s_empty :: a -> Bool s_head :: a -> Char s_tail :: a -> a -- a continuation-passing-style matcher accept :: Stream s => Regex -> (s -> Bool) -> s -> Bool accept Empty k s = k s accept (Plus e1 e2) k s = (accept e1 k s) || (accept e2 k s) accept (Times e1 e2) k s = (accept e1 (accept e2 k)) s accept (Star e) k s = (k s) || (accept e (\s' -> accept (Star e) k s') s) -- FIXME: this will loop forever if you give it (Star x) where x can -- match the empty string accept (Const c) k s = if s_empty s then False else (s_head s) == c && k (s_tail s) class GuestStream g a where <[ gs_empty ]> :: <[ a -> Bool ]>@g <[ gs_head ]> :: <[ a -> Char ]>@g <[ gs_tail ]> :: <[ a -> a ]>@g class GuestEqChar g where <[ (==) ]> :: <[ Char -> Char -> Bool ]>@g staged_accept :: Regex -> forall c s. GuestStream c s => GuestCharLiteral c => GuestLanguageBool c => GuestEqChar c => <[ s -> Bool ]>@c -> <[ s -> Bool ]>@c staged_accept Empty k = <[ \s -> gs_empty s ]> -- note that code for "k" gets duplicated here staged_accept (Plus e1 e2) k = <[ \s -> (~~(staged_accept e1 k) s) || (~~(staged_accept e2 k) s) ]> staged_accept (Times e1 e2) k = <[ \s -> ~~(staged_accept e1 (staged_accept e2 k)) s ]> staged_accept (Star e) k = loop where -- loop :: <[s -> Bool]>@g loop = <[ \s -> ~~k s || ~~(staged_accept e loop) s ]> -- note that loop is not (forall c s. <[s -> Bool]>@c) -- because "k" is free in loop; it is analogous to the free -- environment variable in Nanevski's example staged_accept (Const c) k = <[ \s -> if gs_empty s then false else (gs_head s) == ~~(guestCharLiteral c) && ~~k (gs_tail s) ]> -- this type won't work unless the case for (Star e) is commented out; -- see loop above -- Regex -- -> (forall c s. -- GuestStream c s => -- GuestLanguageBool c => -- GuestEqChar c => -- <[s -> Bool]>@c) -- -> (forall c s. -- GuestStream c s => -- GuestLanguageBool c => -- GuestEqChar c => -- <[s -> Bool]>@c) -------------------------------------------------------------------------------- -- Unflattening -- The current implementation has problems with literals at level>0; -- there are special-purpose hacks for Int and Char, but none for -- unit. So I use this instead as a placeholder for <[ () ]> <[ u ]> = Prelude.error "FIXME" -- This more or less "undoes" the flatten function. People often ask -- me how you "translate generalized arrows back into multi-level -- terms".. I'm not sure why you'd want to do that, but this is how: newtype Code x y = Code { unCode :: forall a. <[ x -> y ]>@a } instance Category Code where id = Code <[ \x -> x ]> f . g = Code <[ \x -> ~~(unCode f) (~~(unCode g) x) ]> instance GArrow Code (,) () where ga_first f = Code <[ \(x,y) -> ((~~(unCode f) x),y) ]> ga_second f = Code <[ \(x,y) -> (x ,(~~(unCode f) y)) ]> ga_cancell = Code <[ \(_,x) -> x ]> ga_cancelr = Code <[ \(x,_) -> x ]> ga_uncancell = Code <[ \x -> (u,x) ]> ga_uncancelr = Code <[ \x -> (x,u) ]> ga_assoc = Code <[ \((x,y),z) -> (x,(y,z)) ]> ga_unassoc = Code <[ \(x,(y,z)) -> ((x,y),z) ]> -------------------------------------------------------------------------------- -- BiGArrows class GArrow g (**) u => BiGArrow g (**) u where -- Note that we trust the user's pair of functions actually are -- mutually inverse; confirming this in the type system would -- require very powerful dependent types (such as Coq's). However, -- the consequences of failure here are much more mild than failures -- in BiArrow.inv: if the functions below are not mutually inverse, -- the LoggingBiGArrow will simply compute the wrong result rather -- than fail in some manner outside the language's semantics. biga_arr :: (x -> y) -> (y -> x) -> g x y biga_inv :: g x y -> g y x -- For any GArrow instance, its mutually inverse pairs form a BiGArrow data GArrow g (**) u => GArrowInversePair g (**) u x y = GArrowInversePair { forward :: g x y , backward :: g y x } instance GArrow g (**) u => Category (GArrowInversePair g (**) u) where id = GArrowInversePair { forward = id , backward = id } f . g = GArrowInversePair { forward = (forward f) . (forward g) , backward = (backward g) . (backward f) } instance GArrow g (**) u => GArrow (GArrowInversePair g (**) u) (**) u where ga_first f = GArrowInversePair { forward = ga_first (forward f), backward = ga_first (backward f) } ga_second f = GArrowInversePair { forward = ga_second (forward f), backward = ga_second (backward f) } ga_cancell = GArrowInversePair { forward = ga_cancell , backward = ga_uncancell } ga_cancelr = GArrowInversePair { forward = ga_cancelr , backward = ga_uncancelr } ga_uncancell = GArrowInversePair { forward = ga_uncancell , backward = ga_cancell } ga_uncancelr = GArrowInversePair { forward = ga_uncancelr , backward = ga_cancelr } ga_assoc = GArrowInversePair { forward = ga_assoc , backward = ga_unassoc } ga_unassoc = GArrowInversePair { forward = ga_unassoc , backward = ga_assoc } instance GArrowSwap g (**) u => GArrowSwap (GArrowInversePair g (**) u) (**) u where ga_swap = GArrowInversePair { forward = ga_swap , backward = ga_swap } -- but notice that we can't (in general) get -- instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ... -- For that, we need PreLenses, which "log the history" where necessary. -- I call this a "PreLens" because it consists of the data required -- for a Lens (as in BCPierce's Lenses) but does not necessarily -- satisfy the putget/getput laws. Specifically, the "extra stuff" we -- store is the inversion function. newtype PreLens x y = PreLens { preLens :: x -> (y , y->x) } instance Category PreLens where id = PreLens { preLens = \x -> (x, (\x -> x)) } f . g = PreLens { preLens = \x -> let (gx,g') = (preLens g) x in let (fgx,f') = (preLens f) gx in (fgx , \q -> g' (f' q)) } instance GArrow PreLens (,) () where ga_first f = PreLens { preLens = \(x,z) -> let (y,f') = (preLens f) x in ((y,z),(\(q1,q2) -> (f' q1,q2))) } ga_second f = PreLens { preLens = \(z,x) -> let (y,f') = (preLens f) x in ((z,y),(\(q1,q2) -> (q1,f' q2))) } ga_cancell = PreLens { preLens = \(_,x) -> (x, (\x -> ((),x))) } ga_cancelr = PreLens { preLens = \(x,_) -> (x, (\x -> (x,()))) } ga_uncancell = PreLens { preLens = \x -> (((),x), (\(_,x) -> x)) } ga_uncancelr = PreLens { preLens = \x -> ((x,()), (\(x,_) -> x)) } ga_assoc = PreLens { preLens = \((x,y),z) -> ( (x,(y,z)) , (\(x,(y,z)) -> ((x,y),z)) ) } ga_unassoc = PreLens { preLens = \(x,(y,z)) -> ( ((x,y),z) , (\((x,y),z) -> (x,(y,z))) ) } instance GArrowDrop PreLens (,) () where ga_drop = PreLens { preLens = \x -> (() , (\() -> x)) } instance GArrowCopy PreLens (,) () where ga_copy = PreLens { preLens = \x -> ((x,x) , fst) } instance GArrowSwap PreLens (,) () where ga_swap = PreLens { preLens = \(x,y) -> ((y,x) , (\(z,q) -> (q,z))) } data Lens x y where Lens :: forall x y c1 c2 . ((x,c1)->(y,c2)) -> ((y,c2)->(x,c1)) -> Lens x y {- -- can we make lenses out of GArrows other than (->)? instance Category Lens where id = Lens (\x -> x) (\x -> x) (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))) (\(z,(c1,c2)) -> let (y,gc) = g2 (z,c2) in let (x,fc) = f2 (y,c1) in (x,(fc,gc))) instance GArrow Lens (,) () where ga_first (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x1,c) in ((y,x2),c')) (\((x1,x2),c) -> let (y,c') = f2 (x1,c) in ((y,x2),c')) ga_second (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x2,c) in ((x1,y),c')) (\((x1,x2),c) -> let (y,c') = f2 (x2,c) in ((x1,y),c')) ga_cancell = Lens (\(((),x),()) -> ( x ,())) (\( x ,()) -> (((),x),())) ga_uncancell = Lens (\( x ,()) -> (((),x),())) (\(((),x),()) -> ( x ,())) ga_cancelr = Lens (\((x,()),()) -> ( x ,())) (\( x ,()) -> ((x,()),())) ga_uncancelr = Lens (\( x ,()) -> ((x,()),())) (\((x,()),()) -> ( x ,())) ga_assoc = Lens (\(((x,y),z),()) -> ((x,(y,z)),())) (\((x,(y,z)),()) -> (((x,y),z),())) ga_unassoc = Lens (\((x,(y,z)),()) -> (((x,y),z),())) (\(((x,y),z),()) -> ((x,(y,z)),())) instance GArrowDrop Lens (,) () where ga_drop = Lens (\(x,()) -> ((),x)) (\((),x) -> (x,())) instance GArrowCopy Lens (,) () where ga_copy = Lens (\(x,()) -> ((x,x),())) (\((x,_),()) -> (x,())) instance GArrowSwap Lens (,) () where ga_swap = Lens (\((x,y),()) -> ((y,x),())) (\((x,y),()) -> ((y,x),())) instance BiGArrow Lens (,) () where biga_arr f f' = Lens (\(x,()) -> ((f x),())) (\(x,()) -> ((f' x),())) biga_inv (Lens f1 f2) = Lens f2 f1 -} -------------------------------------------------------------------------------- -- An example generalized arrow -- *** this will be finished and posted by 14-Mar-2011; the code -- *** below is just a sketch *** {- -- A verilog module is an SDoc (chunk of text) giving the module's -- definition. The UniqueSupply avoids name clashes. data VerilogModule = VerilogModule [VerilogModule] -- dependencies String -> -- module name (Tree String -> -- input port names Tree String -> -- output port names SDoc) -- raw verilog code for the body instance Show VerilogModule where show VerilogModule dep name body = "module "++name++"(FIXME)"++(body FIXME FIXME) data VerilogWrappedType a = { vwt_rep :: String } -- A "verilog garrow" from A to B is, concretely, the source code for a -- verilog module having input ports of type A and output ports of type B; -- the UniqueSupply lets us generate names. data GArrowVerilog a b = UniqueSupply -> VerilogWrappedType a -> VerilogWrappedType b -> GArrowVerilog SDoc instance GArrow GArrowVerilog (,) where ga_id = VerilogModule [] "ga_id" (\ inp outp -> zipTree ... "assign "++outp++" = "++inp) ga_comp f g = VerilogModule [] "ga_comp" ga_first :: g x y -> g (x ** z) (y ** z) ga_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap ga_cancell f = VerilogModule [] "ga_cancell" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in2) ga_cancelr f = VerilogModule [] "ga_cancelr" (\ [in1,in2] [outp] -> "assign "++outp++" = "++in1) ga_uncancell f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out1++"=1'b0;\n assign"++out2++"="++in1) ga_uncancelr f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] -> "assign "++out2++"=1'b0;\n assign"++out1++"="++in1) ga_assoc f = ga_unassoc :: g (x**(y**z)) ((x**y)**z) instance GArrowDrop GArrowVerilog (,) where ga_drop = instance GArrowCopy GArrowVerilog (,) where ga_copy = instance GArrowSwap GArrowVerilog (,) where ga_swap = instance GArrowLoop GArrowVerilog (,) where ga_loop = instance GArrowLiteral GArrowVerilog (,) where ga_literal = -} {- lambda calculus interpreter data Val = Num Int | Fun <[Val -> Val]> This requires higher-order functions in the second level... eval :: Exp -> a Env Val eval (Var s) = <[ lookup s ]> eval (Add e1 e2) = <[ let (Num v1) = ~(eval e1) in let (Num v2) = ~(eval e2) in (Num (v1+v2)) ]> eval (If e1 e2 e3) = <[ let v1 = ~(eval e1) in in if v1 then ~(eval e2) else ~(eval e3) ]> eval (Lam x e) = ??? eval (Var s) = proc env -> returnA -< fromJust (lookup s env) eval (Add e1 e2) = proc env -> (eval e1 -< env) `bind` \ ~(Num u) -> (eval e2 -< env) `bind` \ ~(Num v) -> returnA -< Num (u + v) eval (If e1 e2 e3) = proc env -> (eval e1 -< env) `bind` \ ~(Bl b) -> if b then eval e2 -< env else eval e3 -< env eval (Lam x e) = proc env -> returnA -< Fun (proc v -> eval e -< (x,v):env) eval (App e1 e2) = proc env -> (eval e1 -< env) `bind` \ ~(Fun f) -> (eval e2 -< env) `bind` \ v -> f -< v eval (Var s) = <[ \env -> fromJust (lookup s env) ]> eval (Add e1 e2) = <[ \env -> (~(eval e1) env) + (~(eval e2) env) ]> eval (If e1 e2 e3) = <[ \env -> if ~(eval e1) env then ~(eval e2) env else ~(eval e2) env eval (Lam x e) = <[ \env -> Fun (\v -> ~(eval e) ((x,v):env)) ]> eval (App e1 e2) = <[ \env -> case ~(eval e1) env of (Fun f) -> f (~(eval e2) env) ]> eval (Var s) <[env]> = <[ fromJust (lookup s env) ]> eval (Add e1 e2) <[env]> = <[ (~(eval e1) env) + (~(eval e2) env) ]> -} {- immutable heap with cycles -- an immutable heap; maps Int->(Int,Int) alloc :: A (Int,Int) Int lookup :: A Int (Int,Int) onetwocycle :: A (Int,Int) (Int,Int) onetwocycle = proc \(x,y)-> do x' <- alloc -< (1,y) y' <- alloc -< (2,x) return (x',y') \end{verbatim} \begin{verbatim} alloc :: <[ (Int,Int) -> Int ]> lookup :: <[ Int -> (Int,Int) ]> onetwocycle :: <[ (Int,Int) ]> -> <[ (Int,Int) ]> onetwocycle x y = <[ let x' = ~alloc (1,~y) in let y' = ~alloc (2,~x) in (x',y') ]> onetwocycle' :: <[ (Int,Int) -> (Int,Int) ]> onetwocycle' = back2 onetwocycle \end{verbatim} -} {- The example may seem a little contrived, but its purpose is to illustrate the be- haviour when the argument of mapC refers both to its parameter and a free vari- able (n). \begin{verbatim} -- we can use mapA rather than mapC (from page 100) mapA f = proc xs -> case xs of [] -> returnA -< [] x:xs’ -> do y <- f -< x ys’ <- mapA f -< xs’ returnA -< y:ys example2 = <[ \(n,xs) -> ~(mapA <[ \x-> (~(delay 0) n, x) ]> ) xs ]> <[ example2 (n,xs) = ~(mapA <[ \x-> (~(delay 0) n, x) ]> ) xs ]> \end{verbatim} -} {- delaysA = arr listcase >>> arr (const []) ||| (arr id *** (delaysA >>> delay []) >>> arr (uncurry (:))) nor :: SF (Bool,Bool) Bool nor = arr (not.uncurry (||)) edge :: SF Bool Bool edge = proc a -> do b <- delay False -< a returnA -< a && not b flipflop = proc (reset,set) -> do rec c <- delay False -< nor reset d d <- delay True -< nor set c returnA -< (c,d) halfAdd :: Arrow arr => arr (Bool,Bool) (Bool,Bool) halfAdd = proc (x,y) -> returnA -< (x&&y, x/=y) fullAdd :: Arrow arr => arr (Bool,Bool,Bool) (Bool,Bool) fullAdd = proc (x,y,c) -> do (c1,s1) <- halfAdd -< (x,y) (c2,s2) <- halfAdd -< (s1,c) returnA -< (c1||c2,s2) Here is the appendix of Hughes04: module Circuits where import Control.Arrow import List class ArrowLoop a => ArrowCircuit a where delay :: b -> a b b nor :: Arrow a => a (Bool,Bool) Bool nor = arr (not.uncurry (||)) flipflop :: ArrowCircuit a => a (Bool,Bool) (Bool,Bool) flipflop = loop (arr (\((a,b),~(c,d)) -> ((a,d),(b,c))) >>> nor *** nor >>> delay (False,True) >>> arr id &&& arr id) class Signal a where showSignal :: [a] -> String instance Signal Bool where showSignal bs = concat top++"\n"++concat bot++"\n" where (top,bot) = unzip (zipWith sh (False:bs) bs) sh True True = ("__"," ") sh True False = (" ","|_") sh False True = (" _","| ") sh False False = (" ","__") instance (Signal a,Signal b) => Signal showSignal xys = showSignal (map fst showSignal (map snd instance Signal a => Signal [a] where showSignal = concat . map showSignal sig = concat . map (uncurry replicate) (a,b) where xys) ++ xys) . transpose flipflopInput = sig [(5,(False,False)),(2,(False,True)),(5,(False,False)), (2,(True,False)),(5,(False,False)),(2,(True,True)), (6,(False,False))] -- from Hughes' "programming with Arrows" mapC :: ArrowChoice arr => arr (env,a) b -> arr (env,[a]) [b] mapC c = proc (env,xs) -> case xs of [] -> returnA -< [] x:xs’ -> do y <- c -< (env,x) ys <- mapC c -< (env,xs’) returnA -< y:ys example2 = proc (n,xs) -> (| mapC (\x-> do delay 0 -< n &&& do returnA -< x) |) xs -}