add GArrowSTKCL for flattening of fixpoints

[ghc-base.git] / GHC / HetMet / GArrow.hs

diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs
index 0c32468..8b88b9b 100644 (file)
--- a/GHC/HetMet/GArrow.hs
+++ b/GHC/HetMet/GArrow.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies #-}
+{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies -XTypeFamilies -XFlexibleContexts #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  GHC.HetMet.GArrow
@@ -30,12 +30,19 @@ module GHC.HetMet.GArrow (
   GArrowCurry(..),
   GArrowApply(..),
 
+  GArrowTensor,
+  GArrowUnit,
+  GArrowExponent,
+
+  GArrowKappa(..),
   GArrowSTKC(..),
+  GArrowSTKCL(..),
   GArrowSTLC(..),
   GArrowPCF(..)
 
 ) where
-import Control.Category
+import Control.Category hiding ((.))
+import Prelude          hiding (id)
 
 ------------------------------------------------------------------------
 -- The main GArrow class
@@ -75,6 +82,8 @@ ga_swap_second f =
 
 
 
+
+
 ------------------------------------------------------------------------
 -- Products, Coproducts, etc
 
@@ -99,8 +108,8 @@ ga_inr = ga_uncancell >>> ga_first  ga_never
 -- Loop
 
 class GArrow g (**) u => GArrowLoop g (**) u where
-  ga_loopl    :: g (x**z) (y**z) -> g x y
-  ga_loopr    :: g (z**x) (z**y) -> g x y
+  ga_loopr    :: g (x**z) (y**z) -> g x y
+  ga_loopl    :: g (z**x) (z**y) -> g x y
 
 
 ------------------------------------------------------------------------
@@ -127,7 +136,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
@@ -142,6 +151,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
@@ -155,6 +177,31 @@ class GArrow g (**) u => GArrowCurry g (**) u (~>) where
 
 
 
+
+------------------------------------------------------------------------
+-- 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
 
@@ -163,21 +210,36 @@ class GArrow g (**) u => GArrowCurry g (**) u (~>) where
 -- Lambda Calculus into a Couple of Categorical Programming
 -- Languages__, http://dx.doi.org/10.1007/3-540-60164-3_28
 -- 
-class (GArrowDrop  g (**) u,
-       GArrowCopy  g (**) u,
-       GArrowSwap  g (**) u) =>
-       GArrowSTKC  g (**) u
+
+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 (GArrowSTKC  g (**) u,
-       GArrowCurry g (**) u (~>),
-       GArrowApply g (**) u (~>)) =>
-       GArrowSTLC  g (**) u (~>)
+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 (GArrowSTLC  g (**) u (~>),
-       GArrowLoop  g (**) u) =>
-       GArrowPCF   g (**) u (~>)
+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 (~>)