GHC/HetMet/GArrow.hs

   1 {-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies #-}
   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   GArrowKappa(..),
  34   GArrowSTKC(..),
  35   GArrowSTLC(..),
  36   GArrowPCF(..)
  37
  38 ) where
  39 import Control.Category hiding ((.))
  40 import Prelude          hiding (id)
  41
  42 ------------------------------------------------------------------------
  43 -- The main GArrow class
  44
  45 class Category g => GArrow g (**) u | (**) -> u, u -> (**) where
  46 --id           :: g x x
  47 --comp         :: g x y -> g y z -> g x z
  48   ga_first     :: g x y -> g (x ** z) (y ** z)
  49   ga_second    :: g x y -> g (z ** x) (z ** y)
  50   ga_cancell   :: g (u**x)         x
  51   ga_cancelr   :: g    (x**u)      x
  52   ga_uncancell :: g     x      (u**x)
  53   ga_uncancelr :: g     x         (x**u)
  54   ga_assoc     :: g ((x** y)**z ) ( x**(y **z))
  55   ga_unassoc   :: g ( x**(y **z)) ((x** y)**z )
  56
  57
  58 ------------------------------------------------------------------------
  59 -- The three context-manipulation classes
  60
  61 class GArrow g (**) u => GArrowCopy g (**) u where
  62   ga_copy      :: g x (x**x)
  63
  64 class GArrow g (**) u => GArrowDrop g (**) u where
  65   ga_drop      :: g x u
  66
  67 class GArrow g (**) u => GArrowSwap g (**) u where
  68   ga_swap      :: g (x**y) (y**x)
  69
  70 ga_swap_second f =
  71    ga_swap >>> ga_first f >>> ga_swap
  72    -- implementation of ga_second for GArrowSwap
  73    -- See also
  74    -- http://haskell.org/haskellwiki/Class_system_extension_proposal
  75    -- "Allowing superclass methods to be overridden in derived classes";
  76    -- if we had this we could do a better job here
  77
  78
  79
  80 ------------------------------------------------------------------------
  81 -- Products, Coproducts, etc
  82
  83
  84 class (GArrowDrop g (<*>) u,
  85        GArrowCopy g (<*>) u) =>
  86        GArrowProd g (<*>) u
  87
  88 class GArrow     g (<+>) u =>
  89       GArrowSum  g (<+>) u where
  90   ga_merge :: g (x<+>x) x
  91   ga_never :: g u       x
  92
  93 ga_inl :: GArrowSum g (<+>) u => g x (x<+>y)
  94 ga_inl = ga_uncancelr >>> ga_second ga_never
  95
  96 ga_inr :: GArrowSum g (<+>) u => g x (y<+>x)
  97 ga_inr = ga_uncancell >>> ga_first  ga_never
  98
  99
 100 ------------------------------------------------------------------------
 101 -- Loop
 102
 103 class GArrow g (**) u => GArrowLoop g (**) u where
 104   ga_loopl    :: g (x**z) (y**z) -> g x y
 105   ga_loopr    :: g (z**x) (z**y) -> g x y
 106
 107
 108 ------------------------------------------------------------------------
 109 -- Literal.  Note that ga_literal should never appear in (unflattened)
 110 -- Haskell programs, though the user may wish to write implementations
 111 -- of this function (I haven't yet found a way to enforce this
 112 -- restriction using exports)
 113
 114 class GArrow g (**) u => GArrowLiteral g (**) u t r where
 115   ga_literal  :: t -> g u r
 116
 117
 118
 119
 120 ------------------------------------------------------------------------
 121 -- Constant and Run, which are dual to each other
 122
 123 class GArrow g (**) u => GArrowEval g (**) u r t where
 124   ga_eval      :: g u r -> t
 125
 126 class GArrow g (**) u => GArrowConstant g (**) u t r where
 127   ga_constant  :: t -> g u r
 128
 129
 130
 131 ------------------------------------------------------------------------
 132 -- Reify and Reflect, which are "curried" versions of eval/const
 133
 134 -- If you have this for R the identity map on types, you're basically
 135 -- a Control.Arrow; you can also define essentially all the other
 136 -- methods of GArrow, GArrowDrop, GArrowCopy, etc in terms of this.
 137 class GArrow g (**) u => GArrowReify g (**) u x y r q where
 138   ga_reify     :: (x -> y) -> g r q
 139
 140 class GArrow g (**) u => GArrowReflect g (**) u r q x y where
 141   ga_reflect   :: g r q -> (x -> y)
 142
 143
 144
 145
 146 ------------------------------------------------------------------------
 147 -- The Kappa adjunction
 148 --
 149 -- See Hasegawa, Decomposing Typed Lambda Calculus into a Couple of
 150 -- Categorical Programming Languages) section 3, rule $(\times L)$
 151
 152 class GArrow g (**) u => GArrowKappa g (**) u where
 153   ga_kappa :: (g u x -> g u y) -> g x y
 154
 155
 156
 157
 158
 159 ------------------------------------------------------------------------
 160 -- Apply and Curry
 161
 162 class GArrow g (**) u => GArrowApply g (**) u (~>) where
 163   ga_applyl    :: g (x**(x~>y)   ) y
 164   ga_applyr    :: g (   (x~>y)**x) y
 165
 166 class GArrow g (**) u => GArrowCurry g (**) u (~>) where
 167   ga_curryl    :: g (x**y) z  ->  g x (y~>z)
 168   ga_curryr    :: g (x**y) z  ->  g y (x~>z)
 169
 170
 171
 172
 173 ------------------------------------------------------------------------
 174 -- Commonly Implemented Collections of Classes
 175
 176 --
 177 -- The simply typed KAPPA calculus; see Hasegawa, __Decomposing Typed
 178 -- Lambda Calculus into a Couple of Categorical Programming
 179 -- Languages__, http://dx.doi.org/10.1007/3-540-60164-3_28
 180 --
 181 class (GArrowDrop  g (**) u,
 182        GArrowCopy  g (**) u,
 183        GArrowSwap  g (**) u) =>
 184        GArrowSTKC  g (**) u
 185
 186 -- The simply typed LAMBDA calculus
 187 class (GArrowSTKC  g (**) u,
 188        GArrowCurry g (**) u (~>),
 189        GArrowApply g (**) u (~>)) =>
 190        GArrowSTLC  g (**) u (~>)
 191
 192 -- Programming Language for Computable Functions (w/o integers and booleans)
 193 class (GArrowSTLC  g (**) u (~>),
 194        GArrowLoop  g (**) u) =>
 195        GArrowPCF   g (**) u (~>)
 196
 197
 198
 199
 200
 201 ------------------------------------------------------------------------
 202 -- Experimental, Not Yet Exported
 203
 204 -- See Lindley, Wadler, and Yallop '08 -- except that here ga_force
 205 -- is primitive since there is no "arr" to define it in terms of.
 206 class GArrow g (**) u => GArrowStatic g (**) u (~>) where
 207   ga_delay :: g a b      -> g u (a~>b)
 208   ga_force :: g u (a~>b) -> g a b
 209   -- "ga_static/force_delay"   forall a . force (delay a) = a
 210   -- "ga_static/delay_force"   forall a . delay (force a) = a
 211