IGArrow: major cleanup, finished instance IKappa (->)

diff --git a/GHC/HetMet/IGArrow.hs b/GHC/HetMet/IGArrow.hs
index ea5964c..4846022 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, UndecidableInstances, ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes, MultiParamTypeClasses, TypeOperators, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}

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

@@ -29,10 +29,16 @@ module GHC.HetMet.IGArrow (
 ) where
 import Control.Category
 import GHC.HetMet.GArrow
 ) where
 import Control.Category
 import GHC.HetMet.GArrow

-import GHC.HetMet.Arrow

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

+--
+-- Importing GHC.HetMet.Arrow leads to overlapping instances; that's
+-- why you see (GArrow (->) (,) () => ...) below in many places
+-- instead of simply providing the instance defined in
+-- GHC.HetMet.Arrow.
+--
+--import GHC.HetMet.Arrow

 
 
 
 
 
 

@@ -43,7 +49,7 @@ import Prelude          hiding (id, (.))
 -- | 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 GArrow g (**) u => IGArrow g (**) u gg (***) uu | gg -> (***), (***) -> uu where
+class GArrow g (**) u => IGArrow g (**) u gg (***) uu | g -> (**), (**) -> u, 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))

@@ -59,7 +65,7 @@ class IGArrow g (**) u gg (***) uu => IGArrowCopy g (**) u gg (***) uu where
   iga_copy      :: g u (gg x (x***x))
 
 class IGArrow g (**) u gg (***) uu => IGArrowDrop g (**) u gg (***) uu where
   iga_copy      :: g u (gg x (x***x))
 
 class IGArrow g (**) u gg (***) uu => IGArrowDrop g (**) u gg (***) uu where

-  iga_drop      :: g u (gg x u)
+  iga_drop      :: g u (gg x uu)

 
 class IGArrow g (**) u gg (***) uu => IGArrowSwap g (**) u gg (***) uu where
   iga_swap      :: g u (gg (x***y) (y***x))
 
 class IGArrow g (**) u gg (***) uu => IGArrowSwap g (**) u gg (***) uu where
   iga_swap      :: g u (gg (x***y) (y***x))

@@ -85,222 +91,148 @@ 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
+------------------------------------------------------------------------
+-- Externalization
+--
+-- | An IGArrow may be "externalized" to form a normal generalized
+-- arrow.  If the IGArrow was an instance of class IGArrowXX, the
+-- externalization will be an instance of GArrowYY.
+--
+-- TODO: I should be one level deeper here: assuming an (IGArrow
+-- (IGArrow g)), create an (IGArrow g).
+--
+
+newtype Ex g x y = Ex (g x y)

 
 

---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
+--
+-- | Every IGArrow of (->) is a GArrow
+--
+instance IGArrow (->) (,) () g (**) u => Category (Ex g) where
+  id                = Ex (iga_id ())
+  (Ex g) . (Ex f) = Ex (iga_comp (f,g))

 
 

+instance IGArrow (->) (,) () g (**) u => GArrow (Ex g) (**) u where
+  ga_first     (Ex f) = Ex $ iga_first f
+  ga_second    (Ex f) = Ex $ iga_second f
+  ga_cancell           = Ex $ iga_cancell ()
+  ga_cancelr           = Ex $ iga_cancelr ()
+  ga_uncancell         = Ex $ iga_uncancell ()
+  ga_uncancelr         = Ex $ iga_uncancelr ()
+  ga_assoc             = Ex $ iga_assoc ()
+  ga_unassoc           = Ex $ iga_unassoc ()

 
 

+instance IGArrowCopy (->) (,) () g (**) u => GArrowCopy (Ex g) (**) u where
+  ga_copy              = Ex $ iga_copy ()
+instance IGArrowDrop (->) (,) () g (**) u => GArrowDrop (Ex g) (**) u where
+  ga_drop              = Ex $ iga_drop ()
+instance IGArrowSwap (->) (,) () g (**) u => GArrowSwap (Ex g) (**) u where
+  ga_swap              = Ex $ iga_swap ()

 
 
 
 
 
 

