1 {-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs -XUndecidableInstances #-}
4 import GHC.HetMet.GArrow
5 import Control.Category
7 import Prelude hiding ( id, (.) )
11 --------------------------------------------------------------------------------
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
28 --------------------------------------------------------------------------------
29 -- GArrow-pairs are BiGArrows (but not a GArrowDrop!)
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 ...
54 --------------------------------------------------------------------------------
55 -- BCPierce's symmetric lenses form a BiGArrow *with* GArrowSwap
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.
64 Lens :: forall x y c1 c2 . ((x,c1)->(y,c2)) -> ((y,c2)->(x,c1)) -> Lens x y
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)))
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)),()))
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),()))
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