1 {-# LANGUAGE RankNTypes, MultiParamTypeClasses, TypeOperators, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
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.GArrowFullyEnriched
33 import Prelude hiding (id, (.))
36 -- Importing GHC.HetMet.Arrow leads to overlapping instances; that's
37 -- why you see (GArrow (->) (,) () => ...) below in many places
38 -- instead of simply providing the instance defined in
41 --import GHC.HetMet.Arrow
46 ------------------------------------------------------------------------
49 -- | An "internal generalized arrow" is a GArrow except that it uses
50 -- some *other* GArrow in place of Haskell's function space.
52 class GArrow g (**) u => IGArrow g (**) u gg (***) uu | g -> (**), (**) -> u, gg -> (***), (***) -> uu where
53 iga_id :: g u (gg x x)
54 iga_comp :: g ((gg x y) ** (gg y z)) (gg x z)
55 iga_first :: g (gg x y) (gg (x *** z) (y *** z))
56 iga_second :: g (gg x y) (gg (z *** x) (z *** y))
57 iga_cancell :: g u (gg (uu***x) x)
58 iga_cancelr :: g u (gg (x***uu) x)
59 iga_uncancell :: g u (gg x (uu***x))
60 iga_uncancelr :: g u (gg x (x***uu))
61 iga_assoc :: g u (gg ((x*** y)***z ) ( x***(y ***z)))
62 iga_unassoc :: g u (gg ( x***(y ***z)) ((x*** y)***z ))
64 class IGArrow g (**) u gg (***) uu => IGArrowCopy g (**) u gg (***) uu where
65 iga_copy :: g u (gg x (x***x))
67 class IGArrow g (**) u gg (***) uu => IGArrowDrop g (**) u gg (***) uu where
68 iga_drop :: g u (gg x uu)
70 class IGArrow g (**) u gg (***) uu => IGArrowSwap g (**) u gg (***) uu where
71 iga_swap :: g u (gg (x***y) (y***x))
73 class IGArrow g (**) u gg (***) uu => IGArrowLoop g (**) u gg (***) uu where
74 iga_loopr :: g (gg (x***z) (y***z)) (gg x y)
75 iga_loopl :: g (gg (z***x) (z***y)) (gg x y)
77 class IGArrow g (**) u gg (***) uu => IGArrowLiteral g (**) u gg (***) uu t r where
78 iga_literal :: g t (gg uu r)
80 class IGArrow g (**) u gg (***) uu => IGArrowEval g (**) u gg (***) uu r t where
81 iga_eval :: g (gg uu r) t
83 class IGArrow g (**) u gg (***) uu => IGArrowConstant g (**) u gg (***) uu t r where
84 iga_constant :: g t (gg uu r)
86 class IGArrow g (**) u gg (***) uu => IGArrowReify g (**) u gg (***) uu x y r q where
87 iga_reify :: g (g x y) (gg r q)
89 class IGArrow g (**) u gg (***) uu => IGArrowReflect g (**) u gg (***) uu r q x y where
90 iga_reflect :: g (gg r q) (g x y)
94 ------------------------------------------------------------------------
97 -- | An IGArrow may be "externalized" to form a normal generalized
98 -- arrow. If the IGArrow was an instance of class IGArrowXX, the
99 -- externalization will be an instance of GArrowYY.
101 -- TODO: I should be one level deeper here: assuming an (IGArrow
102 -- (IGArrow g)), create an (IGArrow g).
105 newtype Ex g x y = Ex (g x y)
108 -- | Every IGArrow of (->) is a GArrow
110 instance IGArrow (->) (,) () g (**) u => Category (Ex g) where
112 (Ex g) . (Ex f) = Ex (iga_comp (f,g))
114 instance IGArrow (->) (,) () g (**) u => GArrow (Ex g) (**) u where
115 ga_first (Ex f) = Ex $ iga_first f
116 ga_second (Ex f) = Ex $ iga_second f
117 ga_cancell = Ex $ iga_cancell ()
118 ga_cancelr = Ex $ iga_cancelr ()
119 ga_uncancell = Ex $ iga_uncancell ()
120 ga_uncancelr = Ex $ iga_uncancelr ()
121 ga_assoc = Ex $ iga_assoc ()
122 ga_unassoc = Ex $ iga_unassoc ()
124 instance IGArrowCopy (->) (,) () g (**) u => GArrowCopy (Ex g) (**) u where
125 ga_copy = Ex $ iga_copy ()
126 instance IGArrowDrop (->) (,) () g (**) u => GArrowDrop (Ex g) (**) u where
127 ga_drop = Ex $ iga_drop ()
128 instance IGArrowSwap (->) (,) () g (**) u => GArrowSwap (Ex g) (**) u where
129 ga_swap = Ex $ iga_swap ()
135 ------------------------------------------------------------------------
138 -- | Every GArrow is internal to the GArrow instance on (->)
141 newtype In g x y = In (g x y)
143 instance (GArrow (->) (,) (), GArrow g (**) u) => IGArrow (->) (,) () (In g) (**) u where
145 iga_comp (In f,In g) = In $ f >>> g
146 iga_first (In f) = In $ ga_first f
147 iga_second (In f) = In $ ga_second f
148 iga_cancell _ = In $ ga_cancell
149 iga_cancelr _ = In $ ga_cancelr
150 iga_uncancell _ = In $ ga_uncancell
151 iga_uncancelr _ = In $ ga_uncancelr
152 iga_assoc _ = In $ ga_assoc
153 iga_unassoc _ = In $ ga_unassoc
154 instance (GArrow (->) (,) (), GArrowCopy g (**) u) => IGArrowCopy (->) (,) () (In g) (**) u where
155 iga_copy _ = In $ ga_copy
156 instance (GArrow (->) (,) (), GArrowDrop g (**) u) => IGArrowDrop (->) (,) () (In g) (**) u where
157 iga_drop _ = In $ ga_drop
158 instance (GArrow (->) (,) (), GArrowSwap g (**) u) => IGArrowSwap (->) (,) () (In g) (**) u where
159 iga_swap _ = In $ ga_swap
165 ------------------------------------------------------------------------
168 -- | This is named "kappa" for its similarity to an operator in
169 -- Hasegawa's kappa-calculus, but the formal connection is a bit of
170 -- a stretch; the method iga_kappa below is used by the flattener to
171 -- implement the typing rule for abstraction in Kappa-calculus.
174 -- -------------------------- [Kappa]
178 class GArrow g (**) u => IKappa g (**) u where
179 iga_kappa :: forall a b c .
180 (forall gg (***) uu . (IGArrowCopy g (**) u gg (***) uu,
181 IGArrowDrop g (**) u gg (***) uu,
182 IGArrowSwap g (**) u gg (***) uu) =>
183 g (gg uu a) (gg b c)) ->
184 (forall gg (***) uu . (IGArrowCopy g (**) u gg (***) uu,
185 IGArrowDrop g (**) u gg (***) uu,
186 IGArrowSwap g (**) u gg (***) uu) =>
188 -- TO DO: change the above to iga_kappal, add iga_kappar
191 -- | The (->) GArrow has the Kappa property.
193 instance GArrow (->) (,) () => IKappa (->) (,) () where
194 iga_kappa f = case (homfunctor_inv (\x -> case f (In x) of In x' -> x')) of Ex x -> \() -> x
201 ------------------------------------------------------------------------------
202 -- Self-Internal GArrows
205 -- | A self-internal GArrow is, well, internal to itself
207 class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
210 -- | Self-internal GArrows have curry/apply
212 instance SelfInternalGArrow g (**) u => GArrowApply g (**) u g where
213 ga_applyl = error "FIXME: SelfInternalGArrow => GArrowApply not implemented yet"
214 ga_applyr = error "FIXME: SelfInternalGArrow => GArrowApply not implemented yet"
217 -- | Self-internal GArrows have curry/apply
219 instance SelfInternalGArrow g (**) u => GArrowCurry g (**) u g where
220 ga_curryl = error "FIXME: SelfInternalGArrow => GArrowCurry not implemented yet"
221 ga_curryr = error "FIXME: SelfInternalGArrow => GArrowCurry not implemented yet"
224 -- | Haskell's function space is self-internal
226 instance GArrow (->) (,) () => IGArrow (->) (,) () (->) (,) () where
228 iga_comp (f,g) = f >>> g
230 iga_second = ga_second
231 iga_cancell _ = ga_cancell
232 iga_cancelr _ = ga_cancelr
233 iga_uncancell _ = ga_uncancell
234 iga_uncancelr _ = ga_uncancelr
235 iga_assoc _ = ga_assoc
236 iga_unassoc _ = ga_unassoc
238 --instance GArrow (->) (,) () => SelfInternalGArrow (->) (,) ()