examples/BiGArrow.hs

   1 {-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs -XUndecidableInstances #-}
   2 module BiGArrow
   3 where
   4 import GHC.HetMet.GArrow
   5 import Control.Category
   6 import Control.Arrow
   7 import Prelude hiding ( id, (.) )
   8
   9
  10
  11 --------------------------------------------------------------------------------
  12 -- BiGArrows
  13
  14 class GArrow g (**) u => BiGArrow g (**) u where
  15   -- Note that we trust the user's pair of functions actually are
  16   -- mutually inverse; confirming this in the type system would
  17   -- require very powerful dependent types (such as Coq's).  However,
  18   -- the consequences of failure here are much more mild than failures
  19   -- in BiArrow.inv: if the functions below are not mutually inverse,
  20   -- the LoggingBiGArrow will simply compute the wrong result rather
  21   -- than fail in some manner outside the language's semantics.
  22   biga_arr :: (x -> y) -> (y -> x) -> g x y
  23   biga_inv :: g x y -> g y x
  24
  25
  26
  27
  28 --------------------------------------------------------------------------------
  29 -- GArrow-pairs are BiGArrows (but not a GArrowDrop!)
  30
  31 -- For any GArrow instance, its mutually inverse pairs form a BiGArrow
  32 data GArrow g (**) u => GArrowInversePair g (**) u x y =
  33     GArrowInversePair { forward :: g x y , backward :: g y x }
  34 instance GArrow g (**) u => Category (GArrowInversePair g (**) u) where
  35   id    = GArrowInversePair { forward = id , backward = id }
  36   f . g = GArrowInversePair { forward = (forward f) . (forward g) , backward = (backward g) . (backward f) }
  37 instance GArrow g (**) u => GArrow (GArrowInversePair g (**) u) (**) u where
  38   ga_first     f = GArrowInversePair { forward = ga_first  (forward f), backward = ga_first  (backward f) }
  39   ga_second    f = GArrowInversePair { forward = ga_second (forward f), backward = ga_second (backward f) }
  40   ga_cancell     = GArrowInversePair { forward = ga_cancell           , backward = ga_uncancell }
  41   ga_cancelr     = GArrowInversePair { forward = ga_cancelr           , backward = ga_uncancelr }
  42   ga_uncancell   = GArrowInversePair { forward = ga_uncancell         , backward = ga_cancell   }
  43   ga_uncancelr   = GArrowInversePair { forward = ga_uncancelr         , backward = ga_cancelr   }
  44   ga_assoc       = GArrowInversePair { forward = ga_assoc             , backward = ga_unassoc   }
  45   ga_unassoc     = GArrowInversePair { forward = ga_unassoc           , backward = ga_assoc     }
  46 instance GArrowSwap g (**) u => GArrowSwap (GArrowInversePair g (**) u) (**) u where
  47   ga_swap = GArrowInversePair { forward = ga_swap , backward = ga_swap }
  48 -- but notice that we can't (in general) get
  49 -- instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...
  50
  51
  52
  53
  54 --------------------------------------------------------------------------------
  55 -- BCPierce's symmetric lenses form a BiGArrow *with* GArrowSwap
  56
  57
  58 -- NOTE: if you uncomment, this BE SURE YOU ARE NOT USING -fcoqpass --
  59 -- the code below will trigger one of the not-yet-fixed bugs in the
  60 -- code that turns GHC CoreSyn into strongly-typed Coq expressions.
  61
  62 {-
  63 data Lens x y where
  64   Lens :: forall x y c1 c2 . ((x,c1)->(y,c2)) -> ((y,c2)->(x,c1)) -> Lens x y
  65
  66 -- can we make lenses out of GArrows other than (->)?
  67 instance Category Lens where
  68   id                          = Lens (\x -> x) (\x -> x)
  69   (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)))
  70                                      (\(z,(c1,c2)) -> let (y,gc) = g2 (z,c2) in  let (x,fc) = f2 (y,c1) in  (x,(fc,gc)))
  71
  72 instance GArrow Lens (,) () where
  73   ga_first     (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x1,c) in ((y,x2),c'))
  74                                    (\((x1,x2),c) -> let (y,c') = f2 (x1,c) in ((y,x2),c'))
  75   ga_second    (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x2,c) in ((x1,y),c'))
  76                                    (\((x1,x2),c) -> let (y,c') = f2 (x2,c) in ((x1,y),c'))
  77   ga_cancell                = Lens (\(((),x),()) -> (    x ,()))
  78                                    (\(    x ,()) -> (((),x),()))
  79   ga_uncancell              = Lens (\(    x ,()) -> (((),x),()))
  80                                    (\(((),x),()) -> (    x ,()))
  81   ga_cancelr                = Lens (\((x,()),()) -> (    x ,()))
  82                                    (\( x    ,()) -> ((x,()),()))
  83   ga_uncancelr              = Lens (\( x    ,()) -> ((x,()),()))
  84                                    (\((x,()),()) -> (    x ,()))
  85   ga_assoc                  = Lens (\(((x,y),z),()) -> ((x,(y,z)),()))
  86                                    (\((x,(y,z)),()) -> (((x,y),z),()))
  87   ga_unassoc                = Lens (\((x,(y,z)),()) -> (((x,y),z),()))
  88                                    (\(((x,y),z),()) -> ((x,(y,z)),()))
  89
  90 instance GArrowDrop Lens (,) () where
  91   ga_drop        = Lens (\(x,()) -> ((),x)) (\((),x) -> (x,()))
  92 instance GArrowCopy Lens (,) () where
  93   ga_copy        = Lens (\(x,()) -> ((x,x),())) (\((x,_),()) -> (x,()))
  94 instance GArrowSwap Lens (,) () where
  95   ga_swap        = Lens (\((x,y),()) -> ((y,x),())) (\((x,y),()) -> ((y,x),()))
  96
  97 instance BiGArrow Lens (,) () where
  98   biga_arr f f'  = Lens (\(x,()) -> ((f x),())) (\(x,()) -> ((f' x),()))
  99   biga_inv (Lens f1 f2) = Lens f2 f1
 100 -}