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