GHC/HetMet/IGArrow.hs

   1 {-# LANGUAGE RankNTypes, MultiParamTypeClasses, NoMonomorphismRestriction, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts, FlexibleInstances, DatatypeContexts, UndecidableInstances, ScopedTypeVariables #-}
   2 -----------------------------------------------------------------------------
   3 -- |
   4 -- Module      :  GHC.HetMet.IGArrow
   5 -- Copyright   :  none
   6 -- License     :  public domain
   7 --
   8 -- Maintainer  :  Adam Megacz <megacz@acm.org>
   9 -- Stability   :  experimental
  10 -- Portability :  portable
  11
  12 module GHC.HetMet.IGArrow (
  13   IGArrow(..),
  14   IGArrowDrop(..),
  15   IGArrowCopy(..),
  16   IGArrowSwap(..),
  17   IGArrowLoop(..),
  18
  19   IGArrowEval(..),
  20   IGArrowConstant(..),
  21   IGArrowLiteral(..),
  22
  23   IGArrowReify(..),
  24   IGArrowReflect(..),
  25
  26   -- IGArrowSum(..),  ga_inl, ga_inr,
  27   -- IGArrowProd(..),
  28
  29 ) where
  30 import Control.Category
  31 import GHC.HetMet.GArrow
  32 import GHC.HetMet.Arrow
  33 import GHC.HetMet.GArrowFullyEnriched
  34 import Prelude          hiding (id, (.))
  35
  36
  37
  38
  39
  40 ------------------------------------------------------------------------
  41 -- Internal GArrows
  42 --
  43 -- | An "internal generalized arrow" is a GArrow except that it uses
  44 -- some *other* GArrow in place of Haskell's function space.
  45 --
  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 ))
  57
  58 class IGArrow g (**) u gg (***) uu => IGArrowCopy g (**) u gg (***) uu where
  59   iga_copy      :: g u (gg x (x***x))
  60
  61 class IGArrow g (**) u gg (***) uu => IGArrowDrop g (**) u gg (***) uu where
  62   iga_drop      :: g u (gg x u)
  63
  64 class IGArrow g (**) u gg (***) uu => IGArrowSwap g (**) u gg (***) uu where
  65   iga_swap      :: g u (gg (x***y) (y***x))
  66
  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)
  70
  71 class IGArrow g (**) u gg (***) uu => IGArrowLiteral g (**) u gg (***) uu t r where
  72   iga_literal  :: g t (gg uu r)
  73
  74 class IGArrow g (**) u gg (***) uu => IGArrowEval g (**) u gg (***) uu r t where
  75   iga_eval      :: g (gg uu r) t
  76
  77 class IGArrow g (**) u gg (***) uu => IGArrowConstant g (**) u gg (***) uu t r where
  78   iga_constant  :: g t (gg uu r)
  79
  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)
  82
  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)
  85
  86
  87
  88 {-
  89 -- | This is named "kappa" for its similarity to an operator in
  90 --   Hasegawa's kappa-calculus, but there isn't actually a formal
  91 --   connection.
  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
 103
 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
 107
 108
 109
 110
 111
 112 ------------------------------------------------------------------------------
 113 -- Self-Internal GArrows
 114
 115 --
 116 -- | A self-internal GArrow is, well, internal to itself
 117 --
 118 --class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
 119
 120 --
 121 -- | Self-internal GArrows have curry/apply
 122 --
 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
 126 --
 127 --
 128 -- | Self-internal GArrows have curry/apply
 129 --
 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)
 133
 134
 135
 136
 137
 138 ------------------------------------------------------------------------------
 139 -- Instances
 140
 141 --
 142 -- | Every GArrow is internal to the GArrow instance on (->)
 143 --
 144 {-
 145 instance GArrow g (**) u => IGArrow (->) (,) () g (**) u where
 146   iga_id        _     = id
 147   iga_comp      (f,g) = f >>> g
 148   iga_first           = ga_first
 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
 159 -}
 160
 161 data
 162     In g x y
 163     = In (g x y)
 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
 168
 169 ------------------------------------------------------------------------
 170 -- Externalization
 171 --
 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.
 175 --
 176 -- TODO: I should be one level deeper here: assuming an (IGArrow
 177 -- (IGArrow g)), create an (IGArrow g).
 178 --
 179
 180 data
 181     Ext g x y
 182     = Ext (g x y)
 183
 184
 185 --
 186 -- | Every IGArrow of (->) is a GArrow
 187 --
 188 instance IGArrow (->) (,) () g (**) u => Category (Ext g) where
 189   id                = Ext (iga_id ())
 190   (Ext g) . (Ext f) = Ext (iga_comp (f,g))
 191
 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 ()
 201
 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
 205
 206
 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))
 209 {-
 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)
 215 -}
 216
 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)
 220
 221 --
 222 -- | Every GArrow is also an IKappa of (->) by virtue of GArrowFullyEnriched
 223 --
 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) =>
 239                   (g u a)->(g b c)) ()
 240      = mork $ homfunctor_inv (\y -> case f (In y) of (In q) -> q)
 241
 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))
 248 mork = undefined
 249 {-
 250          z :: forall g (**) . IGArrow (->) (,) () g (**) u => g (a**b) c
 251          z = let
 252                qf :: forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c
 253                qf y = f y
 254              in case homfunctor_inv qf of Ext q -> q
 255 -}
 256
 257 {-
 258 instance IGArrow (->) (,) () g (**) u => GArrowSTKC (Ext g)
 259 -}
 260
 261 -- instance IGArrow g (**) u gg (***) uu => GArrowCopy g (**) u gg (***) uu where
 262 --   iga_copy      = undefined
 263 --
 264 -- instance IGArrow g (**) u gg (***) uu => GArrowDrop g (**) u gg (***) uu where
 265 --   iga_drop      = undefined
 266 --
 267 -- instance IGArrow g (**) u gg (***) uu => GArrowSwap g (**) u gg (***) uu where
 268 --   iga_swap      = undefined
 269 --
 270 -- instance IGArrow g (**) u gg (***) uu => GArrowLoop g (**) u gg (***) uu where
 271 --   iga_loopr    = undefined
 272 --   iga_loopl    = undefined
 273 --
 274 -- instance IGArrow g (**) u gg (***) uu => GArrowLiteral g (**) u gg (***) uu t r where
 275 --   iga_literal  = undefined
 276 --
 277 -- instance IGArrow g (**) u gg (***) uu => GArrowEval g (**) u gg (***) uu r t where
 278 --   iga_eval      = undefined
 279 --
 280 -- instance IGArrow g (**) u gg (***) uu => GArrowConstant g (**) u gg (***) uu t r where
 281 --   iga_constant  = undefined
 282 --
 283 -- instance IGArrow g (**) u gg (***) uu => GArrowReify g (**) u gg (***) uu x y r q where
 284 --   iga_reify     = undefined
 285 --
 286 -- instance IGArrow g (**) u gg (***) uu => GArrowReflect g (**) u gg (***) uu r q x y where
 287 --   iga_reflect   = undefined
 288
 289
 290 -- | Haskell's function space is self-internal
 291 -- instance SelfInternalGArrow (->) (,) ()
 292
 293 --
 294 --     x , 1->a   |-    b ->c
 295 --    --------------------------   [Kappa]
 296 --     x          |- (a,b)->c
 297 --
 298 -- forall a b c x.
 299 --   (forall g (**) u gg (***) uu .
 300 --     IGArrow g (**) u gg (***) uu =>
 301 --       g (x**(gg uu a)) (gg b c))
 302 --   ->
 303 --   (forall g (**) u gg (***) uu .
 304 --     IGArrow g (**) u gg (***) uu =>
 305 --       g x (gg (a***b) c))
 306 -}