1 {-# LANGUAGE RankNTypes, MultiParamTypeClasses, NoMonomorphismRestriction, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts, FlexibleInstances, DatatypeContexts, UndecidableInstances, ScopedTypeVariables #-}
2 -----------------------------------------------------------------------------
4 -- Module : GHC.HetMet.IGArrow
6 -- License : public domain
8 -- Maintainer : Adam Megacz <megacz@acm.org>
9 -- Stability : experimental
10 -- Portability : portable
12 module GHC.HetMet.IGArrow (
26 -- IGArrowSum(..), ga_inl, ga_inr,
30 import Control.Category
31 import GHC.HetMet.GArrow
32 import GHC.HetMet.Arrow
33 import GHC.HetMet.GArrowFullyEnriched
34 import Prelude hiding (id, (.))
40 ------------------------------------------------------------------------
43 -- | An "internal generalized arrow" is a GArrow except that it uses
44 -- some *other* GArrow in place of Haskell's function space.
46 class GArrow g (**) u => IGArrow g (**) u gg (***) uu | gg -> (***), (***) -> uu where
47 iga_id :: g u (gg x x)
48 iga_comp :: g ((gg x y) ** (gg y z)) (gg x z)
49 iga_first :: g (gg x y) (gg (x *** z) (y *** z))
50 iga_second :: g (gg x y) (gg (z *** x) (z *** y))
51 iga_cancell :: g u (gg (uu***x) x)
52 iga_cancelr :: g u (gg (x***uu) x)
53 iga_uncancell :: g u (gg x (uu***x))
54 iga_uncancelr :: g u (gg x (x***uu))
55 iga_assoc :: g u (gg ((x*** y)***z ) ( x***(y ***z)))
56 iga_unassoc :: g u (gg ( x***(y ***z)) ((x*** y)***z ))
58 class IGArrow g (**) u gg (***) uu => IGArrowCopy g (**) u gg (***) uu where
59 iga_copy :: g u (gg x (x***x))
61 class IGArrow g (**) u gg (***) uu => IGArrowDrop g (**) u gg (***) uu where
62 iga_drop :: g u (gg x u)
64 class IGArrow g (**) u gg (***) uu => IGArrowSwap g (**) u gg (***) uu where
65 iga_swap :: g u (gg (x***y) (y***x))
67 class IGArrow g (**) u gg (***) uu => IGArrowLoop g (**) u gg (***) uu where
68 iga_loopr :: g (gg (x***z) (y***z)) (gg x y)
69 iga_loopl :: g (gg (z***x) (z***y)) (gg x y)
71 class IGArrow g (**) u gg (***) uu => IGArrowLiteral g (**) u gg (***) uu t r where
72 iga_literal :: g t (gg uu r)
74 class IGArrow g (**) u gg (***) uu => IGArrowEval g (**) u gg (***) uu r t where
75 iga_eval :: g (gg uu r) t
77 class IGArrow g (**) u gg (***) uu => IGArrowConstant g (**) u gg (***) uu t r where
78 iga_constant :: g t (gg uu r)
80 class IGArrow g (**) u gg (***) uu => IGArrowReify g (**) u gg (***) uu x y r q where
81 iga_reify :: g (g x y) (gg r q)
83 class IGArrow g (**) u gg (***) uu => IGArrowReflect g (**) u gg (***) uu r q x y where
84 iga_reflect :: g (gg r q) (g x y)
89 -- | This is named "kappa" for its similarity to an operator in
90 -- Hasegawa's kappa-calculus, but there isn't actually a formal
92 class GArrow g (**) u => IKappa g (**) u where
93 iga_kappa :: forall a b c uu .
94 (forall gg (***) . (IGArrow g (**) u gg (***) uu,
95 IGArrowCopy g (**) u gg (***) uu,
96 IGArrowSwap g (**) u gg (***) uu,
97 IGArrowDrop g (**) u gg (***) uu) => g (gg uu a) (gg b c)) ->
98 (forall gg (***) . (IGArrow g (**) u gg (***) uu,
99 IGArrowCopy g (**) u gg (***) uu,
100 IGArrowSwap g (**) u gg (***) uu,
101 IGArrowDrop g (**) u gg (***) uu) => g u (gg (a***b) c))
102 -- TO DO: probably need l/r versions of the above
104 --class IGArrow g (**) u gg (***) uu => IGArrowKappa g (**) u gg (***) uu where
105 -- iga_kappa :: g (x**(gg uu a)) (gg b c) -> g x (gg (a***b) c)
106 -- TO DO: probably need l/r versions of the above
112 ------------------------------------------------------------------------------
113 -- Self-Internal GArrows
116 -- | A self-internal GArrow is, well, internal to itself
118 --class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
121 -- | Self-internal GArrows have curry/apply
123 -- instance SelfInternalGArrow g (**) u => GArrowApply g (**) u gg where
124 -- ga_applyl = :: g (x**(g x y) ) y
125 -- ga_applyr :: g ( (g x y)**x) y
128 -- | Self-internal GArrows have curry/apply
130 -- instance SelfInternalGArrow g (**) u gg (***) uu => GArrowCurry g (**) u gg where
131 -- ga_curryl :: g (x**y) z -> g x (g y z)
132 -- ga_curryr :: g (x**y) z -> g y (g x z)
138 ------------------------------------------------------------------------------
142 -- | Every GArrow is internal to the GArrow instance on (->)
145 instance GArrow g (**) u => IGArrow (->) (,) () g (**) u where
147 iga_comp (f,g) = f >>> g
149 iga_second = ga_second
150 iga_cancell _ = ga_cancell
151 iga_cancelr _ = ga_cancelr
152 iga_uncancell _ = ga_uncancell
153 iga_uncancelr _ = ga_uncancelr
154 iga_assoc _ = ga_assoc
155 iga_unassoc _ = ga_unassoc
156 instance GArrowCopy g (**) u => IGArrowCopy (->) (,) () g (**) u where
157 instance GArrowSwap g (**) u => IGArrowSwap (->) (,) () g (**) u where
158 instance GArrowDrop g (**) u => IGArrowDrop (->) (,) () g (**) u where
164 instance GArrow g (**) u => IGArrow (->) (,) () (In g) (**) u where
165 instance GArrowCopy g (**) u => IGArrowCopy (->) (,) () (In g) (**) u where
166 instance GArrowSwap g (**) u => IGArrowSwap (->) (,) () (In g) (**) u where
167 instance GArrowDrop g (**) u => IGArrowDrop (->) (,) () (In g) (**) u where
169 ------------------------------------------------------------------------
172 -- | An IGArrow may be "externalized" to form a normal generalized
173 -- arrow. If the IGArrow was an instance of class IGArrowXX, the
174 -- externalization will be an instance of GArrowYY.
176 -- TODO: I should be one level deeper here: assuming an (IGArrow
177 -- (IGArrow g)), create an (IGArrow g).
186 -- | Every IGArrow of (->) is a GArrow
188 instance IGArrow (->) (,) () g (**) u => Category (Ext g) where
190 (Ext g) . (Ext f) = Ext (iga_comp (f,g))
192 instance IGArrow (->) (,) () g (**) u => GArrow (Ext g) (**) u where
193 -- ga_first (Ext f) = Ext $ iga_first f
194 -- ga_second (Ext f) = Ext $ iga_second f
195 ga_cancell = Ext $ iga_cancell ()
196 ga_cancelr = Ext $ iga_cancelr ()
197 ga_uncancell = Ext $ iga_uncancell ()
198 ga_uncancelr = Ext $ iga_uncancelr ()
199 ga_assoc = Ext $ iga_assoc ()
200 ga_unassoc = Ext $ iga_unassoc ()
202 instance IGArrowSwap (->) (,) () g (**) u => GArrowSwap (Ext g) (**) u where
203 instance IGArrowCopy (->) (,) () g (**) u => GArrowCopy (Ext g) (**) u where
204 instance IGArrowDrop (->) (,) () g (**) u => GArrowDrop (Ext g) (**) u where
207 -- iga_kappa :: forall a b c uu . (forall gg (***) . IGArrow g (**) u gg (***) uu => g (gg uu a) (gg b c)) ->
208 -- (forall gg (***) . IGArrow g (**) u gg (***) uu => g u (gg (a***b) c))
210 Could not deduce (GArrowDrop gg (***) uu,
211 GArrowSwap gg (***) uu,
212 GArrowCopy gg (***) uu)
213 arising from a use of `homfunctor_inv'
214 from the context (IGArrow (->) (,) () gg (***) uu)
217 --homfunctor_inv :: forall a b c u .
218 -- (forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c) ->
219 -- (forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c)
222 -- | Every GArrow is also an IKappa of (->) by virtue of GArrowFullyEnriched
224 instance IKappa (->) (,) () where
225 -- iga_kappa :: forall a b c u .
226 -- (forall g (**) . (IGArrow (->) (,) () g (**) u,
227 -- IGArrowCopy (->) (,) () g (**) u,
228 -- IGArrowSwap (->) (,) () g (**) u,
229 -- IGArrowDrop (->) (,) () g (**) u) => (g u a) -> (g b c)) ->
230 -- (forall g (**) . (IGArrow (->) (,) () g (**) u,
231 -- IGArrowCopy (->) (,) () g (**) u,
232 -- IGArrowSwap (->) (,) () g (**) u,
233 -- IGArrowDrop (->) (,) () g (**) u) => () -> (g (a**b) c))
234 iga_kappa (f :: forall g (**) .
235 (IGArrow (->) (,) () g (**) u,
236 IGArrowCopy (->) (,) () g (**) u,
237 IGArrowDrop (->) (,) () g (**) u,
238 IGArrowSwap (->) (,) () g (**) u) =>
240 = mork $ homfunctor_inv (\y -> case f (In y) of (In q) -> q)
242 mork :: forall u a b c .
243 (forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c)
244 -> (forall g (**) . (IGArrow (->) (,) () g (**) u,
245 IGArrowCopy (->) (,) () g (**) u,
246 IGArrowSwap (->) (,) () g (**) u,
247 IGArrowDrop (->) (,) () g (**) u) => (g (a**b) c))
250 z :: forall g (**) . IGArrow (->) (,) () g (**) u => g (a**b) c
252 qf :: forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c
254 in case homfunctor_inv qf of Ext q -> q
258 instance IGArrow (->) (,) () g (**) u => GArrowSTKC (Ext g)
261 -- instance IGArrow g (**) u gg (***) uu => GArrowCopy g (**) u gg (***) uu where
262 -- iga_copy = undefined
264 -- instance IGArrow g (**) u gg (***) uu => GArrowDrop g (**) u gg (***) uu where
265 -- iga_drop = undefined
267 -- instance IGArrow g (**) u gg (***) uu => GArrowSwap g (**) u gg (***) uu where
268 -- iga_swap = undefined
270 -- instance IGArrow g (**) u gg (***) uu => GArrowLoop g (**) u gg (***) uu where
271 -- iga_loopr = undefined
272 -- iga_loopl = undefined
274 -- instance IGArrow g (**) u gg (***) uu => GArrowLiteral g (**) u gg (***) uu t r where
275 -- iga_literal = undefined
277 -- instance IGArrow g (**) u gg (***) uu => GArrowEval g (**) u gg (***) uu r t where
278 -- iga_eval = undefined
280 -- instance IGArrow g (**) u gg (***) uu => GArrowConstant g (**) u gg (***) uu t r where
281 -- iga_constant = undefined
283 -- instance IGArrow g (**) u gg (***) uu => GArrowReify g (**) u gg (***) uu x y r q where
284 -- iga_reify = undefined
286 -- instance IGArrow g (**) u gg (***) uu => GArrowReflect g (**) u gg (***) uu r q x y where
287 -- iga_reflect = undefined
290 -- | Haskell's function space is self-internal
291 -- instance SelfInternalGArrow (->) (,) ()
295 -- -------------------------- [Kappa]
299 -- (forall g (**) u gg (***) uu .
300 -- IGArrow g (**) u gg (***) uu =>
301 -- g (x**(gg uu a)) (gg b c))
303 -- (forall g (**) u gg (***) uu .
304 -- IGArrow g (**) u gg (***) uu =>
305 -- g x (gg (a***b) c))