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 (z,x) (z,y) -> GArrowSkeleton m x y
50 GAS_loopr :: GArrowSkeleton m (x,z) (y,z) -> 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 GArrowSTKCL (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
131 optimize' (GAS_comp (GAS_comp GAS_unassoc (GAS_second g)) GAS_assoc) = GAS_second (GAS_second g)
132 optimize' (GAS_comp (GAS_comp (GAS_comp f GAS_unassoc) (GAS_second g)) GAS_assoc) = GAS_comp f (GAS_second (GAS_second g))
134 optimize' (GAS_comp (GAS_comp f g) h) = case optimize_pair g h of
135 Nothing -> GAS_comp (optimize' (GAS_comp f g)) h'
136 Just ret' -> GAS_comp f' ret'
141 optimize' (GAS_comp f g ) = case optimize_pair f g of
142 Nothing -> GAS_comp f' g'
147 optimize' (GAS_first GAS_id ) = GAS_id
148 optimize' (GAS_second GAS_id ) = GAS_id
149 optimize' (GAS_first f ) = GAS_first $ optimize' f
150 optimize' (GAS_second f ) = GAS_second $ optimize' f
151 optimize' (GAS_loopl GAS_id) = GAS_id
152 optimize' (GAS_loopr GAS_id) = GAS_id
153 optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f
154 optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f
157 optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
159 optimize_pair f GAS_drop = Just $ GAS_drop
160 optimize_pair GAS_id f = Just $ f
161 optimize_pair f GAS_id = Just $ f
162 optimize_pair GAS_uncancell GAS_cancell = Just $ GAS_id
163 optimize_pair GAS_uncancelr GAS_cancelr = Just $ GAS_id
164 optimize_pair GAS_cancell GAS_uncancell = Just $ GAS_id
165 optimize_pair GAS_cancelr GAS_uncancelr = Just $ GAS_id
166 optimize_pair GAS_uncancelr GAS_cancell = Just $ GAS_id
167 optimize_pair GAS_uncancell GAS_cancelr = Just $ GAS_id
169 -- first priority: eliminate GAS_first
170 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
171 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
172 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
173 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
175 -- second priority: push GAS_swap leftward
176 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
177 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
178 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
179 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
180 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
182 optimize_pair (GAS_first f) (GAS_first g) = Just $ GAS_first (GAS_comp f g)
183 optimize_pair (GAS_second f) (GAS_second g) = Just $ GAS_second (GAS_comp f g)
185 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
186 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
187 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
188 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
191 -- FIXME: valid only for central morphisms
192 --optimize_pair (GAS_second f) (GAS_first g) = Just $ GAS_comp (GAS_first g) (GAS_second f)
193 optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp (GAS_second f) (GAS_first g)
195 optimize_pair _ _ = Nothing