IGArrow: some improvements

diff --git a/GHC/HetMet/IGArrow.hs b/GHC/HetMet/IGArrow.hs
index cc6bd04..ea5964c 100644 (file)
--- a/GHC/HetMet/IGArrow.hs
+++ b/GHC/HetMet/IGArrow.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, MultiParamTypeClasses, NoMonomorphismRestriction, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts, FlexibleInstances, DatatypeContexts #-}
+{-# LANGUAGE RankNTypes, MultiParamTypeClasses, NoMonomorphismRestriction, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts, FlexibleInstances, DatatypeContexts, UndecidableInstances, ScopedTypeVariables #-}

 -----------------------------------------------------------------------------
 -- |
 -- Module      :  GHC.HetMet.IGArrow
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  GHC.HetMet.IGArrow

@@ -27,10 +27,11 @@ module GHC.HetMet.IGArrow (
   -- IGArrowProd(..),
 
 ) where
   -- IGArrowProd(..),
 
 ) where

-import Control.Category hiding ((.))
+import Control.Category

 import GHC.HetMet.GArrow
 import GHC.HetMet.GArrow

-import Prelude          hiding (id)

 import GHC.HetMet.Arrow
 import GHC.HetMet.Arrow

+import GHC.HetMet.GArrowFullyEnriched
+import Prelude          hiding (id, (.))

 
 
 
 
 
 

@@ -42,7 +43,7 @@ import GHC.HetMet.Arrow
 -- | An "internal generalized arrow" is a GArrow except that it uses
 -- some *other* GArrow in place of Haskell's function space.
 --
 -- | An "internal generalized arrow" is a GArrow except that it uses
 -- some *other* GArrow in place of Haskell's function space.
 --

-class IGArrow g (**) u gg (***) uu where
+class GArrow g (**) u => IGArrow g (**) u gg (***) uu | gg -> (***), (***) -> uu where

   iga_id        :: g u (gg x x)
   iga_comp      :: g ((gg x y) ** (gg y z)) (gg x z)
   iga_first     :: g (gg x y) (gg (x *** z) (y *** z))
   iga_id        :: g u (gg x x)
   iga_comp      :: g ((gg x y) ** (gg y z)) (gg x z)
   iga_first     :: g (gg x y) (gg (x *** z) (y *** z))

@@ -84,6 +85,28 @@ class IGArrow g (**) u gg (***) uu => IGArrowReflect g (**) u gg (***) uu r q x
 
 
 
 
 
 

