-{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances #-}
+{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies -XTypeFamilies -XFlexibleContexts #-}
-----------------------------------------------------------------------------
-- |
-- Module : GHC.HetMet.GArrow
GArrowDrop(..),
GArrowCopy(..),
GArrowSwap(..),
+
GArrowLoop(..),
+
+ GArrowEval(..),
+ GArrowConstant(..),
+ GArrowLiteral(..), -- should be implemented, but never invoked, by user code
+
+ GArrowSum(..), ga_inl, ga_inr,
+ GArrowProd(..),
+
GArrowReify(..),
- GArrowReflect(..)
+ GArrowReflect(..),
+
+ GArrowCurry(..),
+ GArrowApply(..),
+
+ GArrowTensor,
+ GArrowUnit,
+ GArrowExponent,
+
+ GArrowSTKC(..),
+ GArrowSTKCL(..),
+ GArrowSTLC(..),
+ GArrowPCF(..)
+
) where
-import Control.Arrow
+import Control.Category hiding ((.))
+import Prelude hiding (id)
+
+------------------------------------------------------------------------
+-- The main GArrow class
-class GArrow g (**) where
- ga_id :: g x x
- ga_comp :: g x y -> g y z -> g x z
+class Category g => GArrow g (**) u | (**) -> u, u -> (**) where
+--id :: g x x
+--comp :: g x y -> g y z -> g x z
ga_first :: g x y -> g (x ** z) (y ** z)
ga_second :: g x y -> g (z ** x) (z ** y)
- ga_cancell :: g (()**x) x
- ga_cancelr :: g (x**()) x
- ga_uncancell :: g x (()**x)
- ga_uncancelr :: g x (x**())
- ga_assoc :: g ((x**y)**z) (x**(y**z))
- ga_unassoc :: g (x**(y**z)) ((x**y)**z)
+ ga_cancell :: g (u**x) x
+ ga_cancelr :: g (x**u) x
+ ga_uncancell :: g x (u**x)
+ ga_uncancelr :: g x (x**u)
+ ga_assoc :: g ((x** y)**z ) ( x**(y **z))
+ ga_unassoc :: g ( x**(y **z)) ((x** y)**z )
+
-class GArrow g (**) => GArrowDrop g (**) where
- ga_drop :: g x ()
+------------------------------------------------------------------------
+-- The three context-manipulation classes
-class GArrow g (**) => GArrowCopy g (**) where
+class GArrow g (**) u => GArrowCopy g (**) u where
ga_copy :: g x (x**x)
-class GArrow g (**) => GArrowSwap g (**) where
- ga_swap :: g (x**y) (y**x)
+class GArrow g (**) u => GArrowDrop g (**) u where
+ ga_drop :: g x u
+
+class GArrow g (**) u => GArrowSwap g (**) u where
+ ga_swap :: g (x**y) (y**x)
+
+ga_swap_second f =
+ ga_swap >>> ga_first f >>> ga_swap
+ -- implementation of ga_second for GArrowSwap
+ -- See also
+ -- http://haskell.org/haskellwiki/Class_system_extension_proposal
+ -- "Allowing superclass methods to be overridden in derived classes";
+ -- if we had this we could do a better job here
+
+
+
+
+
+------------------------------------------------------------------------
+-- Products, Coproducts, etc
+
+
+class (GArrowDrop g (<*>) u,
+ GArrowCopy g (<*>) u) =>
+ GArrowProd g (<*>) u
+
+class GArrow g (<+>) u =>
+ GArrowSum g (<+>) u where
+ ga_merge :: g (x<+>x) x
+ ga_never :: g u x
+
+ga_inl :: GArrowSum g (<+>) u => g x (x<+>y)
+ga_inl = ga_uncancelr >>> ga_second ga_never
+
+ga_inr :: GArrowSum g (<+>) u => g x (y<+>x)
+ga_inr = ga_uncancell >>> ga_first ga_never
+
+
+------------------------------------------------------------------------
+-- Loop
+
+class GArrow g (**) u => GArrowLoop g (**) u where
+ ga_loopr :: g (x**z) (y**z) -> g x y
+ ga_loopl :: g (z**x) (z**y) -> g x y
--- implementation of ga_second for GArrowSwap instances
-ga_swap_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
-class GArrow g (**) => GArrowLoop g (**) where
- ga_loop :: g (x**z) (y**z) -> g x y
+------------------------------------------------------------------------
+-- Literal. Note that ga_literal should never appear in (unflattened)
+-- Haskell programs, though the user may wish to write implementations
+-- of this function (I haven't yet found a way to enforce this
+-- restriction using exports)
-class GArrow g (**) => GArrowLiteral g (**) a where
- ga_literal :: a -> g () a
+class GArrow g (**) u => GArrowLiteral g (**) u t r where
+ ga_literal :: t -> g u r
--- not sure -- subject to change
-class GArrow g (**) => GArrowReify g (**) where
- ga_reify :: (x -> y) -> g x y
--- not sure -- subject to change
-class GArrow g (**) => GArrowReflect g (**) where
- ga_reflect :: g x y -> (x -> y)
+------------------------------------------------------------------------
+-- Constant and Run, which are dual to each other
-------------------------------------------------------------------------------
--- GArrow instances for Control.Arrow
+class GArrow g (**) u => GArrowEval g (**) u r t where
+ ga_eval :: g u r -> t
-instance Arrow a => GArrow a (,) where
- ga_id = arr Prelude.id
- ga_comp = (>>>)
- ga_first = first
- ga_second = second
- ga_cancell = arr (\((),x) -> x)
- ga_cancelr = arr (\(x,()) -> x)
- ga_uncancell = arr (\x -> ((),x))
- ga_uncancelr = arr (\x -> (x,()))
- ga_assoc = arr (\((x,y),z) -> (x,(y,z)))
- ga_unassoc = arr (\(x,(y,z)) -> ((x,y),z))
-
-instance Arrow a => GArrowDrop a (,) where
- ga_drop = arr (\x -> ())
+class GArrow g (**) u => GArrowConstant g (**) u t r where
+ ga_constant :: t -> g u r
-instance Arrow a => GArrowCopy a (,) where
- ga_copy = arr (\x -> (x,x))
-instance Arrow a => GArrowSwap a (,) where
- ga_swap = arr (\(x,y) -> (y,x))
-instance Arrow a => GArrowLiteral a (,) where
- ga_literal x = arr (\() -> x)
-instance Arrow a => GArrowReify a (,) where
- ga_reify = arr
-instance ArrowLoop a => GArrowLoop a (,) where
- ga_loop = loop
+------------------------------------------------------------------------
+-- Reify and Reflect, which are "curried" versions of eval/const
+-- If you have this for R the identity map on types, you're basically
+-- a Control.Arrow; you can also define essentially all the other
+-- methods of GArrow, GArrowDrop, GArrowCopy, etc in terms of this.
+class GArrow g (**) u => GArrowReify g (**) u x y r q where
+ ga_reify :: (x -> y) -> g r q
+
+class GArrow g (**) u => GArrowReflect g (**) u r q x y where
+ ga_reflect :: g r q -> (x -> y)
+
+
+
+
+
+------------------------------------------------------------------------
+-- Apply and Curry
+
+class GArrow g (**) u => GArrowApply g (**) u (~>) where
+ ga_applyl :: g (x**(x~>y) ) y
+ ga_applyr :: g ( (x~>y)**x) y
+
+class GArrow g (**) u => GArrowCurry g (**) u (~>) where
+ ga_curryl :: g (x**y) z -> g x (y~>z)
+ ga_curryr :: g (x**y) z -> g y (x~>z)
+
+
+
+
+
+------------------------------------------------------------------------
+-- Type Families
+
+--
+-- The GArrow and GArrow{Copy,Drop,Swap} classes brandish their tensor
+-- and unit types; this is important because we might want to have
+-- both "instance GArrow g X Y" and "instance GArrow g Z Q" -- in
+-- fact, this is exactly how sums and pairs are defined.
+--
+-- However, in daily practice it's a pain to have all those extra type
+-- variables floating around. If you'd like to hide them, you can use
+-- the type families below to do so; see the definition of class
+-- GArrowSTKC for an example. Keep in mind, however, that any given
+-- type may only have a single instance declared using the type
+-- families.
+--
+
+type family GArrowTensor g :: * -> * -> * -- (**)
+type family GArrowUnit g :: * -- ()
+type family GArrowExponent g :: * -> * -> * -- (~>)
+
+
+
+
+------------------------------------------------------------------------
+-- Commonly Implemented Collections of Classes
+
+--
+-- The simply typed KAPPA calculus; see Hasegawa, __Decomposing Typed
+-- Lambda Calculus into a Couple of Categorical Programming
+-- Languages__, http://dx.doi.org/10.1007/3-540-60164-3_28
+--
+
+class (GArrowDrop g (GArrowTensor g) (GArrowUnit g),
+ GArrowCopy g (GArrowTensor g) (GArrowUnit g),
+ GArrowSwap g (GArrowTensor g) (GArrowUnit g)) =>
+ GArrowSTKC g
+
+class (GArrowDrop g (GArrowTensor g) (GArrowUnit g),
+ GArrowCopy g (GArrowTensor g) (GArrowUnit g),
+ GArrowSwap g (GArrowTensor g) (GArrowUnit g),
+ GArrowLoop g (GArrowTensor g) (GArrowUnit g)) =>
+ GArrowSTKCL g
+
+-- The simply typed LAMBDA calculus
+class (GArrowDrop g (GArrowTensor g) (GArrowUnit g),
+ GArrowCopy g (GArrowTensor g) (GArrowUnit g),
+ GArrowSwap g (GArrowTensor g) (GArrowUnit g),
+ GArrowCurry g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
+ GArrowApply g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g)
+ ) =>
+ GArrowSTLC g
+
+-- Programming Language for Computable Functions (w/o integers and booleans)
+class (GArrowDrop g (GArrowTensor g) (GArrowUnit g),
+ GArrowCopy g (GArrowTensor g) (GArrowUnit g),
+ GArrowSwap g (GArrowTensor g) (GArrowUnit g),
+ GArrowCurry g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
+ GArrowApply g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
+ GArrowLoop g (GArrowTensor g) (GArrowUnit g)
+ ) =>
+ GArrowPCF g (**) u (~>)
+
+
+
+
+
+------------------------------------------------------------------------
+-- Experimental, Not Yet Exported
+
+-- See Lindley, Wadler, and Yallop '08 -- except that here ga_force
+-- is primitive since there is no "arr" to define it in terms of.
+class GArrow g (**) u => GArrowStatic g (**) u (~>) where
+ ga_delay :: g a b -> g u (a~>b)
+ ga_force :: g u (a~>b) -> g a b
+ -- "ga_static/force_delay" forall a . force (delay a) = a
+ -- "ga_static/delay_force" forall a . delay (force a) = a