examples/tutorial.hs

   1 {-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -XFlexibleContexts -XMultiParamTypeClasses -ddump-types #-}
   2 module GArrowsTutorial
   3 where
   4 import Data.Bits
   5 import GHC.HetMet.CodeTypes hiding ((-))
   6 import Prelude (undefined, ($), (==), fromInteger, Bool(..), Int, (-), negate, mod, (*), (+), Char, (||), (&&))
   7
   8 -- The best way to understand heterogeneous metaprogramming and
   9 -- generalized arrows is to play around with this file, poking at the
  10 -- examples until they fail to typecheck -- you'll learn a lot that
  11 -- way!
  12
  13 -- Once you've built the modified compiler, you can compile this file
  14 -- with:
  15 --
  16 --    $ inplace/bin/ghc-stage2 tutorial.hs
  17 --
  18
  19 -- -XModalTypes adds a new syntactical expression, "code brackets":
  20 code_fst = <[ \(x,y) -> x ]>
  21
  22 -- This new expression is the introduction form for modal types:
  23 code_fst :: forall a b g. <[ (a,b) -> a ]>@g
  24
  25 -- Think of <[T]>@g as being the type of programs written in language
  26 -- "g" which, when "executed", return a value of type "T".  I mention
  27 -- "language g" because the *heterogeneous* aspect of HetMet means
  28 -- that we can limit the sorts of constructs allowed inside the code
  29 -- brackets, permitting only a subset of Haskell (you have to use
  30 -- Haskell syntax, though).
  31
  32 -- There is a second new expression form, "~~", called "escape":
  33
  34 code_fst_fst = <[ \z -> ~~code_fst (~~code_fst z) ]>
  35
  36 -- Note that ~~ binds more tightly than any other operator.  There is
  37 -- an alternate version, "~~$", which binds more weakly than any other
  38 -- operator (this is really handy sometimes!).  To demonstrate this,
  39 -- the next two expressions differ only in superficial syntax:
  40
  41 example1    foo bar = <[ ~~$ foo bar  ]>
  42 example2    foo bar = <[ ~~( foo bar) ]>
  43 -- example3 foo bar = <[ ~~  foo bar  ]>
  44
  45 -- ... but the third one is completely different (and in fact, doesn't
  46 -- even parse, but we'll get to that in a moment)
  47
  48 -- The escape operation must appear within code brackets.  In truth,
  49 -- it is really a "hole" punched in the code brackets -- the thing to
  50 -- which the escape operator gets applied is typed as if it were
  51 -- *outside* the code brackets.  It must have type <[T]>, and the
  52 -- escape operator allows it to be used *inside* code brackets as if
  53 -- it had type "T".
  54
  55 -- So, the escape operator is basically a way of pasting code
  56 -- fragments into each other.
  57
  58 -- This is where those type variables after the "@" sign come in: if
  59 -- you paste two pieces of code into a third, all three must be
  60 -- written in the same language.  We express this by unifying their
  61 -- tyvars:
  62
  63 compose_code :: forall g a b c. <[a->b]>@g -> <[b->c]>@g -> <[a->c]>@g
  64 compose_code x y = <[ \z -> ~~y (~~x z) ]>
  65
  66 -- Now, try commenting out the type ascription above and uncommenting
  67 -- any of these three:
  68 --
  69 -- compose_code :: forall g h a b c. <[a->b]>@h -> <[b->c]>@g -> <[a->c]>@g
  70 -- compose_code :: forall g h a b c. <[a->b]>@g -> <[b->c]>@h -> <[a->c]>@g
  71 -- compose_code :: forall g h a b c. <[a->b]>@g -> <[b->c]>@g -> <[a->c]>@h
  72 --
  73
  74 -- The typechecker won't let you get away with that -- you're trying
  75 -- to force a type which is "too polymorphic" onto paste2.  If the
  76 -- compiler allowed that, the resulting metaprogram might try to
  77 -- splice together programs written in different languages, resulting
  78 -- in mayhem.
  79
  80 -- NEW SCOPING RULES: The syntactical depth (or just "depth") of an
  81 -- expression is the number of surrounding code-brackets minus the
  82 -- number of surrounding escapes (this is strictly a syntax concept
  83 -- and has NOTHING to do with the type system!).  It is very important
  84 -- to keep in mind that the scope of a bound variable extends only to
  85 -- expressions at the same depth!  To demonstrate, the following
  86 -- expression will fail to parse:
  87
  88 -- badness = \x -> <[ x ]>
  89
  90 -- ...and in the following expression, the occurrence of "x" is bound
  91 -- by the first (outer) lambda, not the second one:
  92
  93 no_shadowing_here = \x -> <[ \x -> ~~x ]>
  94
  95 -- the rest of this file contains a bunch of example programs:
  96 -- exponentiation, dot-product, a bunch of classic MetaML idioms, and
  97 -- a translation of Nanevski+Pfenning's two-stage regex matcher.
  98
  99
 100
 101
 102
 103
 104 --------------------------------------------------------------------------------
 105 -- Ye Olde and Most Venerable "pow" Function
 106
 107 pow n =
 108    if n==0
 109    then <[ \x -> 1 ]>
 110    else <[ \x -> x * ~~(pow (n - 1)) x ]>
 111
 112
 113 -- a more efficient two-level pow
 114 pow' 0  = <[ \x -> 1 ]>
 115 pow' 1  = <[ \x -> x ]>
 116 pow' n  = if   n `mod` 2==0
 117           then <[ \x -> (\y -> y*y) (~~(pow' $ n `shiftR` 2) x) ]>
 118           else <[ \x -> x * ~~(pow' $ n-1) x ]>
 119
 120
 121
 122
 123
 124
 125
 126
 127
 128
 129
 130 --------------------------------------------------------------------------------
 131 -- Dot Product
 132 --
 133 --  This shows how to build a two-level program one step at a time by
 134 --  slowly rearranging it until the brackets can be inserted.
 135 --
 136
 137 -- a one-level function to compute the dot product of two vectors
 138 dotproduct :: [Int] -> [Int] -> Int
 139 dotproduct v1 v2 =
 140   case v1 of
 141     []     -> 0
 142     (a:ax) -> case v2 of
 143                    []     -> 0
 144                    (b:bx) ->
 145                        (a*b)+(dotproduct ax bx)
 146
 147 -- A slightly modified version of the dot product: note that we
 148 -- check for zeroes and ones to avoid multiplying.  In a one-level
 149 -- program this yields no advantage, however!
 150 dotproduct' :: [Int] -> [Int] -> Int
 151 dotproduct' v1 v2 =
 152   case v1 of
 153     []     -> 0
 154     (0:ax) -> case v2 of
 155                    []     -> 0
 156                    (b:bx) -> (dotproduct' ax bx)
 157     (1:ax) -> case v2 of
 158                    []     -> 0
 159                    (b:bx) -> b+(dotproduct' ax bx)
 160     (a:ax) -> case v2 of
 161                    []     -> 0
 162                    (b:bx) ->
 163                        (a*b)+(dotproduct' ax bx)
 164
 165 -- A two-level version of the dot product.  Note how we ask for the first
 166 -- vector, then produce a program which is optimized for multiplying
 167 -- by that particular vector.  If there are zeroes or ones in the
 168 -- original vector, we will emit code which is faster than a one-level
 169 -- dot product.
 170 dotproduct'' :: forall g.
 171                 GuestLanguageAdd         g Int =>
 172                 GuestLanguageMult        g Int =>
 173                 GuestLanguageFromInteger g Int =>
 174                 [Int] -> <[ [Int] -> Int ]>@g
 175 dotproduct'' v1 =
 176   case v1 of
 177     []     -> <[ \v2 -> 0 ]>
 178     (0:ax) -> <[ \v2 -> case v2 of
 179                           []     -> 0
 180                           (b:bx) -> ~~(dotproduct'' ax) bx ]>
 181     (1:ax) -> <[ \v2 -> case v2 of
 182                           []     -> 0
 183                           (b:bx) -> b + ~~(dotproduct'' ax) bx ]>
 184     (a:ax) -> <[ \v2 -> case v2 of
 185                           []     -> 0
 186                           (b:bx) -> %%a * b + ~~(dotproduct'' ax) bx ]>
 187
 188
 189
 190
 191
 192
 193 --------------------------------------------------------------------------------
 194 -- Taha-Sheard "isomorphism for code types"
 195
 196 back  :: forall a b c. (<[b]>@a -> <[c]>@a) -> <[ b->c ]>@a
 197 back  = \f -> <[ \x -> ~~(f <[x]>) ]>
 198
 199 forth :: forall a b c. <[b->c]>@a -> (<[b]>@a -> <[c]>@a)
 200 forth = \f -> \x -> <[ ~~f ~~x ]>
 201
 202
 203
 204 --------------------------------------------------------------------------------
 205 -- Examples of "running" code; these examples illustrate the sorts of
 206 -- scoping problems that the Taha-Nielsen environment classifiers look
 207 -- for in the context of HOMOGENEOUS metaprogramming.  You can't
 208 -- actually define these functions for ALL generalized arrows -- only
 209 -- those for which you've defined some sort of interpretation in Haskell.
 210
 211 run :: forall a. (forall b. <[a]>@b) -> a
 212 run = undefined
 213
 214 -- the typchecker correctly rejects this bogosity if you uncomment it:
 215 -- bogus = <[ \x -> ~~( run <[ x ]> ) ]>
 216
 217 -- The Calcano-Moggi-Taha paper on environment classifier inference
 218 -- had a special type for closed code and two special expressions
 219 -- "close" and "open".  These are unnecessary in SystemFC1 where we
 220 -- can use higher-rank polymorphism to get the same result (although
 221 -- in truth it's cheating a bit since their type inference is
 222 -- decidable with no annotations, whereas Rank-N inference is not):
 223
 224 data ClosedCode a = ClosedCode (forall b. <[a]>@b)
 225
 226 open :: forall a b. ClosedCode a -> <[a]>@b
 227 open (ClosedCode x) = x
 228
 229 close :: (forall b. <[a]>@b) -> ClosedCode a
 230 close x = ClosedCode x
 231
 232 run_closed :: ClosedCode a -> a
 233 run_closed = undefined
 234
 235
 236
 237
 238 --------------------------------------------------------------------------------
 239 -- A two-level Regular Expression matcher, adapted from Nanevski+Pfenning, Figure 6
 240 data Regex
 241  = Empty
 242  | Plus  Regex Regex
 243  | Times Regex Regex
 244  | Star  Regex
 245  | Const Char
 246
 247 class Stream a where
 248   s_empty :: a -> Bool
 249   s_head  :: a -> Char
 250   s_tail  :: a -> a
 251
 252 -- a continuation-passing-style matcher
 253
 254 accept :: Stream s => Regex -> (s -> Bool) -> s -> Bool
 255
 256 accept Empty k s          =
 257   k s
 258
 259 accept (Plus e1 e2) k s   =
 260  (accept e1 k s) || (accept e2 k s)
 261
 262 accept (Times e1 e2) k s  =
 263  (accept e1 (accept e2 k)) s
 264
 265 accept (Star e) k s       =
 266  (k s) || (accept e (\s' -> accept (Star e) k s') s)
 267  -- FIXME: this will loop forever if you give it (Star x) where x can
 268  -- match the empty string
 269
 270 accept (Const c) k s      =
 271  if s_empty s
 272  then False
 273  else (s_head s) == c && k (s_tail s)
 274
 275 class GuestStream g a where
 276   <[ gs_empty ]> :: <[ a -> Bool ]>@g
 277   <[ gs_head  ]> :: <[ a -> Char ]>@g
 278   <[ gs_tail  ]> :: <[ a -> a    ]>@g
 279
 280 class GuestEqChar g where
 281   <[ (==) ]> :: <[ Char -> Char -> Bool ]>@g
 282
 283 staged_accept ::
 284     Regex
 285     -> forall c s.
 286          GuestStream c s =>
 287          GuestLanguageBool c =>
 288          GuestEqChar c =>
 289          <[ s -> Bool ]>@c
 290       -> <[ s -> Bool ]>@c
 291
 292 staged_accept Empty k            =
 293    <[ \s -> gs_empty s ]>
 294
 295 -- note that code for "k" gets duplicated here
 296 staged_accept (Plus e1 e2) k     =
 297    <[ \s -> (~~(staged_accept e1 k) s) || (~~(staged_accept e2 k) s) ]>
 298
 299 staged_accept (Times e1 e2) k    =
 300    <[ \s -> ~~(staged_accept e1 (staged_accept e2 k)) s ]>
 301
 302 staged_accept (Star e) k         =
 303    loop
 304     where
 305     -- loop :: <[s -> Bool]>@g
 306      loop =  <[ \s -> ~~k s || ~~(staged_accept e loop) s ]>
 307     -- note that loop is not (forall c s. <[s -> Bool]>@c)
 308     -- because "k" is free in loop; it is analogous to the free
 309     -- environment variable in Nanevski's example
 310
 311 staged_accept (Const c) k        =
 312     <[ \s -> if gs_empty s
 313              then false
 314              else (gs_head s) == %%c && ~~k (gs_tail s) ]>
 315 {-
 316  this type won't work unless the case for (Star e) is commented out;
 317  see loop above
 318       Regex
 319       -> (forall c s.
 320           GuestStream c s =>
 321           GuestLanguageBool c =>
 322           GuestEqChar c =>
 323           []_c (s -> Bool))
 324      -> (forall c s.
 325           GuestStream c s =>
 326           GuestLanguageBool c =>
 327           GuestEqChar c =>
 328           []_c (s -> Bool))
 329 -}
 330
 331
 332
 333 --------------------------------------------------------------------------------
 334 -- An example generalized arrow
 335
 336 --  *** this will be finished and posted by 14-Mar-2011; the code
 337 --  *** below is just a sketch ***
 338
 339 {-
 340 -- A verilog module is an SDoc (chunk of text) giving the module's
 341 -- definition.  The UniqueSupply avoids name clashes.
 342 data VerilogModule =
 343   VerilogModule
 344     [VerilogModule]     -- dependencies
 345     String ->           -- module name
 346     (Tree String ->        -- input port names
 347      Tree String ->        -- output port names
 348      SDoc)              -- raw verilog code for the body
 349
 350
 351 instance Show VerilogModule where
 352   show VerilogModule dep name body =
 353     "module "++name++"(FIXME)"++(body FIXME FIXME)
 354
 355 data VerilogWrappedType a =
 356   { vwt_rep :: String }
 357
 358 -- A "verilog garrow" from A to B is, concretely, the source code for a
 359 -- verilog module having input ports of type A and output ports of type B;
 360 -- the UniqueSupply lets us generate names.
 361 data GArrowVerilog a b =
 362   UniqueSupply ->
 363   VerilogWrappedType a ->
 364   VerilogWrappedType b ->
 365   GArrowVerilog SDoc
 366
 367 instance GArrow GArrowVerilog (,) where
 368   ga_id            =  VerilogModule [] "ga_id"   (\ inp outp -> zipTree ... "assign "++outp++" = "++inp)
 369   ga_comp      f g =  VerilogModule [] "ga_comp"
 370   ga_first     :: g x y -> g (x ** z) (y ** z)
 371   ga_second    f   =  ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
 372   ga_cancell   f   =  VerilogModule [] "ga_cancell" (\ [in1,in2] [outp]      -> "assign "++outp++" = "++in2)
 373   ga_cancelr   f   =  VerilogModule [] "ga_cancelr" (\ [in1,in2] [outp]      -> "assign "++outp++" = "++in1)
 374   ga_uncancell f   =  VerilogModule [] "ga_cancelr" (\ [in1]     [out1,out2] -> "assign "++out1++"=1'b0;\n assign"++out2++"="++in1)
 375   ga_uncancelr f   =  VerilogModule [] "ga_cancelr" (\ [in1]     [out1,out2] -> "assign "++out2++"=1'b0;\n assign"++out1++"="++in1)
 376   ga_assoc     f   =
 377   ga_unassoc   :: g (x**(y**z)) ((x**y)**z)
 378
 379 instance GArrowDrop GArrowVerilog (,) where
 380   ga_drop      =
 381
 382 instance GArrowCopy GArrowVerilog (,) where
 383   ga_copy      =
 384
 385 instance GArrowSwap GArrowVerilog (,) where
 386   ga_swap      =
 387
 388 instance GArrowLoop GArrowVerilog (,) where
 389   ga_loop      =
 390
 391 instance GArrowLiteral GArrowVerilog (,) where
 392   ga_literal   =
 393 -}
 394
 395
 396
 397
 398 -- is there an official place to import this from so I don't have to write it myself?
 399
 400 ifThenElse True  a _ = a
 401 ifThenElse False _ b = b