-------------------------------------------------------------------------------
--- Self-Internal GArrows

 
 

---
--- | A self-internal GArrow is, well, internal to itself
---
---class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u

 
 

+------------------------------------------------------------------------
+-- Internalization

 --
 --

--- | Self-internal GArrows have curry/apply
---
--- instance SelfInternalGArrow g (**) u => GArrowApply g (**) u gg where
---   ga_applyl =    :: g (x**(g x y)   ) y
---   ga_applyr    :: g (   (g x y)**x) y
--- 
---
--- | Self-internal GArrows have curry/apply
+-- | Every GArrow is internal to the GArrow instance on (->)

 --
 --

--- instance SelfInternalGArrow g (**) u gg (***) uu => GArrowCurry g (**) u gg where
---   ga_curryl    :: g (x**y) z  ->  g x (g y z)
---   ga_curryr    :: g (x**y) z  ->  g y (g x z)

 
 

+newtype In g x y = In (g x y)

 
 

+instance (GArrow (->) (,) (), GArrow g (**) u) => IGArrow (->) (,) () (In g) (**) u where
+  iga_id        _           = In $ id
+  iga_comp      (In f,In g) = In $ f >>> g
+  iga_first     (In f)      = In $ ga_first f
+  iga_second    (In f)      = In $ ga_second f
+  iga_cancell   _           = In $ ga_cancell
+  iga_cancelr   _           = In $ ga_cancelr
+  iga_uncancell _           = In $ ga_uncancell
+  iga_uncancelr _           = In $ ga_uncancelr
+  iga_assoc     _           = In $ ga_assoc
+  iga_unassoc   _           = In $ ga_unassoc
+instance (GArrow (->) (,) (), GArrowCopy g (**) u) => IGArrowCopy (->) (,) () (In g) (**) u where
+  iga_copy      _           = In $ ga_copy
+instance (GArrow (->) (,) (), GArrowDrop g (**) u) => IGArrowDrop (->) (,) () (In g) (**) u where
+  iga_drop      _           = In $ ga_drop
+instance (GArrow (->) (,) (), GArrowSwap g (**) u) => IGArrowSwap (->) (,) () (In g) (**) u where
+  iga_swap      _           = In $ ga_swap

 
 
 
 
 
 

-------------------------------------------------------------------------------
--- Instances

 
 

---
--- | 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
-  iga_first           = ga_first
-  iga_second          = ga_second
-  iga_cancell   _     = ga_cancell
-  iga_cancelr   _     = ga_cancelr
-  iga_uncancell _     = ga_uncancell
-  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
+-- Kappa

 --
 --

--- | An IGArrow may be "externalized" to form a normal generalized
--- arrow.  If the IGArrow was an instance of class IGArrowXX, the
--- externalization will be an instance of GArrowYY.
+-- | This is named "kappa" for its similarity to an operator in
+--   Hasegawa's kappa-calculus, but the formal connection is a bit of
+--   a stretch; the method iga_kappa below is used by the flattener to
+--   implement the typing rule for abstraction in Kappa-calculus.

 --
 --

--- TODO: I should be one level deeper here: assuming an (IGArrow
--- (IGArrow g)), create an (IGArrow g).
+--         x , 1->a   |-    b ->c
+--        --------------------------   [Kappa]
+--         x          |- (a,b)->c
+--
+--
+class GArrow g (**) u => IKappa g (**) u where
+  iga_kappa :: forall a b c .
+              (forall gg (***) uu . (IGArrowCopy g (**) u gg (***) uu,
+                                     IGArrowDrop g (**) u gg (***) uu,
+                                     IGArrowSwap g (**) u gg (***) uu) =>
+               g (gg uu a) (gg b c)) ->
+              (forall gg (***) uu . (IGArrowCopy g (**) u gg (***) uu,
+                                     IGArrowDrop g (**) u gg (***) uu,
+                                     IGArrowSwap g (**) u gg (***) uu) =>
+               g u (gg (a***b) c))
+  -- TO DO: change the above to iga_kappal, add iga_kappar
+
+--
+-- | The (->) GArrow has the Kappa property.

 --
 --

