1 {-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies #-}
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,
39 import Control.Category hiding ((.))
40 import Prelude hiding (id)
42 ------------------------------------------------------------------------
43 -- The main GArrow class
45 class Category g => GArrow g (**) u | (**) -> u, u -> (**) where
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 )
58 ------------------------------------------------------------------------
59 -- The three context-manipulation classes
61 class GArrow g (**) u => GArrowCopy g (**) u where
64 class GArrow g (**) u => GArrowDrop g (**) u where
67 class GArrow g (**) u => GArrowSwap g (**) u where
68 ga_swap :: g (x**y) (y**x)
71 ga_swap >>> ga_first f >>> ga_swap
72 -- implementation of ga_second for GArrowSwap
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
80 ------------------------------------------------------------------------
81 -- Products, Coproducts, etc
84 class (GArrowDrop g (<*>) u,
85 GArrowCopy g (<*>) u) =>
88 class GArrow g (<+>) u =>
89 GArrowSum g (<+>) u where
90 ga_merge :: g (x<+>x) x
93 ga_inl :: GArrowSum g (<+>) u => g x (x<+>y)
94 ga_inl = ga_uncancelr >>> ga_second ga_never
96 ga_inr :: GArrowSum g (<+>) u => g x (y<+>x)
97 ga_inr = ga_uncancell >>> ga_first ga_never
100 ------------------------------------------------------------------------
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
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)
114 class GArrow g (**) u => GArrowLiteral g (**) u t r where
115 ga_literal :: t -> g u r
120 ------------------------------------------------------------------------
121 -- Constant and Run, which are dual to each other
123 class GArrow g (**) u => GArrowEval g (**) u r t where
124 ga_eval :: g u r -> t
126 class GArrow g (**) u => GArrowConstant g (**) u t r where
127 ga_constant :: t -> g u r
131 ------------------------------------------------------------------------
132 -- Reify and Reflect, which are "curried" versions of eval/const
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
140 class GArrow g (**) u => GArrowReflect g (**) u r q x y where
141 ga_reflect :: g r q -> (x -> y)
146 ------------------------------------------------------------------------
147 -- The Kappa adjunction
149 -- See Hasegawa, Decomposing Typed Lambda Calculus into a Couple of
150 -- Categorical Programming Languages) section 3, rule $(\times L)$
152 class GArrow g (**) u => GArrowKappa g (**) u where
153 ga_kappa :: (g u x -> g u y) -> g x y
159 ------------------------------------------------------------------------
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
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)
173 ------------------------------------------------------------------------
174 -- Commonly Implemented Collections of Classes
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
181 class (GArrowDrop g (**) u,
183 GArrowSwap g (**) u) =>
186 -- The simply typed LAMBDA calculus
187 class (GArrowSTKC g (**) u,
188 GArrowCurry g (**) u (~>),
189 GArrowApply g (**) u (~>)) =>
190 GArrowSTLC g (**) u (~>)
192 -- Programming Language for Computable Functions (w/o integers and booleans)
193 class (GArrowSTLC g (**) u (~>),
194 GArrowLoop g (**) u) =>
195 GArrowPCF g (**) u (~>)
201 ------------------------------------------------------------------------
202 -- Experimental, Not Yet Exported
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