add GArrowTensor, GArrowUnit, and GArrowExponent which use type families to reduce...

diff --git a/GHC/HetMet/CodeTypes.hs b/GHC/HetMet/CodeTypes.hs
index d7dcac2..fcb13ca 100644 (file)
--- a/GHC/HetMet/CodeTypes.hs
+++ b/GHC/HetMet/CodeTypes.hs
@@ -31,11 +31,11 @@ hetmet_csp = Prelude.error "hetmet_csp should never be evaluated; did you forget
 
 hetmet_flatten ::
    forall g .
-    GArrowSTKC g (,) () =>
+    GArrowSTKC g =>
       forall x y.
          <[ y ]>@g
          ->
-         (g () y)
+         (g (GArrowUnit g) y)
 hetmet_flatten x = unG (pga_flatten x)
 
 -- After the flattening pass the argument and result types of this
@@ -46,18 +46,18 @@ hetmet_flatten x = unG (pga_flatten x)
 pga_flatten ::
    forall g x y.
      <[ y ]>@g ->
-     PGArrow g () y
+     PGArrow g (GArrowUnit g) y
 pga_flatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
 pga_unflatten ::
    forall g x y.
-     PGArrow g () y ->
+     PGArrow g (GArrowUnit g) y ->
      <[ y ]>@g
 pga_unflatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
 
 pga_flattened_id ::
    forall g x y.
-     PGArrow g () y ->
-     PGArrow g () y
+     PGArrow g (GArrowUnit g) y ->
+     PGArrow g (GArrowUnit g) y
 pga_flattened_id x = x
 
 

diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs
index b9bfccf..0ba6e3f 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,6 +30,10 @@ module GHC.HetMet.GArrow (
   GArrowCurry(..),
   GArrowApply(..),
 
+  GArrowTensor,
+  GArrowUnit,
+  GArrowExponent,
+
   GArrowKappa(..),
   GArrowSTKC(..),
   GArrowSTLC(..),
@@ -77,6 +81,8 @@ ga_swap_second f =
 
 
 
+
+
 ------------------------------------------------------------------------
 -- Products, Coproducts, etc
 
@@ -170,6 +176,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
 
@@ -178,21 +209,30 @@ 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
 
 -- 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 (~>)
 
 
 

diff --git a/GHC/HetMet/Private.hs b/GHC/HetMet/Private.hs
index a55d282..9308087 100644 (file)
--- a/GHC/HetMet/Private.hs
+++ b/GHC/HetMet/Private.hs
@@ -37,41 +37,41 @@ import GHC.HetMet.GArrow
 -------------------------------------------------------------------------
 -- Used internally by the compiler, subject to change without notice!!
 
-newtype PGArrow g x y = PGArrowD { unG :: GArrowSTKC g (,) () => g x y }
+newtype PGArrow g x y = PGArrowD { unG :: GArrowSTKC g => g x y }
 
 pga_id        :: forall g x. PGArrow g x x
 pga_id        =  PGArrowD { unG = Control.Category.id }
 pga_comp      :: forall g x y z. PGArrow g x y -> PGArrow g y z -> PGArrow g x z
 pga_comp f g  =  PGArrowD { unG = unG f >>> unG g }
-pga_first     :: forall g x y z . PGArrow g x y -> PGArrow g (x , z) (y , z)
+pga_first     :: forall g x y z . PGArrow g x y -> PGArrow g (GArrowTensor g x z) (GArrowTensor g y z)
 pga_first f   =  PGArrowD { unG = ga_first $ unG f }
-pga_second    :: forall g x y z . PGArrow g x y -> PGArrow g (z , x) (z , y)
+pga_second    :: forall g x y z . PGArrow g x y -> PGArrow g (GArrowTensor g z x) (GArrowTensor g z y)
 pga_second f  =  PGArrowD { unG = ga_second $ unG f }
-pga_cancell   :: forall g x . PGArrow g ((),x)         x
+pga_cancell   :: forall g x . PGArrow g (GArrowTensor g (GArrowUnit g) x)         x
 pga_cancell   =  PGArrowD { unG = ga_cancell }
-pga_cancelr   :: forall g x . PGArrow g    (x,())      x
+pga_cancelr   :: forall g x . PGArrow g    (GArrowTensor g x (GArrowUnit g))      x
 pga_cancelr   =  PGArrowD { unG = ga_cancelr }
-pga_uncancell :: forall g x . PGArrow g     x      ((),x)
+pga_uncancell :: forall g x . PGArrow g     x      (GArrowTensor g (GArrowUnit g) x)
 pga_uncancell =  PGArrowD { unG = ga_uncancell }
-pga_uncancelr :: forall g x . PGArrow g     x         (x,())
+pga_uncancelr :: forall g x . PGArrow g     x         (GArrowTensor g x (GArrowUnit g))
 pga_uncancelr =  PGArrowD { unG = ga_uncancelr }
-pga_assoc     :: forall g x y z . PGArrow g ((x, y),z ) ( x,(y ,z))
+pga_assoc     :: forall g x y z . PGArrow g (GArrowTensor g (GArrowTensor g x y) z) (GArrowTensor g x (GArrowTensor g y z))
 pga_assoc     =  PGArrowD { unG = ga_assoc }
-pga_unassoc   :: forall g x y z . PGArrow g ( x,(y ,z)) ((x, y),z )
+pga_unassoc   :: forall g x y z . PGArrow g (GArrowTensor g x (GArrowTensor g y z)) (GArrowTensor g (GArrowTensor g x y) z)
 pga_unassoc   =  PGArrowD { unG = ga_unassoc }
-pga_copy      :: forall g x . PGArrow g x (x,x)
+pga_copy      :: forall g x . PGArrow g x (GArrowTensor g x x)
 pga_copy      =  PGArrowD { unG = ga_copy }
-pga_drop      :: forall g x . PGArrow g x ()
+pga_drop      :: forall g x . PGArrow g x (GArrowUnit g)
 pga_drop      =  PGArrowD { unG = ga_drop }
-pga_swap      :: forall g x y . PGArrow g (x,y) (y,x)
+pga_swap      :: forall g x y . PGArrow g (GArrowTensor g x y) (GArrowTensor g y x)
 pga_swap      =  PGArrowD { unG = ga_swap }
-pga_applyl    :: forall g x y . PGArrow g (x,(x->y)   ) y
+pga_applyl    :: forall g x y . PGArrow g (GArrowTensor g x (GArrowExponent g x y)   ) y
 pga_applyl    =  error "not implemented"
-pga_applyr    :: forall g x y . PGArrow g (   (x->y),x) y
+pga_applyr    :: forall g x y . PGArrow g (GArrowTensor g (GArrowExponent g x y) x) y
 pga_applyr    =  error "not implemented"
-pga_curryl    :: forall g x y z . PGArrow g (x,y) z  ->  PGArrow g x (y->z)
+pga_curryl    :: forall g x y z . PGArrow g (GArrowTensor g x y) z  ->  PGArrow g x (GArrowExponent g y z)
 pga_curryl    =  error "not implemented"
-pga_curryr    :: forall g x y z . PGArrow g (x,y) z  ->  PGArrow g y (x->z)
+pga_curryr    :: forall g x y z . PGArrow g (GArrowTensor g x y) z  ->  PGArrow g y (GArrowExponent g x z)
 pga_curryr    =  error "not implemented"
-pga_kappa     :: forall g x y . (g () x -> g () y) -> g x y
+pga_kappa     :: forall g x y . (g (GArrowUnit g) x -> g (GArrowUnit g) y) -> g x y
 pga_kappa     =  error "not implemented"