1 {-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies #-}
2 -----------------------------------------------------------------------------
4 -- Module : GArrowSkeleton
6 -- License : public domain
8 -- Maintainer : Adam Megacz <megacz@acm.org>
9 -- Stability : experimental
11 -- | Sometimes it is convenient to be able to get your hands on the
12 -- explicit boxes-and-wires representation of a GArrow-polymorphic
13 -- term. GArrowSkeleton lets you do that.
15 -- HOWEVER: technically this instance violates the laws (and RULEs)
16 -- for Control.Category; the compiler might choose to optimize (f >>>
17 -- id) into f, and this optimization would produce a change in
18 -- behavior below -- you'd get (GAS_comp f GAS_id) instead of f. In
19 -- practice this means that the user must be prepared for the skeleton
20 -- TikZ diagram to be a nondeterministically-chosen boxes-and-wires
21 -- diagram which ks *equivalent to* the term, rather than structurally
22 -- exactly equal to it.
24 module GArrowSkeleton (GArrowSkeleton(..), optimize)
26 import Prelude hiding ( id, (.), lookup )
27 import Control.Category
28 import GHC.HetMet.GArrow
30 import Control.Monad.State
32 data GArrowSkeleton m :: * -> * -> *
34 GAS_const :: Int -> GArrowSkeleton m () Int
35 GAS_id :: GArrowSkeleton m x x
36 GAS_comp :: GArrowSkeleton m x y -> GArrowSkeleton m y z -> GArrowSkeleton m x z
37 GAS_first :: GArrowSkeleton m x y -> GArrowSkeleton m (x,z) (y,z)
38 GAS_second :: GArrowSkeleton m x y -> GArrowSkeleton m (z,x) (z,y)
39 GAS_cancell :: GArrowSkeleton m ((),x) x
40 GAS_cancelr :: GArrowSkeleton m (x,()) x
41 GAS_uncancell :: GArrowSkeleton m x ((),x)
42 GAS_uncancelr :: GArrowSkeleton m x (x,())
43 GAS_assoc :: GArrowSkeleton m ((x,y),z) (x,(y,z))
44 GAS_unassoc :: GArrowSkeleton m (x,(y,z)) ((x,y),z)
45 GAS_drop :: GArrowSkeleton m x ()
46 GAS_copy :: GArrowSkeleton m x (x,x)
47 GAS_swap :: GArrowSkeleton m (x,y) (y,x)
48 GAS_merge :: GArrowSkeleton m (x,y) z
49 GAS_loopl :: GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y
50 GAS_loopr :: GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y
51 GAS_misc :: m x y -> GArrowSkeleton m x y
53 instance Category (GArrowSkeleton m) where
57 instance GArrow (GArrowSkeleton m) (,) () where
59 ga_second = GAS_second
60 ga_cancell = GAS_cancell
61 ga_cancelr = GAS_cancelr
62 ga_uncancell = GAS_uncancell
63 ga_uncancelr = GAS_uncancelr
65 ga_unassoc = GAS_unassoc
67 instance GArrowDrop (GArrowSkeleton m) (,) () where
70 instance GArrowCopy (GArrowSkeleton m) (,) () where
73 instance GArrowSwap (GArrowSkeleton m) (,) () where
76 instance GArrowLoop (GArrowSkeleton m) (,) () where
80 type instance GArrowTensor (GArrowSkeleton m) = (,)
81 type instance GArrowUnit (GArrowSkeleton m) = ()
82 type instance GArrowExponent (GArrowSkeleton m) = (->)
84 instance GArrowSTKC (GArrowSkeleton m)
87 -- | Simple structural equality on skeletons. NOTE: two skeletons
88 -- with the same shape but different types will nonetheless be "equal";
89 -- there's no way around this since types are gone at runtime.
91 instance Eq ((GArrowSkeleton m) a b)
95 (===) :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) c d -> Bool
96 (GAS_id ) === (GAS_id ) = True
97 (GAS_comp g f) === (GAS_comp g' f') = f===f' && g===g'
98 (GAS_first f) === (GAS_first f') = f===f'
99 (GAS_second f) === (GAS_second f') = f===f'
100 GAS_cancell === GAS_cancell = True
101 GAS_cancelr === GAS_cancelr = True
102 GAS_uncancell === GAS_uncancell = True
103 GAS_uncancelr === GAS_uncancelr = True
104 GAS_drop === GAS_drop = True
105 (GAS_const i) === (GAS_const i') = i==i'
106 GAS_copy === GAS_copy = True
107 GAS_merge === GAS_merge = True
108 GAS_swap === GAS_swap = True
109 GAS_assoc === GAS_assoc = True
110 GAS_unassoc === GAS_unassoc = True
111 (GAS_loopl f) === (GAS_loopl f') = f === f'
112 (GAS_loopr f) === (GAS_loopr f') = f === f'
114 -- FIXME: GAS_misc's are never equal!!!
117 -- | Performs some very simple-minded optimizations on a
118 -- boxes-and-wires diagram. Preserves equivalence up to the GArrow
119 -- laws, but no guarantees about which optimizations actually happen.
121 optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
122 optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
124 optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
126 -- Some optimizations fail due to misparenthesization; we default to
127 -- left-associativity and hope for the best
128 optimize' (GAS_comp f (GAS_comp g h)) = GAS_comp (GAS_comp f g) h
129 optimize' (GAS_comp (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k
130 optimize' (GAS_comp (GAS_comp f g) h) = case optimize_pair g h of
131 Nothing -> GAS_comp (optimize' (GAS_comp f g)) h'
132 Just ret' -> GAS_comp f' ret'
137 optimize' (GAS_comp f g ) = case optimize_pair f g of
138 Nothing -> GAS_comp f' g'
143 optimize' (GAS_first GAS_id ) = GAS_id
144 optimize' (GAS_second GAS_id ) = GAS_id
145 optimize' (GAS_first f ) = GAS_first $ optimize' f
146 optimize' (GAS_second f ) = GAS_second $ optimize' f
147 optimize' (GAS_loopl GAS_id) = GAS_id
148 optimize' (GAS_loopr GAS_id) = GAS_id
149 optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f
150 optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f
153 optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
155 optimize_pair f GAS_drop = Just $ GAS_drop
156 optimize_pair GAS_id f = Just $ f
157 optimize_pair f GAS_id = Just $ f
158 optimize_pair GAS_uncancell GAS_cancell = Just $ GAS_id
159 optimize_pair GAS_uncancelr GAS_cancelr = Just $ GAS_id
160 optimize_pair GAS_cancell GAS_uncancell = Just $ GAS_id
161 optimize_pair GAS_cancelr GAS_uncancelr = Just $ GAS_id
162 optimize_pair GAS_uncancelr GAS_cancell = Just $ GAS_id
163 optimize_pair GAS_uncancell GAS_cancelr = Just $ GAS_id
165 -- first priority: eliminate GAS_first
166 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
167 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
168 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
169 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
171 -- second priority: push GAS_swap leftward... why isn't this working?
172 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
173 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
174 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
176 optimize_pair (GAS_first f) (GAS_first g) = Just $ GAS_first (GAS_comp f g)
177 optimize_pair (GAS_second f) (GAS_second g) = Just $ GAS_second (GAS_comp f g)
179 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
180 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
182 optimize_pair _ _ = Nothing