+{-
+-- | This is named "kappa" for its similarity to an operator in
+--   Hasegawa's kappa-calculus, but there isn't actually a formal
+--   connection.
+class GArrow g (**) u => IKappa g (**) u where
+  iga_kappa     :: forall a b c uu .
+                   (forall gg (***) . (IGArrow     g (**) u gg (***) uu,
+                                       IGArrowCopy g (**) u gg (***) uu,
+                                       IGArrowSwap g (**) u gg (***) uu,
+                                       IGArrowDrop g (**) u gg (***) uu) => g (gg uu a) (gg b c)) ->
+                   (forall gg (***) . (IGArrow     g (**) u gg (***) uu,
+                                       IGArrowCopy g (**) u gg (***) uu,
+                                       IGArrowSwap g (**) u gg (***) uu,
+                                       IGArrowDrop g (**) u gg (***) uu) => g u (gg (a***b) c))
+  -- TO DO: probably need l/r versions of the above
+
+--class IGArrow g (**) u gg (***) uu => IGArrowKappa g (**) u gg (***) uu where
+--  iga_kappa     :: g (x**(gg uu a)) (gg b c) -> g x (gg (a***b) c)
+  -- TO DO: probably need l/r versions of the above
+
+
+

 
 
 ------------------------------------------------------------------------------
 
 
 ------------------------------------------------------------------------------

@@ -92,7 +115,7 @@ class IGArrow g (**) u gg (***) uu => IGArrowReflect g (**) u gg (***) uu r q x
 --
 -- | A self-internal GArrow is, well, internal to itself
 --
 --
 -- | A self-internal GArrow is, well, internal to itself
 --

-class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
+--class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u

 
 --
 -- | Self-internal GArrows have curry/apply
 
 --
 -- | Self-internal GArrows have curry/apply

@@ -118,6 +141,7 @@ class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
 --
 -- | Every GArrow is internal to the GArrow instance on (->)
 --
 --
 -- | Every GArrow is internal to the GArrow instance on (->)
 --

+{-

 instance GArrow g (**) u => IGArrow (->) (,) () g (**) u where
   iga_id        _     = id
   iga_comp      (f,g) = f >>> g
 instance GArrow g (**) u => IGArrow (->) (,) () g (**) u where
   iga_id        _     = id
   iga_comp      (f,g) = f >>> g

@@ -129,11 +153,18 @@ instance GArrow g (**) u => IGArrow (->) (,) () g (**) u where
   iga_uncancelr _     = ga_uncancelr
   iga_assoc     _     = ga_assoc
   iga_unassoc   _     = ga_unassoc
   iga_uncancelr _     = ga_uncancelr
   iga_assoc     _     = ga_assoc
   iga_unassoc   _     = ga_unassoc

-
-
-
-
-
+instance GArrowCopy g (**) u => IGArrowCopy (->) (,) () g (**) u where
+instance GArrowSwap g (**) u => IGArrowSwap (->) (,) () g (**) u where
+instance GArrowDrop g (**) u => IGArrowDrop (->) (,) () g (**) u where
+-}
+
+data
+    In g x y
+    = In (g x y)
+instance GArrow g (**) u     => IGArrow (->) (,) ()     (In g) (**) u where
+instance GArrowCopy g (**) u => IGArrowCopy (->) (,) () (In g) (**) u where
+instance GArrowSwap g (**) u => IGArrowSwap (->) (,) () (In g) (**) u where
+instance GArrowDrop g (**) u => IGArrowDrop (->) (,) () (In g) (**) u where

 
 ------------------------------------------------------------------------
 -- Externalization
 
 ------------------------------------------------------------------------
 -- Externalization

@@ -146,10 +177,86 @@ instance GArrow g (**) u => IGArrow (->) (,) () g (**) u where
 -- (IGArrow g)), create an (IGArrow g).
 --
 
 -- (IGArrow g)), create an (IGArrow g).
 --
 

