examples/GArrowSkeleton.hs

   1 {-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies #-}
   2 -----------------------------------------------------------------------------
   3 -- |
   4 -- Module      :  GArrowSkeleton
   5 -- Copyright   :  none
   6 -- License     :  public domain
   7 --
   8 -- Maintainer  :  Adam Megacz <megacz@acm.org>
   9 -- Stability   :  experimental
  10 --
  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.
  14 --
  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.
  23 --
  24 module GArrowSkeleton (GArrowSkeleton(..), optimize)
  25 where
  26 import Prelude hiding ( id, (.), lookup )
  27 import Control.Category
  28 import GHC.HetMet.GArrow
  29 import Unify
  30 import Control.Monad.State
  31
  32 data GArrowSkeleton m :: * -> * -> *
  33  where
  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
  52
  53 instance Category (GArrowSkeleton m) where
  54   id           = GAS_id
  55   g . f        = GAS_comp f g
  56
  57 instance GArrow (GArrowSkeleton m) (,) () where
  58   ga_first     = GAS_first
  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
  64   ga_assoc     = GAS_assoc
  65   ga_unassoc   = GAS_unassoc
  66
  67 instance GArrowDrop (GArrowSkeleton m) (,) () where
  68   ga_drop      = GAS_drop
  69
  70 instance GArrowCopy (GArrowSkeleton m) (,) () where
  71   ga_copy      = GAS_copy
  72
  73 instance GArrowSwap (GArrowSkeleton m) (,) () where
  74   ga_swap      = GAS_swap
  75
  76 instance GArrowLoop (GArrowSkeleton m) (,) () where
  77   ga_loopl     = GAS_loopl
  78   ga_loopr     = GAS_loopr
  79
  80 type instance GArrowTensor      (GArrowSkeleton m) = (,)
  81 type instance GArrowUnit        (GArrowSkeleton m) = ()
  82 type instance GArrowExponent    (GArrowSkeleton m) = (->)
  83
  84 instance GArrowSTKCL (GArrowSkeleton m)
  85
  86 --
  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.
  90 --
  91 instance Eq ((GArrowSkeleton m) a b)
  92  where
  93   x == y = x === y
  94    where
  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'
 113     _ === _                                     = False
 114     -- FIXME: GAS_misc's are never equal!!!
 115
 116 --
 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.
 120 --
 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'
 123  where
 124   optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
 125
 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
 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))
 133
 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'
 137                                               where
 138                                                 f' = optimize' f
 139                                                 g' = optimize' g
 140                                                 h' = optimize' h
 141   optimize' (GAS_comp      f g     ) = case optimize_pair f g of
 142                                          Nothing   -> GAS_comp f' g'
 143                                          Just ret' -> ret'
 144                                         where
 145                                          f' = optimize' f
 146                                          g' = optimize' 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
 155   optimize' x                   = x
 156
 157   optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
 158
 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
 168
 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
 174
 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
 181
 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)
 184
 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
 189
 190
 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)
 194
 195   optimize_pair _ _                           = Nothing
 196
 197