X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=GHC%2FHetMet%2FGArrow.hs;h=9878a4d5842e4947449c873392f5cef26819058d;hb=fe3e9a061c212b2c9f83e31632236afcaacacb81;hp=e1ac446e7377db27f25baa6d095b8528ae9742c4;hpb=5d6e930086fffc10e70fe91fa30ae01d9f75c6a9;p=ghc-base.git

diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs
index e1ac446..9878a4d 100644
--- a/GHC/HetMet/GArrow.hs
+++ b/GHC/HetMet/GArrow.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances -XFunctionalDependencies #-}
+{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies -XTypeFamilies -XFlexibleContexts #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  GHC.HetMet.GArrow
@@ -14,46 +14,234 @@ 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(..),
-  GArrowLiteral(..)
+
+  GArrowCurry(..),
+  GArrowApply(..),
+
+  GArrowTensor,
+  GArrowUnit,
+  GArrowExponent,
+
+  GArrowSTKC(..),
+  GArrowSTKCL(..),
+  GArrowSTLC(..),
+  GArrowPCF(..)
+
 ) where
-import Control.Category
+import Control.Category hiding ((.))
+import Prelude          hiding (id)
+
+------------------------------------------------------------------------
+-- The main GArrow class
 
-class Category g => GArrow g (**) | g -> (**) where
+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 ()
 
-class GArrow g (**) => GArrowCopy g (**) where
+------------------------------------------------------------------------
+-- The three context-manipulation classes
+
+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
+
+
+------------------------------------------------------------------------
+-- 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 (**) u => GArrowLiteral g (**) u t r where
+  ga_literal  :: t -> g u r
+
+
+
+
+------------------------------------------------------------------------
+-- Constant and Run, which are dual to each other
+
+class GArrow g (**) u => GArrowEval g (**) u r t where
+  ga_eval      :: g u r -> t
+
+class GArrow g (**) u => GArrowConstant g (**) u t r where
+  ga_constant  :: t -> g u r
+
+
+
+
+
+------------------------------------------------------------------------
+-- 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 (~>)
+
 
--- implementation of ga_second for GArrowSwap instances
-ga_swap_second f = ga_swap >>> ga_first f >>> ga_swap
 
-class GArrow g (**) => GArrowLoop g (**) where
-  ga_loop      :: g (x**z) (y**z) -> g x y
 
-class GArrow g (**) => GArrowLiteral g (**) a where
-  ga_literal   :: a -> g () a
 
--- not sure -- subject to change
-class GArrow g (**) => GArrowReify g (**) where
-  ga_reify     :: (x -> y) -> g x y
+------------------------------------------------------------------------
+-- Experimental, Not Yet Exported
 
--- not sure -- subject to change
-class GArrow g (**) => GArrowReflect g (**) where
-  ga_reflect   :: g x y -> (x -> y)
+-- 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