From: Adam Megacz Date: Tue, 29 Mar 2011 11:15:27 +0000 (-0700) Subject: reorganized examples directory X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=caa7ad74b99b34abc5181553e66423da6bdfee26 reorganized examples directory --- diff --git a/examples/BiGArrow.hs b/examples/BiGArrow.hs new file mode 100644 index 0000000..466fbc2 --- /dev/null +++ b/examples/BiGArrow.hs @@ -0,0 +1,100 @@ +{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs -XUndecidableInstances #-} +module BiGArrow +where +import GHC.HetMet.GArrow +import Control.Category +import Control.Arrow +import Prelude hiding ( id, (.) ) + + + +-------------------------------------------------------------------------------- +-- 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 + + + + +-------------------------------------------------------------------------------- +-- GArrow-pairs are BiGArrows (but not a GArrowDrop!) + +-- 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 ... + + + + +-------------------------------------------------------------------------------- +-- BCPierce's symmetric lenses form a BiGArrow *with* GArrowSwap + + +-- NOTE: if you uncomment, this BE SURE YOU ARE NOT USING -fcoqpass -- +-- the code below will trigger one of the not-yet-fixed bugs in the +-- code that turns GHC CoreSyn into strongly-typed Coq expressions. + +{- +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 +-} diff --git a/examples/CircuitExample.hs b/examples/CircuitExample.hs new file mode 100644 index 0000000..f4f5151 --- /dev/null +++ b/examples/CircuitExample.hs @@ -0,0 +1,48 @@ +{-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds -XMultiParamTypeClasses -XTypeOperators #-} +module CircuitExample +where +import GHC.HetMet.CodeTypes hiding ((-)) +import GHC.HetMet.GArrow +import Control.Category +import Prelude hiding ( id, (.) ) + +-- +-- From the Appendix of Hughes' __Programming with Arrows__ +-- + +class GArrowLoop g (**) u => GArrowCircuit g (**) u b where + delay :: Bool -> g b b + +-- GArrows which can implment LookUp Tables (LUTs) +class GArrow g (**) u => GArrowLUT g (**) u b where + lut1 :: ( Bool -> Bool) -> g b b + lut2 :: ((Bool,Bool) -> Bool) -> g (b,b) b + lut3 :: ((Bool,Bool,Bool) -> Bool) -> g (b,b,b) b + +nor = lut2 (not.uncurry (||)) + +flipflop = ga_loopl $ ga_second ga_swap >>> + ga_assoc >>> + ga_second ga_unassoc >>> + ga_second (ga_first ga_swap) >>> + ga_second ga_assoc >>> + ga_unassoc >>> + ga_first nor >>> + ga_second nor >>> + ga_first (delay False) >>> + ga_second (delay True) >>> + ga_copy + +edge = ga_copy >>> + ga_first (delay False) >>> + lut2 (\(x,y) -> x && (not y)) + +-- 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) diff --git a/examples/CommandSyntaxExample.hs b/examples/CommandSyntaxExample.hs new file mode 100644 index 0000000..e06920c --- /dev/null +++ b/examples/CommandSyntaxExample.hs @@ -0,0 +1,40 @@ +{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds #-} +module CommandSyntaxExample +where + +-- +-- Please ignore this; I never got around to implementing it. +-- + +{- +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} + + +-- 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 +-} diff --git a/examples/DotProduct.hs b/examples/DotProduct.hs new file mode 100644 index 0000000..6de0c01 --- /dev/null +++ b/examples/DotProduct.hs @@ -0,0 +1,65 @@ +{-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds -XFlexibleContexts #-} +module DotProduct +where +import GHC.HetMet.CodeTypes hiding ((-)) +import Prelude hiding ( id, (.) ) + +-------------------------------------------------------------------------------- +-- 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 ]> diff --git a/examples/GArrowTutorial.hs b/examples/GArrowTutorial.hs new file mode 100644 index 0000000..c614d0d --- /dev/null +++ b/examples/GArrowTutorial.hs @@ -0,0 +1,214 @@ +{-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -XFlexibleContexts -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds #-} +module GArrowTutorial +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. +-- + +-------------------------------------------------------------------------------- +-- 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 ]> + + + diff --git a/examples/GArrowVerilog.hs b/examples/GArrowVerilog.hs new file mode 100644 index 0000000..c867dac --- /dev/null +++ b/examples/GArrowVerilog.hs @@ -0,0 +1,65 @@ +{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds #-} +module GArrowVerilog +where +import Prelude hiding ( id, (.) ) + +-- +-- Please ignore this; I didn't manage to finish it +-- + + +{- +-- 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 = +-} diff --git a/examples/ImmutableHeap.hs b/examples/ImmutableHeap.hs new file mode 100644 index 0000000..56ff12c --- /dev/null +++ b/examples/ImmutableHeap.hs @@ -0,0 +1,23 @@ +{-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -ddump-types -XNoMonoPatBinds #-} +module ImmutableHeap +where +import IsomorphismForCodeTypes +import Prelude hiding ( id, (.) ) + + +class GuestLanguageHeap c where + alloc :: <[ (Integer,Integer) -> Integer ]>@c + lookup :: <[ Integer -> (Integer,Integer) ]>@c + +-- +-- Here's nice example of Sheard's observation that it's often easier +-- to write two-stage programs by applying "back" to some function rather than +-- writing the final result directly +-- +onetwocycle = back onetwocycle' + where + onetwocycle' xy = <[ let (x,y) = ~~xy + in let x' = ~~alloc (1,x) + in let y' = ~~alloc (2,y) + in (x',y') + ]> diff --git a/examples/IsomorphismForCodeTypes.hs b/examples/IsomorphismForCodeTypes.hs new file mode 100644 index 0000000..6e245d7 --- /dev/null +++ b/examples/IsomorphismForCodeTypes.hs @@ -0,0 +1,12 @@ +{-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds #-} +module IsomorphismForCodeTypes +where + +-------------------------------------------------------------------------------- +-- 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 ]> diff --git a/examples/LambdaCalculusInterpreter.hs b/examples/LambdaCalculusInterpreter.hs new file mode 100644 index 0000000..67aae51 --- /dev/null +++ b/examples/LambdaCalculusInterpreter.hs @@ -0,0 +1,49 @@ +{-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds #-} +module LambdaCalculusInterpreter +where +import Prelude hiding ( id, (.) ) + +-- +-- A two-stage (untyped) Lambda Calculus interpreter, from Hughes' +-- __Generalizing Monads to Arrows__. +-- + +-- +-- Note how we have to use environment classifiers to tie Env, Val, +-- and Exp together (I miss Coq's [Section] command!!), yet the result +-- of "eval" is polymorphic in this classifier -- so long as the "Env" +-- and "Val" share it. +-- + +type Id = String +data Exp = Var Id + | Add Exp Exp + | If Exp Exp Exp + | App Exp Exp + | Lam Id Exp + +type Env c = [(Id,Val c)] +data Val c = Num Int | Fun <[Val c -> Val c]>@c + + +-- +-- This won't work until I implement proper support for inductive +-- types in the guest language +-- + +{- +eval :: Exp -> forall c. <[ Env c -> Val c ]>@c + +eval (If e1 e2 e3) = <[ \env -> if ~~(eval e1) + then ~~(eval e2) + else ~~(eval e3) ]> + +eval (Add e1 e2) = <[ \env -> let (Num v1) = ~~(eval e1) env + in let (Num v2) = ~~(eval e2) env + in (Num (v1+v2)) ]> + +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 ]> +-} diff --git a/examples/RegexMatcher.hs b/examples/RegexMatcher.hs new file mode 100644 index 0000000..ca02755 --- /dev/null +++ b/examples/RegexMatcher.hs @@ -0,0 +1,163 @@ +{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -ddump-types #-} +module RegexMatcher +where +import GHC.HetMet.CodeTypes hiding ((-)) + +-------------------------------------------------------------------------------- +-- +-- A one-level Regular Expression matcher, adapted from +-- Nanevski+Pfenning's _Staged computation with names and necessity_, +-- Figure 5 +-- + +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. If the "b" argument is false +-- the expression must match at least one character before passing +-- control to the continuation (this avoids the equality test in the +-- Nanevski+Pfenning code) + +accept :: Stream s => + Regex -> + Bool -> -- may only match the empty string if this is True + (s -> Bool) -> + s -> + Bool + +accept Empty False k s = + False + +accept Empty True k s = + k s + +accept (Plus e1 e2) emptyOk k s = + (accept e1 emptyOk k s) || (accept e2 emptyOk k s) + +accept (Times e1 e2) True k s = + (accept e1 True (accept e2 True k)) s + +accept (Times e1 e2) False k s = + (accept e1 False (accept e2 True k)) s || + (accept e1 True (accept e2 False k)) s + +accept (Star e) emptyOk k s = + (emptyOk && (k s)) || + (accept e emptyOk (\s' -> accept (Star e) False k s') s) + +accept (Const c) emptyOk k s = + if s_empty s + then False + else (s_head s) == c && k (s_tail s) + + + +-------------------------------------------------------------------------------- +-- +-- A two-level Regular Expression matcher, adapted from +-- Nanevski+Pfenning's _Staged computation with names and necessity_, +-- Figure 6 +-- + +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 + -> Bool + -> forall c s. + GuestStream c s => + GuestCharLiteral c => + GuestLanguageBool c => + GuestEqChar c => + <[ s -> Bool ]>@c + -> <[ s -> Bool ]>@c + +staged_accept Empty False k = + <[ \s -> false ]> + +staged_accept Empty True k = + <[ \s -> gs_empty s ]> + +staged_accept (Plus e1 e2) emptyOk k = + <[ \s -> let k' = ~~k + in (~~(staged_accept e1 emptyOk <[k']>) s) || + (~~(staged_accept e2 emptyOk <[k']>) s) + ]> + +staged_accept (Times e1 e2) True k = + <[ \s -> ~~(staged_accept e1 True (staged_accept e2 True k)) s ]> + +staged_accept (Times e1 e2) emptyOk k = + <[ \s -> ~~(staged_accept e1 True (staged_accept e2 False k)) s || + ~~(staged_accept e1 False (staged_accept e2 True k)) s + ]> + +staged_accept (Star e) emptyOk' k = + loop emptyOk' + where + -- loop :: Bool -> <[s -> Bool]>@g + loop emptyOk = if emptyOk + then <[ \s -> ~~k s || ~~(staged_accept e True (loop False)) s ]> + else <[ \s -> ~~(staged_accept e False (loop False)) 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) emptyOk k = + <[ \s -> if gs_empty s + then false + else (gs_head s) == ~~(guestCharLiteral c) && ~~k (gs_tail s) ]> + +-- +-- Take particular note of the "Plus" case above: note that (following +-- Nanevski+Pfenning) the code for "k" is not duplicated -- it is +-- escapified into the constructed term only once, and a tiny scrap of +-- code containing nothing more than the variable name k' is passed +-- to the recursive call. This is in contrast with the naive implementation +-- shown below: +-- +-- staged_accept (Plus e1 e2) emptyOk k = +-- <[ \s -> (~~(staged_accept e1 emptyOk k) s) || +-- (~~(staged_accept e2 emptyOk k) s) +-- ]> +-- + +-- +-- The following commented-out type is "too polymorphic" -- try +-- uncommenting it to see what happens. It's a great example of the +-- kind of thing that environment classifiers guard against: the +-- continuation code and the result code get their classifiers +-- unified. +-- +{- +staged_accept :: + Regex + -> Bool + -> (forall c s. + GuestStream c s => + GuestCharLiteral c => + GuestLanguageBool c => + GuestEqChar c => + <[s -> Bool]>@c) + -> (forall c s. + GuestStream c s => + GuestCharLiteral c => + GuestLanguageBool c => + GuestEqChar c => + <[s -> Bool]>@c) +-} diff --git a/examples/TypeSafeRun.hs b/examples/TypeSafeRun.hs new file mode 100644 index 0000000..52978da --- /dev/null +++ b/examples/TypeSafeRun.hs @@ -0,0 +1,35 @@ +{-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds #-} +module TypeSafeRun +where +import Prelude hiding ( id, (.) ) + +-------------------------------------------------------------------------------- +-- 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 diff --git a/examples/Unflattening.hs b/examples/Unflattening.hs new file mode 100644 index 0000000..f9ca4ba --- /dev/null +++ b/examples/Unflattening.hs @@ -0,0 +1,47 @@ +{-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds -XMultiParamTypeClasses #-} +module Unflattening +where +import GHC.HetMet.CodeTypes hiding ((-)) +import GHC.HetMet.GArrow +import Control.Category +import Control.Arrow +import Prelude hiding ( id, (.) ) + +-------------------------------------------------------------------------------- +-- 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) ]> + +instance GArrowDrop Code (,) () where + ga_drop = Code <[ \_ -> u ]> + +instance GArrowCopy Code (,) () where + ga_copy = Code <[ \x -> (x,x) ]> + +instance GArrowSwap Code (,) () where + ga_swap = Code <[ \(x,y) -> (y,x) ]> diff --git a/examples/tutorial.hs b/examples/tutorial.hs deleted file mode 100644 index 7668eab..0000000 --- a/examples/tutorial.hs +++ /dev/null @@ -1,827 +0,0 @@ -{-# 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 --} - - -