GHC/HetMet/GArrow.hs

   1 {-# LANGUAGE MultiParamTypeClasses, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts #-}
   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   GArrowSTKC(..),
  38   GArrowSTKCL(..),
  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_loopr    :: g (x**z) (y**z) -> g x y
 111   ga_loopl    :: 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
 139 ------------------------------------------------------------------------
 140 -- Reify and Reflect, which are "curried" versions of eval/const
 141
 142 -- If you have this for R the identity map on types, you're basically
 143 -- a Control.Arrow; you can also define essentially all the other
 144 -- methods of GArrow, GArrowDrop, GArrowCopy, etc in terms of this.
 145 class GArrow g (**) u => GArrowReify g (**) u x y r q where
 146   ga_reify     :: (x -> y) -> g r q
 147
 148 class GArrow g (**) u => GArrowReflect g (**) u r q x y where
 149   ga_reflect   :: g r q -> (x -> y)
 150
 151
 152
 153
 154
 155 ------------------------------------------------------------------------
 156 -- Apply and Curry
 157
 158 class GArrow g (**) u => GArrowApply g (**) u (~>) where
 159   ga_applyl    :: g (x**(x~>y)   ) y
 160   ga_applyr    :: g (   (x~>y)**x) y
 161
 162 class GArrow g (**) u => GArrowCurry g (**) u (~>) where
 163   ga_curryl    :: g (x**y) z  ->  g x (y~>z)
 164   ga_curryr    :: g (x**y) z  ->  g y (x~>z)
 165
 166
 167
 168
 169
 170 ------------------------------------------------------------------------
 171 -- Type Families
 172
 173 --
 174 -- The GArrow and GArrow{Copy,Drop,Swap} classes brandish their tensor
 175 -- and unit types; this is important because we might want to have
 176 -- both "instance GArrow g X Y" and "instance GArrow g Z Q" -- in
 177 -- fact, this is exactly how sums and pairs are defined.
 178 --
 179 -- However, in daily practice it's a pain to have all those extra type
 180 -- variables floating around.  If you'd like to hide them, you can use
 181 -- the type families below to do so; see the definition of class
 182 -- GArrowSTKC for an example.  Keep in mind, however, that any given
 183 -- type may only have a single instance declared using the type
 184 -- families.
 185 --
 186
 187 type family GArrowTensor   g :: * -> * -> *   -- (**)
 188 type family GArrowUnit     g :: *             -- ()
 189 type family GArrowExponent g :: * -> * -> *   -- (~>)
 190
 191
 192
 193
 194 ------------------------------------------------------------------------
 195 -- Commonly Implemented Collections of Classes
 196
 197 --
 198 -- The simply typed KAPPA calculus; see Hasegawa, __Decomposing Typed
 199 -- Lambda Calculus into a Couple of Categorical Programming
 200 -- Languages__, http://dx.doi.org/10.1007/3-540-60164-3_28
 201 --
 202
 203 class (GArrowDrop  g (GArrowTensor g) (GArrowUnit g),
 204        GArrowCopy  g (GArrowTensor g) (GArrowUnit g),
 205        GArrowSwap  g (GArrowTensor g) (GArrowUnit g)) =>
 206        GArrowSTKC  g
 207
 208 class (GArrowDrop  g (GArrowTensor g) (GArrowUnit g),
 209        GArrowCopy  g (GArrowTensor g) (GArrowUnit g),
 210        GArrowSwap  g (GArrowTensor g) (GArrowUnit g),
 211        GArrowLoop  g (GArrowTensor g) (GArrowUnit g)) =>
 212        GArrowSTKCL  g
 213
 214 -- The simply typed LAMBDA calculus
 215 class (GArrowDrop  g (GArrowTensor g) (GArrowUnit g),
 216        GArrowCopy  g (GArrowTensor g) (GArrowUnit g),
 217        GArrowSwap  g (GArrowTensor g) (GArrowUnit g),
 218        GArrowCurry g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
 219        GArrowApply g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g)
 220        ) =>
 221        GArrowSTLC  g
 222
 223 -- Programming Language for Computable Functions (w/o integers and booleans)
 224 class (GArrowDrop  g (GArrowTensor g) (GArrowUnit g),
 225        GArrowCopy  g (GArrowTensor g) (GArrowUnit g),
 226        GArrowSwap  g (GArrowTensor g) (GArrowUnit g),
 227        GArrowCurry g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
 228        GArrowApply g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
 229        GArrowLoop  g (GArrowTensor g) (GArrowUnit g)
 230       ) =>
 231       GArrowPCF   g (**) u (~>)
 232
 233
 234
 235
 236
 237 ------------------------------------------------------------------------
 238 -- Experimental, Not Yet Exported
 239
 240 -- See Lindley, Wadler, and Yallop '08 -- except that here ga_force
 241 -- is primitive since there is no "arr" to define it in terms of.
 242 class GArrow g (**) u => GArrowStatic g (**) u (~>) where
 243   ga_delay :: g a b      -> g u (a~>b)
 244   ga_force :: g u (a~>b) -> g a b
 245   -- "ga_static/force_delay"   forall a . force (delay a) = a
 246   -- "ga_static/delay_force"   forall a . delay (force a) = a
 247