+instance GArrow (->) (,) () => IKappa (->) (,) () where
+  iga_kappa f = case (homfunctor_inv (\x -> case f (In x) of In x' -> x')) of Ex x -> \() -> x

 
 

-data
-    Ext g x y
-    = Ext (g x y)

 
 
 
 

+
+
+
+------------------------------------------------------------------------------
+-- Self-Internal GArrows
+

 --
 --

--- | Every IGArrow of (->) is a GArrow
+-- | A self-internal GArrow is, well, internal to itself

 --
 --

-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)
+class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u

 
 --
 
 --

--- | Every GArrow is also an IKappa of (->) by virtue of GArrowFullyEnriched
+-- | Self-internal GArrows have curry/apply

 --
 --

-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 => GArrowDrop g (**) u gg (***) uu where
---   iga_drop      = undefined
--- 
--- instance IGArrow g (**) u gg (***) uu => GArrowSwap g (**) u gg (***) uu where
---   iga_swap      = undefined
--- 
--- instance IGArrow g (**) u gg (***) uu => GArrowLoop g (**) u gg (***) uu where
---   iga_loopr    = undefined
---   iga_loopl    = undefined
--- 
--- instance IGArrow g (**) u gg (***) uu => GArrowLiteral g (**) u gg (***) uu t r where
---   iga_literal  = undefined
--- 
--- instance IGArrow g (**) u gg (***) uu => GArrowEval g (**) u gg (***) uu r t where
---   iga_eval      = undefined
--- 
--- instance IGArrow g (**) u gg (***) uu => GArrowConstant g (**) u gg (***) uu t r where
---   iga_constant  = undefined
--- 
--- instance IGArrow g (**) u gg (***) uu => GArrowReify g (**) u gg (***) uu x y r q where
---   iga_reify     = undefined
--- 
--- instance IGArrow g (**) u gg (***) uu => GArrowReflect g (**) u gg (***) uu r q x y where
---   iga_reflect   = undefined
-
+instance SelfInternalGArrow g (**) u => GArrowApply g (**) u g where
+  ga_applyl = error "FIXME: SelfInternalGArrow => GArrowApply not implemented yet"
+  ga_applyr = error "FIXME: SelfInternalGArrow => GArrowApply not implemented yet"

 
 

--- | Haskell's function space is self-internal
--- instance SelfInternalGArrow (->) (,) ()
+--
+-- | Self-internal GArrows have curry/apply
+--
+instance SelfInternalGArrow g (**) u => GArrowCurry g (**) u g where
+  ga_curryl = error "FIXME: SelfInternalGArrow => GArrowCurry not implemented yet"
+  ga_curryr = error "FIXME: SelfInternalGArrow => GArrowCurry not implemented yet"

 
 --
 
 --

---     x , 1->a   |-    b ->c
---    --------------------------   [Kappa]
---     x          |- (a,b)->c
+-- | Haskell's function space is self-internal

 --
 --

--- 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
+instance GArrow (->) (,) () => IGArrow (->) (,) () (->) (,) () where
+  iga_id        _ = id
+  iga_comp  (f,g) = f >>> g
+  iga_first       = ga_first
+  iga_second      = ga_second
+  iga_cancell   _ = ga_cancell
+  iga_cancelr   _ = ga_cancelr
+  iga_uncancell _ = ga_uncancell
+  iga_uncancelr _ = ga_uncancelr
+  iga_assoc     _ = ga_assoc
+  iga_unassoc   _ = ga_unassoc
+
+--instance GArrow (->) (,) () => SelfInternalGArrow (->) (,) ()