add IGArrow: internal GArrows

diff --git a/GHC/HetMet/IGArrow.hs b/GHC/HetMet/IGArrow.hs
new file mode 100644 (file)
index 0000000..cc6bd04
--- /dev/null
+++ b/GHC/HetMet/IGArrow.hs
@@ -0,0 +1,180 @@
+{-# 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