-newtype
-    IGArrow g (**) u q (***) uu =>
-    Ext g (**) u q (***) uu x y
-    = Ext { unExt :: g u (q x y) }
+data
+    Ext g x y
+    = Ext (g x y)
+
+
+--
+-- | Every IGArrow of (->) is a GArrow
+--
+instance IGArrow (->) (,) () g (**) u => Category (Ext g) where
+  id                = Ext (iga_id ())
+  (Ext g) . (Ext f) = Ext (iga_comp (f,g))
+
+instance IGArrow (->) (,) () g (**) u => GArrow (Ext g) (**) u where
+--  ga_first     (Ext f) = Ext $ iga_first f
+--  ga_second    (Ext f) = Ext $ iga_second f
+  ga_cancell           = Ext $ iga_cancell ()
+  ga_cancelr           = Ext $ iga_cancelr ()
+  ga_uncancell         = Ext $ iga_uncancell ()
+  ga_uncancelr         = Ext $ iga_uncancelr ()
+  ga_assoc             = Ext $ iga_assoc ()
+  ga_unassoc           = Ext $ iga_unassoc ()
+
+instance IGArrowSwap (->) (,) () g (**) u => GArrowSwap (Ext g) (**) u where
+instance IGArrowCopy (->) (,) () g (**) u => GArrowCopy (Ext g) (**) u where
+instance IGArrowDrop (->) (,) () g (**) u => GArrowDrop (Ext g) (**) u where
+
+
+--  iga_kappa     :: forall a b c uu . (forall gg (***) . IGArrow g (**) u gg (***) uu => g (gg uu a) (gg b c)) ->
+--                   (forall gg (***) . IGArrow g (**) u gg (***) uu => g u (gg (a***b) c))
+{-
+    Could not deduce (GArrowDrop gg (***) uu,
+                      GArrowSwap gg (***) uu,
+                      GArrowCopy gg (***) uu)
+      arising from a use of `homfunctor_inv'
+    from the context (IGArrow (->) (,) () gg (***) uu)
+-}
+
+--homfunctor_inv :: forall a b c u .
+--    (forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c) ->
+--    (forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c)
+
+--
+-- | Every GArrow is also an IKappa of (->) by virtue of GArrowFullyEnriched
+--
+instance IKappa (->) (,) () where
+--  iga_kappa     :: forall a b c u .
+--                   (forall g (**) . (IGArrow     (->) (,) () g (**) u,
+--                                       IGArrowCopy (->) (,) () g (**) u,
+--                                       IGArrowSwap (->) (,) () g (**) u,
+--                                       IGArrowDrop (->) (,) () g (**) u) => (g u a) -> (g b c)) ->
+--                   (forall g (**) . (IGArrow     (->) (,) () g (**) u,
+--                                       IGArrowCopy (->) (,) () g (**) u,
+--                                       IGArrowSwap (->) (,) () g (**) u,
+--                                       IGArrowDrop (->) (,) () g (**) u) => () -> (g (a**b) c))
+  iga_kappa (f :: forall g (**) .
+                  (IGArrow (->) (,) () g (**) u,
+                   IGArrowCopy (->) (,) () g (**) u,
+                   IGArrowDrop (->) (,) () g (**) u,
+                   IGArrowSwap (->) (,) () g (**) u) =>
+                  (g u a)->(g b c)) ()
+     = mork $ homfunctor_inv (\y -> case f (In y) of (In q) -> q)
+
+mork :: forall u a b c . 
+        (forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c)
+ -> (forall g (**) . (IGArrow     (->) (,) () g (**) u,
+                      IGArrowCopy (->) (,) () g (**) u,
+                      IGArrowSwap (->) (,) () g (**) u,
+                      IGArrowDrop (->) (,) () g (**) u) => (g (a**b) c))
+mork = undefined
+{-
+         z :: forall g (**) . IGArrow (->) (,) () g (**) u => g (a**b) c
+         z = let 
+               qf :: forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c
+               qf y = f y
+             in case homfunctor_inv qf of Ext q -> q
+-}
+
+{-
+instance IGArrow (->) (,) () g (**) u => GArrowSTKC (Ext g)
+-}

 
 -- instance IGArrow g (**) u gg (***) uu => GArrowCopy g (**) u gg (***) uu where
 --   iga_copy      = undefined
 
 -- instance IGArrow g (**) u gg (***) uu => GArrowCopy g (**) u gg (***) uu where
 --   iga_copy      = undefined

@@ -178,3 +285,22 @@ newtype
 -- 
 -- instance IGArrow g (**) u gg (***) uu => GArrowReflect g (**) u gg (***) uu r q x y where
 --   iga_reflect   = undefined
 -- 
 -- instance IGArrow g (**) u gg (***) uu => GArrowReflect g (**) u gg (***) uu r q x y where
 --   iga_reflect   = undefined

+
+
+-- | Haskell's function space is self-internal
+-- instance SelfInternalGArrow (->) (,) ()
+
+--
+--     x , 1->a   |-    b ->c
+--    --------------------------   [Kappa]
+--     x          |- (a,b)->c
+--
+-- forall a b c x.
+--   (forall g (**) u gg (***) uu .
+--     IGArrow g (**) u gg (***) uu =>
+--       g (x**(gg uu a)) (gg b c))
+--   ->
+--   (forall g (**) u gg (***) uu .
+--     IGArrow g (**) u gg (***) uu =>
+--       g x (gg (a***b) c))
+-}
\ No newline at end of file