1 {-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies -XTypeFamilies -XFlexibleContexts #-}
2 -----------------------------------------------------------------------------
4 -- Module : GHC.HetMet.GArrow
6 -- License : public domain
8 -- Maintainer : Adam Megacz <megacz@acm.org>
9 -- Stability : experimental
10 -- Portability : portable
12 module GHC.HetMet.GArrow (
22 GArrowLiteral(..), -- should be implemented, but never invoked, by user code
24 GArrowSum(..), ga_inl, ga_inr,
44 import Control.Category hiding ((.))
45 import Prelude hiding (id)
47 ------------------------------------------------------------------------
48 -- The main GArrow class
50 class Category g => GArrow g (**) u | (**) -> u, u -> (**) where
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 )
63 ------------------------------------------------------------------------
64 -- The three context-manipulation classes
66 class GArrow g (**) u => GArrowCopy g (**) u where
69 class GArrow g (**) u => GArrowDrop g (**) u where
72 class GArrow g (**) u => GArrowSwap g (**) u where
73 ga_swap :: g (x**y) (y**x)
76 ga_swap >>> ga_first f >>> ga_swap
77 -- implementation of ga_second for GArrowSwap
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
87 ------------------------------------------------------------------------
88 -- Products, Coproducts, etc
91 class (GArrowDrop g (<*>) u,
92 GArrowCopy g (<*>) u) =>
95 class GArrow g (<+>) u =>
96 GArrowSum g (<+>) u where
97 ga_merge :: g (x<+>x) x
100 ga_inl :: GArrowSum g (<+>) u => g x (x<+>y)
101 ga_inl = ga_uncancelr >>> ga_second ga_never
103 ga_inr :: GArrowSum g (<+>) u => g x (y<+>x)
104 ga_inr = ga_uncancell >>> ga_first ga_never
107 ------------------------------------------------------------------------
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
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)
121 class GArrow g (**) u => GArrowLiteral g (**) u t r where
122 ga_literal :: t -> g u r
127 ------------------------------------------------------------------------
128 -- Constant and Run, which are dual to each other
130 class GArrow g (**) u => GArrowEval g (**) u r t where
131 ga_eval :: g u r -> t
133 class GArrow g (**) u => GArrowConstant g (**) u t r where
134 ga_constant :: t -> g u r
138 ------------------------------------------------------------------------
139 -- Reify and Reflect, which are "curried" versions of eval/const
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
147 class GArrow g (**) u => GArrowReflect g (**) u r q x y where
148 ga_reflect :: g r q -> (x -> y)
153 ------------------------------------------------------------------------
154 -- The Kappa adjunction
156 -- See Hasegawa, Decomposing Typed Lambda Calculus into a Couple of
157 -- Categorical Programming Languages) section 3, rule $(\times L)$
159 class GArrow g (**) u => GArrowKappa g (**) u where
160 ga_kappa :: (g u x -> g u y) -> g x y
166 ------------------------------------------------------------------------
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
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)
181 ------------------------------------------------------------------------
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.
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
198 type family GArrowTensor g :: * -> * -> * -- (**)
199 type family GArrowUnit g :: * -- ()
200 type family GArrowExponent g :: * -> * -> * -- (~>)
205 ------------------------------------------------------------------------
206 -- Commonly Implemented Collections of Classes
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
214 class (GArrowDrop g (GArrowTensor g) (GArrowUnit g),
215 GArrowCopy g (GArrowTensor g) (GArrowUnit g),
216 GArrowSwap g (GArrowTensor g) (GArrowUnit g)) =>
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)) =>
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)
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)
242 GArrowPCF g (**) u (~>)
248 ------------------------------------------------------------------------
249 -- Experimental, Not Yet Exported
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