--- /dev/null
+{-# LANGUAGE RankNTypes, MultiParamTypeClasses, NoMonomorphismRestriction, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts, FlexibleInstances, DatatypeContexts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : GHC.HetMet.IGArrow
+-- Copyright : none
+-- License : public domain
+--
+-- Maintainer : Adam Megacz <megacz@acm.org>
+-- Stability : experimental
+-- Portability : portable
+
+module GHC.HetMet.IGArrow (
+ IGArrow(..),
+ IGArrowDrop(..),
+ IGArrowCopy(..),
+ IGArrowSwap(..),
+ IGArrowLoop(..),
+
+ IGArrowEval(..),
+ IGArrowConstant(..),
+ IGArrowLiteral(..),
+
+ IGArrowReify(..),
+ IGArrowReflect(..),
+
+ -- IGArrowSum(..), ga_inl, ga_inr,
+ -- IGArrowProd(..),
+
+) where
+import Control.Category hiding ((.))
+import GHC.HetMet.GArrow
+import Prelude hiding (id)
+import GHC.HetMet.Arrow
+
+
+
+
+
+------------------------------------------------------------------------
+-- Internal GArrows
+--
+-- | 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
+ 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_second :: g (gg x y) (gg (z *** x) (z *** y))
+ iga_cancell :: g u (gg (uu***x) x)
+ iga_cancelr :: g u (gg (x***uu) x)
+ iga_uncancell :: g u (gg x (uu***x))
+ iga_uncancelr :: g u (gg x (x***uu))
+ iga_assoc :: g u (gg ((x*** y)***z ) ( x***(y ***z)))
+ iga_unassoc :: g u (gg ( x***(y ***z)) ((x*** y)***z ))
+
+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_drop :: g u (gg x u)
+
+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 => IGArrowLoop g (**) u gg (***) uu where
+ iga_loopr :: g (gg (x***z) (y***z)) (gg x y)
+ iga_loopl :: g (gg (z***x) (z***y)) (gg x y)
+
+class IGArrow g (**) u gg (***) uu => IGArrowLiteral g (**) u gg (***) uu t r where
+ iga_literal :: g t (gg uu r)
+
+class IGArrow g (**) u gg (***) uu => IGArrowEval g (**) u gg (***) uu r t where
+ iga_eval :: g (gg uu r) t
+
+class IGArrow g (**) u gg (***) uu => IGArrowConstant g (**) u gg (***) uu t r where
+ iga_constant :: g t (gg uu r)
+
+class IGArrow g (**) u gg (***) uu => IGArrowReify g (**) u gg (***) uu x y r q where
+ iga_reify :: g (g x y) (gg r q)
+
+class IGArrow g (**) u gg (***) uu => IGArrowReflect g (**) u gg (***) uu r q x y where
+ iga_reflect :: g (gg r q) (g x y)
+
+
+
+
+
+------------------------------------------------------------------------------
+-- Self-Internal GArrows
+
+--
+-- | A self-internal GArrow is, well, internal to itself
+--
+class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
+
+--
+-- | 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
+--
+-- 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)
+
+
+
+
+
+------------------------------------------------------------------------------
+-- 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
+
+
+
+
+
+
+------------------------------------------------------------------------
+-- 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
+ IGArrow g (**) u q (***) uu =>
+ Ext g (**) u q (***) uu x y
+ = Ext { unExt :: g u (q x y) }
+
+-- 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