GHC/HetMet/GArrow.hs

   1 {-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies -XTypeFamilies -XFlexibleContexts #-}
   2 -----------------------------------------------------------------------------
   3 -- |
   4 -- Module      :  GHC.HetMet.GArrow
   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.GArrow (
  13   GArrow(..),
  14   GArrowDrop(..),
  15   GArrowCopy(..),
  16   GArrowSwap(..),
  17
  18   GArrowLoop(..),
  19
  20   GArrowEval(..),
  21   GArrowConstant(..),
  22   GArrowLiteral(..),   -- should be implemented, but never invoked, by user code
  23
  24   GArrowSum(..),  ga_inl, ga_inr,
  25   GArrowProd(..),
  26
  27   GArrowReify(..),
  28   GArrowReflect(..),
  29
  30   GArrowCurry(..),
  31   GArrowApply(..),
  32
  33   GArrowTensor,
  34   GArrowUnit,
  35   GArrowExponent,
  36
  37   GArrowKappa(..),
  38   GArrowSTKC(..),
  39   GArrowSTKCL(..),
  40   GArrowSTLC(..),
  41   GArrowPCF(..)
  42
  43 ) where
  44 import Control.Category hiding ((.))
  45 import Prelude          hiding (id)
  46
  47 ------------------------------------------------------------------------
  48 -- The main GArrow class
  49
  50 class Category g => GArrow g (**) u | (**) -> u, u -> (**) where
  51 --id           :: g x x
  52 --comp         :: g x y -> g y z -> g x z
  53   ga_first     :: g x y -> g (x ** z) (y ** z)
  54   ga_second    :: g x y -> g (z ** x) (z ** y)
  55   ga_cancell   :: g (u**x)         x
  56   ga_cancelr   :: g    (x**u)      x
  57   ga_uncancell :: g     x      (u**x)
  58   ga_uncancelr :: g     x         (x**u)
  59   ga_assoc     :: g ((x** y)**z ) ( x**(y **z))
  60   ga_unassoc   :: g ( x**(y **z)) ((x** y)**z )
  61
  62
  63 ------------------------------------------------------------------------
  64 -- The three context-manipulation classes
  65
  66 class GArrow g (**) u => GArrowCopy g (**) u where
  67   ga_copy      :: g x (x**x)
  68
  69 class GArrow g (**) u => GArrowDrop g (**) u where
  70   ga_drop      :: g x u
  71
  72 class GArrow g (**) u => GArrowSwap g (**) u where
  73   ga_swap      :: g (x**y) (y**x)
  74
  75 ga_swap_second f =
  76    ga_swap >>> ga_first f >>> ga_swap
  77    -- implementation of ga_second for GArrowSwap
  78    -- See also
  79    -- http://haskell.org/haskellwiki/Class_system_extension_proposal
  80    -- "Allowing superclass methods to be overridden in derived classes";
  81    -- if we had this we could do a better job here
  82
  83
  84
  85
  86
  87 ------------------------------------------------------------------------
  88 -- Products, Coproducts, etc
  89
  90
  91 class (GArrowDrop g (<*>) u,
  92        GArrowCopy g (<*>) u) =>
  93        GArrowProd g (<*>) u
  94
  95 class GArrow     g (<+>) u =>
  96       GArrowSum  g (<+>) u where
  97   ga_merge :: g (x<+>x) x
  98   ga_never :: g u       x
  99
 100 ga_inl :: GArrowSum g (<+>) u => g x (x<+>y)
 101 ga_inl = ga_uncancelr >>> ga_second ga_never
 102
 103 ga_inr :: GArrowSum g (<+>) u => g x (y<+>x)
 104 ga_inr = ga_uncancell >>> ga_first  ga_never
 105
 106
 107 ------------------------------------------------------------------------
 108 -- Loop
 109
 110 class GArrow g (**) u => GArrowLoop g (**) u where
 111   ga_loopr    :: g (x**z) (y**z) -> g x y
 112   ga_loopl    :: g (z**x) (z**y) -> g x y
 113
 114
 115 ------------------------------------------------------------------------
 116 -- Literal.  Note that ga_literal should never appear in (unflattened)
 117 -- Haskell programs, though the user may wish to write implementations
 118 -- of this function (I haven't yet found a way to enforce this
 119 -- restriction using exports)
 120
 121 class GArrow g (**) u => GArrowLiteral g (**) u t r where
 122   ga_literal  :: t -> g u r
 123
 124
 125
 126
 127 ------------------------------------------------------------------------
 128 -- Constant and Run, which are dual to each other
 129
 130 class GArrow g (**) u => GArrowEval g (**) u r t where
 131   ga_eval      :: g u r -> t
 132
 133 class GArrow g (**) u => GArrowConstant g (**) u t r where
 134   ga_constant  :: t -> g u r
 135
 136
 137
 138 ------------------------------------------------------------------------
 139 -- Reify and Reflect, which are "curried" versions of eval/const
 140
 141 -- If you have this for R the identity map on types, you're basically
 142 -- a Control.Arrow; you can also define essentially all the other
 143 -- methods of GArrow, GArrowDrop, GArrowCopy, etc in terms of this.
 144 class GArrow g (**) u => GArrowReify g (**) u x y r q where
 145   ga_reify     :: (x -> y) -> g r q
 146
 147 class GArrow g (**) u => GArrowReflect g (**) u r q x y where
 148   ga_reflect   :: g r q -> (x -> y)
 149
 150
 151
 152
 153 ------------------------------------------------------------------------
 154 -- The Kappa adjunction
 155 --
 156 -- See Hasegawa, Decomposing Typed Lambda Calculus into a Couple of
 157 -- Categorical Programming Languages) section 3, rule $(\times L)$
 158
 159 class GArrow g (**) u => GArrowKappa g (**) u where
 160   ga_kappa :: (g u x -> g u y) -> g x y
 161
 162
 163
 164
 165
 166 ------------------------------------------------------------------------
 167 -- Apply and Curry
 168
 169 class GArrow g (**) u => GArrowApply g (**) u (~>) where
 170   ga_applyl    :: g (x**(x~>y)   ) y
 171   ga_applyr    :: g (   (x~>y)**x) y
 172
 173 class GArrow g (**) u => GArrowCurry g (**) u (~>) where
 174   ga_curryl    :: g (x**y) z  ->  g x (y~>z)
 175   ga_curryr    :: g (x**y) z  ->  g y (x~>z)
 176
 177
 178
 179
 180
 181 ------------------------------------------------------------------------
 182 -- Type Families
 183
 184 --
 185 -- The GArrow and GArrow{Copy,Drop,Swap} classes brandish their tensor
 186 -- and unit types; this is important because we might want to have
 187 -- both "instance GArrow g X Y" and "instance GArrow g Z Q" -- in
 188 -- fact, this is exactly how sums and pairs are defined.
 189 --
 190 -- However, in daily practice it's a pain to have all those extra type
 191 -- variables floating around.  If you'd like to hide them, you can use
 192 -- the type families below to do so; see the definition of class
 193 -- GArrowSTKC for an example.  Keep in mind, however, that any given
 194 -- type may only have a single instance declared using the type
 195 -- families.
 196 --
 197
 198 type family GArrowTensor   g :: * -> * -> *   -- (**)
 199 type family GArrowUnit     g :: *             -- ()
 200 type family GArrowExponent g :: * -> * -> *   -- (~>)
 201
 202
 203
 204
 205 ------------------------------------------------------------------------
 206 -- Commonly Implemented Collections of Classes
 207
 208 --
 209 -- The simply typed KAPPA calculus; see Hasegawa, __Decomposing Typed
 210 -- Lambda Calculus into a Couple of Categorical Programming
 211 -- Languages__, http://dx.doi.org/10.1007/3-540-60164-3_28
 212 --
 213
 214 class (GArrowDrop  g (GArrowTensor g) (GArrowUnit g),
 215        GArrowCopy  g (GArrowTensor g) (GArrowUnit g),
 216        GArrowSwap  g (GArrowTensor g) (GArrowUnit g)) =>
 217        GArrowSTKC  g
 218
 219 class (GArrowDrop  g (GArrowTensor g) (GArrowUnit g),
 220        GArrowCopy  g (GArrowTensor g) (GArrowUnit g),
 221        GArrowSwap  g (GArrowTensor g) (GArrowUnit g),
 222        GArrowLoop  g (GArrowTensor g) (GArrowUnit g)) =>
 223        GArrowSTKCL  g
 224
 225 -- The simply typed LAMBDA calculus
 226 class (GArrowDrop  g (GArrowTensor g) (GArrowUnit g),
 227        GArrowCopy  g (GArrowTensor g) (GArrowUnit g),
 228        GArrowSwap  g (GArrowTensor g) (GArrowUnit g),
 229        GArrowCurry g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
 230        GArrowApply g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g)
 231        ) =>
 232        GArrowSTLC  g
 233
 234 -- Programming Language for Computable Functions (w/o integers and booleans)
 235 class (GArrowDrop  g (GArrowTensor g) (GArrowUnit g),
 236        GArrowCopy  g (GArrowTensor g) (GArrowUnit g),
 237        GArrowSwap  g (GArrowTensor g) (GArrowUnit g),
 238        GArrowCurry g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
 239        GArrowApply g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
 240        GArrowLoop  g (GArrowTensor g) (GArrowUnit g)
 241       ) =>
 242       GArrowPCF   g (**) u (~>)
 243
 244
 245
 246
 247
 248 ------------------------------------------------------------------------
 249 -- Experimental, Not Yet Exported
 250
 251 -- See Lindley, Wadler, and Yallop '08 -- except that here ga_force
 252 -- is primitive since there is no "arr" to define it in terms of.
 253 class GArrow g (**) u => GArrowStatic g (**) u (~>) where
 254   ga_delay :: g a b      -> g u (a~>b)
 255   ga_force :: g u (a~>b) -> g a b
 256   -- "ga_static/force_delay"   forall a . force (delay a) = a
 257   -- "ga_static/delay_force"   forall a . delay (force a) = a
 258