X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=GHC%2FHetMet%2FGArrow.hs;h=0ba6e3f4686408c268c9f5b0413f6104c33e580a;hb=cc87288eddc05564cd759a3273dbbad99985fb0d;hp=d55a807b6ee05670f16835d46b56beebc2fcc61d;hpb=f98950484a7cb01e43352e3d88277a2784cd58bf;p=ghc-base.git

diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs
index d55a807..0ba6e3f 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
@@ -21,21 +21,32 @@ module GHC.HetMet.GArrow (
   GArrowConstant(..),
   GArrowLiteral(..),   -- should be implemented, but never invoked, by user code
 
-  GArrowSum(..),
+  GArrowSum(..),  ga_inl, ga_inr,
   GArrowProd(..),
 
   GArrowReify(..),
   GArrowReflect(..),
 
   GArrowCurry(..),
-  GArrowApply(..)
+  GArrowApply(..),
+
+  GArrowTensor,
+  GArrowUnit,
+  GArrowExponent,
+
+  GArrowKappa(..),
+  GArrowSTKC(..),
+  GArrowSTLC(..),
+  GArrowPCF(..)
+
 ) where
-import Control.Category
+import Control.Category hiding ((.))
+import Prelude          hiding (id)
 
 ------------------------------------------------------------------------
 -- The main GArrow class
 
-class Category g => GArrow g (**) u | (**) -> u 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)
@@ -70,24 +81,26 @@ ga_swap_second f =
 
 
 
+
+
 ------------------------------------------------------------------------
 -- Products, Coproducts, etc
 
 
-class (GArrow     g (**)  u,
-       GArrow     g (<*>) u) =>
-       GArrowProd g (**)  u (<*>) where
-  ga_prod_copy :: g x (x<*>x)
-  ga_prod_drop :: g x  u
+class (GArrowDrop g (<*>) u,
+       GArrowCopy g (<*>) u) =>
+       GArrowProd g (<*>) u
 
-class (GArrow     g (**)  u,
-       GArrow     g (<+>) v) => 
-       GArrowSum  g (**)  u v (<+>) where
-  ga_merge :: g (x**x) x
-  ga_never :: g v      x
-      
+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
 
 
 ------------------------------------------------------------------------
@@ -122,7 +135,7 @@ class GArrow g (**) u => GArrowConstant g (**) u t r where
 
 
 ------------------------------------------------------------------------
--- Reify and Reflect, which are "curried" versions
+-- 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
@@ -137,6 +150,19 @@ class GArrow g (**) u => GArrowReflect g (**) u r q x y where
 
 
 ------------------------------------------------------------------------
+-- The Kappa adjunction
+--
+-- See Hasegawa, Decomposing Typed Lambda Calculus into a Couple of
+-- Categorical Programming Languages) section 3, rule $(\times L)$
+
+class GArrow g (**) u => GArrowKappa g (**) u where
+  ga_kappa :: (g u x -> g u y) -> g x y
+
+
+
+
+
+------------------------------------------------------------------------
 -- Apply and Curry
 
 class GArrow g (**) u => GArrowApply g (**) u (~>) where
@@ -144,5 +170,82 @@ class GArrow g (**) u => GArrowApply g (**) u (~>) where
   ga_applyr    :: g (   (x~>y)**x) y
 
 class GArrow g (**) u => GArrowCurry g (**) u (~>) where
-  ga_curryl    :: g x (y**(x~>y)   )
-  ga_curryr    :: g x (   (x~>y)**y)
+  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
+
+-- 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
+