GHC/HetMet/IGArrow.hs

   1 {-# LANGUAGE RankNTypes, MultiParamTypeClasses, TypeOperators, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
   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.GArrowFullyEnriched
  33 import Prelude          hiding (id, (.))
  34
  35 --
  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
  39 -- GHC.HetMet.Arrow.
  40 --
  41 --import GHC.HetMet.Arrow
  42
  43
  44
  45
  46 ------------------------------------------------------------------------
  47 -- Internal GArrows
  48 --
  49 -- | An "internal generalized arrow" is a GArrow except that it uses
  50 -- some *other* GArrow in place of Haskell's function space.
  51 --
  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 ))
  63
  64 class IGArrow g (**) u gg (***) uu => IGArrowCopy g (**) u gg (***) uu where
  65   iga_copy      :: g u (gg x (x***x))
  66
  67 class IGArrow g (**) u gg (***) uu => IGArrowDrop g (**) u gg (***) uu where
  68   iga_drop      :: g u (gg x uu)
  69
  70 class IGArrow g (**) u gg (***) uu => IGArrowSwap g (**) u gg (***) uu where
  71   iga_swap      :: g u (gg (x***y) (y***x))
  72
  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)
  76
  77 class IGArrow g (**) u gg (***) uu => IGArrowLiteral g (**) u gg (***) uu t r where
  78   iga_literal  :: g t (gg uu r)
  79
  80 class IGArrow g (**) u gg (***) uu => IGArrowEval g (**) u gg (***) uu r t where
  81   iga_eval      :: g (gg uu r) t
  82
  83 class IGArrow g (**) u gg (***) uu => IGArrowConstant g (**) u gg (***) uu t r where
  84   iga_constant  :: g t (gg uu r)
  85
  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)
  88
  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)
  91
  92
  93
  94 ------------------------------------------------------------------------
  95 -- Externalization
  96 --
  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.
 100 --
 101 -- TODO: I should be one level deeper here: assuming an (IGArrow
 102 -- (IGArrow g)), create an (IGArrow g).
 103 --
 104
 105 newtype Ex g x y = Ex (g x y)
 106
 107 --
 108 -- | Every IGArrow of (->) is a GArrow
 109 --
 110 instance IGArrow (->) (,) () g (**) u => Category (Ex g) where
 111   id                = Ex (iga_id ())
 112   (Ex g) . (Ex f) = Ex (iga_comp (f,g))
 113
 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 ()
 123
 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 ()
 130
 131
 132
 133
 134
 135 ------------------------------------------------------------------------
 136 -- Internalization
 137 --
 138 -- | Every GArrow is internal to the GArrow instance on (->)
 139 --
 140
 141 newtype In g x y = In (g x y)
 142
 143 instance (GArrow (->) (,) (), GArrow g (**) u) => IGArrow (->) (,) () (In g) (**) u where
 144   iga_id        _           = In $ id
 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
 160
 161
 162
 163
 164
 165 ------------------------------------------------------------------------
 166 -- Kappa
 167 --
 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.
 172 --
 173 --         x , 1->a   |-    b ->c
 174 --        --------------------------   [Kappa]
 175 --         x          |- (a,b)->c
 176 --
 177 --
 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) =>
 187                g u (gg (a***b) c))
 188   -- TO DO: change the above to iga_kappal, add iga_kappar
 189
 190 --
 191 -- | The (->) GArrow has the Kappa property.
 192 --
 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
 195
 196
 197
 198
 199
 200
 201 ------------------------------------------------------------------------------
 202 -- Self-Internal GArrows
 203
 204 --
 205 -- | A self-internal GArrow is, well, internal to itself
 206 --
 207 class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
 208
 209 --
 210 -- | Self-internal GArrows have curry/apply
 211 --
 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"
 215
 216 --
 217 -- | Self-internal GArrows have curry/apply
 218 --
 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"
 222
 223 --
 224 -- | Haskell's function space is self-internal
 225 --
 226 instance GArrow (->) (,) () => IGArrow (->) (,) () (->) (,) () where
 227   iga_id        _ = id
 228   iga_comp  (f,g) = f >>> g
 229   iga_first       = ga_first
 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
 237
 238 --instance GArrow (->) (,) () => SelfInternalGArrow (->) (,) ()