-{-# 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
-- IGArrowProd(..),
) where
-import Control.Category hiding ((.))
+import Control.Category
import GHC.HetMet.GArrow
-import Prelude hiding (id)
import GHC.HetMet.Arrow
+import GHC.HetMet.GArrowFullyEnriched
+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.
--
-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))
+{-
+-- | 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
+
+
+
------------------------------------------------------------------------------
--
-- | 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
--
-- | 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_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
-- (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 => 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