GHC/HetMet/IGArrow.hs

   1 {-# LANGUAGE RankNTypes, MultiParamTypeClasses, NoMonomorphismRestriction, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts, FlexibleInstances, DatatypeContexts #-}
   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 hiding ((.))
  31 import GHC.HetMet.GArrow
  32 import Prelude          hiding (id)
  33 import GHC.HetMet.Arrow
  34
  35
  36
  37
  38
  39 ------------------------------------------------------------------------
  40 -- Internal GArrows
  41 --
  42 -- | An "internal generalized arrow" is a GArrow except that it uses
  43 -- some *other* GArrow in place of Haskell's function space.
  44 --
  45 class IGArrow g (**) u gg (***) uu where
  46   iga_id        :: g u (gg x x)
  47   iga_comp      :: g ((gg x y) ** (gg y z)) (gg x z)
  48   iga_first     :: g (gg x y) (gg (x *** z) (y *** z))
  49   iga_second    :: g (gg x y) (gg (z *** x) (z *** y))
  50   iga_cancell   :: g u (gg (uu***x)         x)
  51   iga_cancelr   :: g u (gg    (x***uu)      x)
  52   iga_uncancell :: g u (gg     x      (uu***x))
  53   iga_uncancelr :: g u (gg     x         (x***uu))
  54   iga_assoc     :: g u (gg ((x*** y)***z ) ( x***(y ***z)))
  55   iga_unassoc   :: g u (gg ( x***(y ***z)) ((x*** y)***z ))
  56
  57 class IGArrow g (**) u gg (***) uu => IGArrowCopy g (**) u gg (***) uu where
  58   iga_copy      :: g u (gg x (x***x))
  59
  60 class IGArrow g (**) u gg (***) uu => IGArrowDrop g (**) u gg (***) uu where
  61   iga_drop      :: g u (gg x u)
  62
  63 class IGArrow g (**) u gg (***) uu => IGArrowSwap g (**) u gg (***) uu where
  64   iga_swap      :: g u (gg (x***y) (y***x))
  65
  66 class IGArrow g (**) u gg (***) uu => IGArrowLoop g (**) u gg (***) uu where
  67   iga_loopr    :: g (gg (x***z) (y***z)) (gg x y)
  68   iga_loopl    :: g (gg (z***x) (z***y)) (gg x y)
  69
  70 class IGArrow g (**) u gg (***) uu => IGArrowLiteral g (**) u gg (***) uu t r where
  71   iga_literal  :: g t (gg uu r)
  72
  73 class IGArrow g (**) u gg (***) uu => IGArrowEval g (**) u gg (***) uu r t where
  74   iga_eval      :: g (gg uu r) t
  75
  76 class IGArrow g (**) u gg (***) uu => IGArrowConstant g (**) u gg (***) uu t r where
  77   iga_constant  :: g t (gg uu r)
  78
  79 class IGArrow g (**) u gg (***) uu => IGArrowReify g (**) u gg (***) uu x y r q where
  80   iga_reify     :: g (g x y) (gg r q)
  81
  82 class IGArrow g (**) u gg (***) uu => IGArrowReflect g (**) u gg (***) uu r q x y where
  83   iga_reflect   :: g (gg r q) (g x y)
  84
  85
  86
  87
  88
  89 ------------------------------------------------------------------------------
  90 -- Self-Internal GArrows
  91
  92 --
  93 -- | A self-internal GArrow is, well, internal to itself
  94 --
  95 class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
  96
  97 --
  98 -- | Self-internal GArrows have curry/apply
  99 --
 100 -- instance SelfInternalGArrow g (**) u => GArrowApply g (**) u gg where
 101 --   ga_applyl =    :: g (x**(g x y)   ) y
 102 --   ga_applyr    :: g (   (g x y)**x) y
 103 --
 104 --
 105 -- | Self-internal GArrows have curry/apply
 106 --
 107 -- instance SelfInternalGArrow g (**) u gg (***) uu => GArrowCurry g (**) u gg where
 108 --   ga_curryl    :: g (x**y) z  ->  g x (g y z)
 109 --   ga_curryr    :: g (x**y) z  ->  g y (g x z)
 110
 111
 112
 113
 114
 115 ------------------------------------------------------------------------------
 116 -- Instances
 117
 118 --
 119 -- | Every GArrow is internal to the GArrow instance on (->)
 120 --
 121 instance GArrow g (**) u => IGArrow (->) (,) () g (**) u where
 122   iga_id        _     = id
 123   iga_comp      (f,g) = f >>> g
 124   iga_first           = ga_first
 125   iga_second          = ga_second
 126   iga_cancell   _     = ga_cancell
 127   iga_cancelr   _     = ga_cancelr
 128   iga_uncancell _     = ga_uncancell
 129   iga_uncancelr _     = ga_uncancelr
 130   iga_assoc     _     = ga_assoc
 131   iga_unassoc   _     = ga_unassoc
 132
 133
 134
 135
 136
 137
 138 ------------------------------------------------------------------------
 139 -- Externalization
 140 --
 141 -- | An IGArrow may be "externalized" to form a normal generalized
 142 -- arrow.  If the IGArrow was an instance of class IGArrowXX, the
 143 -- externalization will be an instance of GArrowYY.
 144 --
 145 -- TODO: I should be one level deeper here: assuming an (IGArrow
 146 -- (IGArrow g)), create an (IGArrow g).
 147 --
 148
 149 newtype
 150     IGArrow g (**) u q (***) uu =>
 151     Ext g (**) u q (***) uu x y
 152     = Ext { unExt :: g u (q x y) }
 153
 154 -- instance IGArrow g (**) u gg (***) uu => GArrowCopy g (**) u gg (***) uu where
 155 --   iga_copy      = undefined
 156 --
 157 -- instance IGArrow g (**) u gg (***) uu => GArrowDrop g (**) u gg (***) uu where
 158 --   iga_drop      = undefined
 159 --
 160 -- instance IGArrow g (**) u gg (***) uu => GArrowSwap g (**) u gg (***) uu where
 161 --   iga_swap      = undefined
 162 --
 163 -- instance IGArrow g (**) u gg (***) uu => GArrowLoop g (**) u gg (***) uu where
 164 --   iga_loopr    = undefined
 165 --   iga_loopl    = undefined
 166 --
 167 -- instance IGArrow g (**) u gg (***) uu => GArrowLiteral g (**) u gg (***) uu t r where
 168 --   iga_literal  = undefined
 169 --
 170 -- instance IGArrow g (**) u gg (***) uu => GArrowEval g (**) u gg (***) uu r t where
 171 --   iga_eval      = undefined
 172 --
 173 -- instance IGArrow g (**) u gg (***) uu => GArrowConstant g (**) u gg (***) uu t r where
 174 --   iga_constant  = undefined
 175 --
 176 -- instance IGArrow g (**) u gg (***) uu => GArrowReify g (**) u gg (***) uu x y r q where
 177 --   iga_reify     = undefined
 178 --
 179 -- instance IGArrow g (**) u gg (***) uu => GArrowReflect g (**) u gg (***) uu r q x y where
 180 --   iga_reflect   = undefined