examples/tutorial.hs

   1 {-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -XFlexibleContexts -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs -XUndecidableInstances #-}
   2 module GArrowsTutorial
   3 where
   4 import Data.Bits
   5 import Data.Bool (not)
   6 import GHC.HetMet.CodeTypes hiding ((-))
   7 import GHC.HetMet.GArrow
   8 import Control.Category
   9 import Control.Arrow
  10 import Prelude hiding ( id, (.) )
  11
  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
  15 -- way!
  16
  17 -- Once you've built the modified compiler, you can compile this file
  18 -- with:
  19 --
  20 --    $ inplace/bin/ghc-stage2 tutorial.hs
  21 --
  22
  23 -- -XModalTypes adds a new syntactical expression, "code brackets":
  24 code_fst = <[ \(x,y) -> x ]>
  25
  26 -- This new expression is the introduction form for modal types:
  27 code_fst :: forall a b g. <[ (a,b) -> a ]>@g
  28
  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).
  35
  36 -- There is a second new expression form, "~~", called "escape":
  37
  38 code_fst_fst = <[ \z -> ~~code_fst (~~code_fst z) ]>
  39
  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:
  44
  45 example1    foo bar = <[ ~~$ foo bar  ]>
  46 example2    foo bar = <[ ~~( foo bar) ]>
  47 -- example3 foo bar = <[ ~~  foo bar  ]>
  48
  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)
  51
  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
  57 -- it had type "T".
  58
  59 -- So, the escape operator is basically a way of pasting code
  60 -- fragments into each other.
  61
  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
  65 -- tyvars:
  66
  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) ]>
  69
  70 -- Now, try commenting out the type ascription above and uncommenting
  71 -- any of these three:
  72 --
  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
  76 --
  77
  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
  82 -- in mayhem.
  83
  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:
  91
  92 -- badness = \x -> <[ x ]>
  93
  94 -- ...and in the following expression, the occurrence of "x" is bound
  95 -- by the first (outer) lambda, not the second one:
  96
  97 no_shadowing_here = \x -> <[ \x -> ~~x ]>
  98
  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!
 102
 103 foo       =    \x         -> x+1
 104 <[ foo ]> = <[ \(x::Bool) -> x   ]>
 105
 106 -- Now you can use foo (the second one!) inside code-brackets:
 107
 108 bar x = <[ foo ~~x ]>
 109
 110 bar :: forall g. <[Bool]>@g -> <[Bool]>@g
 111
 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 ]>
 116
 117 -- It has to be this way -- to see why, consider a term which is more
 118 -- polymorphic than "foo":
 119
 120 <[ foo' ]> = <[ \x -> x ]>
 121
 122 -- Its type is:
 123
 124 <[ foo' ]> :: forall a g . <[ a -> a ]>@g
 125
 126 -- ...and there's no way to express the g-polymorphism entirely from
 127 -- within the brackets.
 128
 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
 132
 133 increment_at_level1 = <[ \x -> x + 1 ]>
 134
 135 -- However, in unmodified haskell an identifier like (+) may have only
 136 -- one type.  In this case that type is:
 137 --
 138 --     (+) :: Num a => a -> a -> a
 139 --
 140 -- Now, we could simply decree that when (+) appears inside code
 141 -- brackets, an "implicit ~~" is inserted, so the desugared expression
 142 -- is:
 143 --
 144 --    increment_at_level1 = <[ \x -> ~~(+) x 1 ]>
 145 --
 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:
 150 --
 151 --    (+) :: Num a => (a,a) -> a
 152 --
 153 -- ... or even something less polymorphic, like
 154 --
 155 --    (+) :: (Int,Int) -> Int
 156 --
 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.
 161 --
 162 -- In hindsight, what we REALLY want is for increment_at_level1 to
 163 -- be desugared like this (much like the Arrow (|...|) syntax):
 164 --
 165 --   increment_at_level1 = <[ \x -> ~~( <[x]> + <[1]> ) ]>
 166 --
 167 -- ... because then we can declare
 168 --
 169 --   instance Num a => Num <[a]> where ...
 170 --
 171 -- or just
 172 --
 173 --   instance Num <[Int]> where ...
 174 --
 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.
 186 --
 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.
 189 --
 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.
 193 --
 194
 195
 196
 197
 198
 199
 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.
 203
 204
 205
 206
 207
 208
 209 --------------------------------------------------------------------------------
 210 -- Ye Olde and Most Venerable "pow" Function
 211
 212 pow :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer -> <[ Integer -> Integer ]>@c
 213 pow n =
 214    if n==0
 215    then <[ \x -> 1 ]>
 216    else <[ \x -> x * ~~(pow (n - 1)) x ]>
 217
 218
 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 ]>
 226
 227
 228
 229
 230
 231
 232
 233
 234
 235
 236 --------------------------------------------------------------------------------
 237 -- Dot Product
 238 --
 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.
 241 --
 242
 243 -- a one-level function to compute the dot product of two vectors
 244 dotproduct :: [Int] -> [Int] -> Int
 245 dotproduct v1 v2 =
 246   case v1 of
 247     []     -> 0
 248     (a:ax) -> case v2 of
 249                    []     -> 0
 250                    (b:bx) ->
 251                        (a*b)+(dotproduct ax bx)
 252
 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
 257 dotproduct' v1 v2 =
 258   case v1 of
 259     []     -> 0
 260     (0:ax) -> case v2 of
 261                    []     -> 0
 262                    (b:bx) -> (dotproduct' ax bx)
 263     (1:ax) -> case v2 of
 264                    []     -> 0
 265                    (b:bx) -> b+(dotproduct' ax bx)
 266     (a:ax) -> case v2 of
 267                    []     -> 0
 268                    (b:bx) ->
 269                        (a*b)+(dotproduct' ax bx)
 270
 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
 275 -- dot product.
 276
 277 dotproduct'' :: forall g.
 278                 GuestLanguageAdd         g Integer =>
 279                 GuestLanguageMult        g Integer =>
 280                 GuestIntegerLiteral      g         =>
 281                 [Integer] -> <[ [Integer] -> Integer ]>@g
 282 dotproduct'' v1 =
 283   case v1 of
 284     []     -> <[ \v2 -> 0 ]>
 285     (0:ax) -> <[ \v2 -> case v2 of
 286                           []     -> 0
 287                           (b:bx) -> ~~(dotproduct'' ax) bx ]>
 288     (1:ax) -> <[ \v2 -> case v2 of
 289                           []     -> 0
 290                           (b:bx) -> b + ~~(dotproduct'' ax) bx ]>
 291
 292     (a:ax) -> <[ \v2 -> case v2 of
 293                           []     -> 0
 294                           (b:bx) -> ~~(guestIntegerLiteral a) * b + ~~(dotproduct'' ax) bx ]>
 295
 296
 297
 298
 299 --------------------------------------------------------------------------------
 300 -- Taha-Sheard "isomorphism for code types"
 301
 302 back  :: forall a b c. (<[b]>@a -> <[c]>@a) -> <[ b->c ]>@a
 303 back  = \f -> <[ \x -> ~~(f <[x]>) ]>
 304
 305 forth :: forall a b c. <[b->c]>@a -> (<[b]>@a -> <[c]>@a)
 306 forth = \f -> \x -> <[ ~~f ~~x ]>
 307
 308
 309
 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.
 316
 317 run :: forall a. (forall b. <[a]>@b) -> a
 318 run = undefined
 319
 320 -- the typchecker correctly rejects this bogosity if you uncomment it:
 321 -- bogus = <[ \x -> ~~( run <[ x ]> ) ]>
 322
 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):
 329
 330 data ClosedCode a = ClosedCode (forall b. <[a]>@b)
 331
 332 open :: forall a b. ClosedCode a -> <[a]>@b
 333 open (ClosedCode x) = x
 334
 335 close :: (forall b. <[a]>@b) -> ClosedCode a
 336 close x = ClosedCode x
 337
 338 run_closed :: ClosedCode a -> a
 339 run_closed = undefined
 340
 341
 342
 343 --------------------------------------------------------------------------------
 344 -- A two-level Regular Expression matcher, adapted from Nanevski+Pfenning, Figure 6
 345 data Regex
 346  = Empty
 347  | Plus  Regex Regex
 348  | Times Regex Regex
 349  | Star  Regex
 350  | Const Char
 351
 352 class Stream a where
 353   s_empty :: a -> Bool
 354   s_head  :: a -> Char
 355   s_tail  :: a -> a
 356
 357 -- a continuation-passing-style matcher
 358
 359 accept :: Stream s => Regex -> (s -> Bool) -> s -> Bool
 360
 361 accept Empty k s          =
 362   k s
 363
 364 accept (Plus e1 e2) k s   =
 365  (accept e1 k s) || (accept e2 k s)
 366
 367 accept (Times e1 e2) k s  =
 368  (accept e1 (accept e2 k)) s
 369
 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
 374
 375 accept (Const c) k s      =
 376  if s_empty s
 377  then False
 378  else (s_head s) == c && k (s_tail s)
 379
 380 class GuestStream g a where
 381   <[ gs_empty ]> :: <[ a -> Bool ]>@g
 382   <[ gs_head  ]> :: <[ a -> Char ]>@g
 383   <[ gs_tail  ]> :: <[ a -> a    ]>@g
 384
 385 class GuestEqChar g where
 386   <[ (==) ]> :: <[ Char -> Char -> Bool ]>@g
 387 {-
 388 staged_accept ::
 389     Regex
 390     -> forall c s.
 391          GuestStream c s =>
 392          GuestCharLiteral c =>
 393          GuestLanguageBool c =>
 394          GuestEqChar c =>
 395          <[ s -> Bool ]>@c
 396       -> <[ s -> Bool ]>@c
 397
 398 staged_accept Empty k            =
 399    <[ \s -> gs_empty s ]>
 400
 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) ]>
 404
 405 staged_accept (Times e1 e2) k    =
 406    <[ \s -> ~~(staged_accept e1 (staged_accept e2 k)) s ]>
 407
 408 staged_accept (Star e) k         =
 409    loop
 410     where
 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
 416
 417
 418 staged_accept (Const c) k        =
 419     <[ \s -> if gs_empty s
 420              then false
 421              else (gs_head s) == ~~(guestCharLiteral c) && ~~k (gs_tail s) ]>
 422 -}
 423
 424 -- this type won't work unless the case for (Star e) is commented out;
 425 -- see loop above
 426 --      Regex
 427 --      -> (forall c s.
 428 --          GuestStream c s =>
 429 --          GuestLanguageBool c =>
 430 --          GuestEqChar c =>
 431 --          <[s -> Bool]>@c)
 432 --     -> (forall c s.
 433 --          GuestStream c s =>
 434 --          GuestLanguageBool c =>
 435 --          GuestEqChar c =>
 436 --          <[s -> Bool]>@c)
 437
 438
 439
 440
 441 --------------------------------------------------------------------------------
 442 -- Unflattening
 443
 444 {-
 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 }
 449
 450 instance Category Code where
 451   id             = Code <[ \x -> x ]>
 452   f . g          = Code <[ \x -> ~~(unCode f) (~~(unCode g) x) ]>
 453
 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 ]>
 458
 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) ]>
 464 -}
 465
 466
 467
 468 --------------------------------------------------------------------------------
 469 -- BiGArrows
 470
 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
 481
 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 }
 499 {-
 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 }
 502 -}
 503 -- but notice that we can't (in general) get
 504 -- instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...
 505
 506 {-
 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) }
 513
 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)) }
 517
 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))) ) }
 527
 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))) }
 534
 535
 536
 537 data Lens x y where
 538   Lens :: forall x y c1 c2 . ((x,c1)->(y,c2)) -> ((y,c2)->(x,c1)) -> Lens x y
 539
 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)))
 545
 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)),()))
 563
 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),()))
 570
 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
 574 -}
 575
 576
 577
 578 --------------------------------------------------------------------------------
 579 -- An example generalized arrow
 580
 581 --  *** this will be finished and posted by 14-Mar-2011; the code
 582 --  *** below is just a sketch ***
 583
 584 {-
 585 -- A verilog module is an SDoc (chunk of text) giving the module's
 586 -- definition.  The UniqueSupply avoids name clashes.
 587 data VerilogModule =
 588   VerilogModule
 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
 594
 595
 596 instance Show VerilogModule where
 597   show VerilogModule dep name body =
 598     "module "++name++"(FIXME)"++(body FIXME FIXME)
 599
 600 data VerilogWrappedType a =
 601   { vwt_rep :: String }
 602
 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 =
 607   UniqueSupply ->
 608   VerilogWrappedType a ->
 609   VerilogWrappedType b ->
 610   GArrowVerilog SDoc
 611
 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)
 621   ga_assoc     f   =
 622   ga_unassoc   :: g (x**(y**z)) ((x**y)**z)
 623
 624 instance GArrowDrop GArrowVerilog (,) where
 625   ga_drop      =
 626
 627 instance GArrowCopy GArrowVerilog (,) where
 628   ga_copy      =
 629
 630 instance GArrowSwap GArrowVerilog (,) where
 631   ga_swap      =
 632
 633 instance GArrowLoop GArrowVerilog (,) where
 634   ga_loop      =
 635
 636 instance GArrowLiteral GArrowVerilog (,) where
 637   ga_literal   =
 638 -}
 639
 640
 641
 642
 643
 644 {-
 645 lambda calculus interpreter
 646
 647 data Val =
 648   Num Int
 649 | Fun <[Val -> Val]>
 650
 651 This requires higher-order functions in the second level...
 652
 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)
 657                       in (Num (v1+v2)) ]>
 658 eval (If  e1 e2 e3) = <[ let v1 = ~(eval e1) in
 659                       in if v1
 660                          then ~(eval e2)
 661                          else ~(eval e3) ]>
 662 eval (Lam x  e)     = ???
 663
 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
 673                         else eval e3 -< 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 ->
 679                 f -< v
 680
 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
 684                                 then ~(eval e2) env
 685                                 else ~(eval e2) 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) ]>
 691 -}
 692
 693
 694
 695
 696
 697 {-
 698 immutable heap with cycles
 699
 700 -- an immutable heap; maps Int->(Int,Int)
 701
 702 alloc  :: A (Int,Int) Int
 703 lookup :: A Int       (Int,Int)
 704
 705 onetwocycle :: A (Int,Int) (Int,Int)
 706 onetwocycle =
 707   proc \(x,y)-> do
 708                  x' <- alloc -< (1,y)
 709                  y' <- alloc -< (2,x)
 710                  return (x',y')
 711 \end{verbatim}
 712
 713 \begin{verbatim}
 714 alloc  :: <[ (Int,Int) ->  Int      ]>
 715 lookup :: <[ Int       -> (Int,Int) ]>
 716
 717 onetwocycle :: <[ (Int,Int) ]> -> <[ (Int,Int) ]>
 718 onetwocycle x y = <[
 719   let    x' = ~alloc (1,~y)
 720   in let y' = ~alloc (2,~x)
 721   in (x',y')
 722 ]>
 723
 724 onetwocycle' :: <[ (Int,Int) -> (Int,Int) ]>
 725 onetwocycle' = back2 onetwocycle
 726 \end{verbatim}
 727 -}
 728
 729
 730
 731
 732 {-
 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).
 736
 737 \begin{verbatim}
 738 -- we can use mapA rather than mapC (from page 100)
 739
 740 mapA f = proc xs -> case xs of
 741 [] -> returnA -< [] x:xs’ -> do y <- f -< x
 742 ys’ <- mapA f -< xs’ returnA -< y:ys
 743
 744 example2 =
 745    <[ \(n,xs) ->
 746        ~(mapA <[ \x-> (~(delay 0) n, x) ]> )
 747         xs
 748     ]>
 749
 750 <[ example2 (n,xs) =
 751    ~(mapA <[ \x-> (~(delay 0) n, x) ]> ) xs ]>
 752 \end{verbatim}
 753 -}
 754
 755
 756
 757
 758
 759
 760 {-
 761 delaysA =
 762    arr listcase >>>
 763     arr (const []) |||
 764      (arr id *** (delaysA >>> delay []) >>>
 765        arr (uncurry (:)))
 766
 767 nor :: SF (Bool,Bool) Bool
 768 nor = arr (not.uncurry (||))
 769
 770 edge :: SF Bool Bool
 771 edge =
 772    proc a -> do
 773    b <- delay False -< a
 774    returnA -< a && not b
 775
 776 flipflop =
 777    proc (reset,set) -> do
 778    rec c <- delay False -< nor
 779    reset d d <- delay True -< nor set c
 780    returnA -< (c,d)
 781
 782 halfAdd :: Arrow arr => arr (Bool,Bool) (Bool,Bool)
 783 halfAdd =
 784    proc (x,y) -> returnA -< (x&&y, x/=y)
 785
 786 fullAdd ::
 787    Arrow arr => arr (Bool,Bool,Bool) (Bool,Bool)
 788 fullAdd =
 789    proc (x,y,c) -> do
 790    (c1,s1) <- halfAdd -< (x,y)
 791    (c2,s2) <- halfAdd -< (s1,c)
 792    returnA -< (c1||c2,s2)
 793
 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)
 809 . transpose
 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))]
 812
 813
 814
 815
 816
 817 -- from Hughes' "programming with Arrows"
 818
 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
 822
 823 example2 = proc (n,xs) -> (| mapC (\x-> do delay 0 -< n
 824 &&& do returnA -< x) |) xs
 825 -}
 826
 827
 828