rename GArrowKappa to GArrowFullyEnriched

[ghc-base.git] / GHC / HetMet / GArrowFullyEnriched.hs

diff --git a/GHC/HetMet/GArrowFullyEnriched.hs b/GHC/HetMet/GArrowFullyEnriched.hs
new file mode 100644 (file)
index 0000000..a18d9a5
--- /dev/null
+++ b/GHC/HetMet/GArrowFullyEnriched.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE RankNTypes, FlexibleInstances, UndecidableInstances, TypeFamilies, MultiParamTypeClasses #-}
+-----------------------------------------------------------------------------
+--
+-- | The instance witnessing contextual closure of GArrowSTKC.
+--
+-- Module      :  GHC.HetMet.GArrowFullyEnriched
+-- Copyright   :  none
+-- License     :  public domain
+--
+-- Maintainer  :  Adam Megacz <megacz@acm.org>
+-- Stability   :  experimental
+-- Portability :  portable
+
+module GHC.HetMet.GArrowFullyEnriched (
+-- | It's easy to write a function with this type:
+--
+-- >  homfunctor :: (GArrow g (,) () => g a b -> (g () a -> g () b))
+--
+-- ... it's nothing more than the precomposition function:
+--
+-- >  homfunctor = (.)
+--
+-- however, writing its *inverse* is not so easy:
+--
+-- >  homfunctor_inv :: (GArrow g (,) () => (g () a -> g () b) -> g a b)
+--
+-- Think about it.  This is saying that every way of turning a @(g ()
+-- a)@ into a @(g () b)@ is equivalent to precomposition, for some
+-- magically-divined value of type @(g a b)@.  That's hard to believe!
+-- In fact, it's flat out false unless we exploit parametricity.  This
+-- module does that, and wraps up all of the magic in an easy-to-use
+-- implementation of homfunctor_inv.
+--
+-- Note that @homfunctor_inv@ needs instances of @GArrowDrop@,
+-- @GArrowCopy@, and @GArrowSwap@ in order to work this magic.
+--
+
+ homfunctor_inv
+
+-- * Category Theoretic Background
+-- $extradoc1
+
+) where
+import Control.Category ( (>>>) )
+import qualified Control.Category
+import GHC.HetMet.GArrow
+
+newtype Polynomial g t x y = Polynomial { unPoly :: g (GArrowTensor g x t) y }
+
+instance GArrowSTKC g => Control.Category.Category (Polynomial g t) where
+  id           = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr }
+  (.) g f      = Polynomial { unPoly = ga_second ga_copy >>> ga_unassoc >>> ga_first (unPoly f) >>> (unPoly g) }
+
+instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrow (Polynomial g t) (**) u where
+  ga_first   f =  Polynomial { unPoly = ga_assoc >>> ga_second ga_swap >>> ga_unassoc >>> ga_first (unPoly f)  }
+  ga_second  f =  Polynomial { unPoly = ga_assoc >>>                                      ga_second (unPoly f) }
+  ga_cancell   =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_cancell   }
+  ga_cancelr   =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_cancelr   }
+  ga_uncancell =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_uncancell }
+  ga_uncancelr =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_uncancelr }
+  ga_assoc     =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_assoc     }
+  ga_unassoc   =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_unassoc   }
+
+type instance GArrowUnit   (Polynomial g t) = GArrowUnit   g
+
+type instance GArrowTensor (Polynomial g t) = GArrowTensor g
+
+instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowDrop (Polynomial g t) (**) u
+ where
+  ga_drop = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_drop   }
+
+instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowCopy (Polynomial g t) (**) u
+ where
+  ga_copy = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_copy   }
+
+instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowSwap (Polynomial g t) (**) u
+ where
+  ga_swap = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_swap   }
+
+instance GArrowSTKC g => GArrowSTKC (Polynomial g t)
+
+--
+-- | Given an **instance-polymorphic** Haskell function @(g () a)->(g () b)@ we can produce
+-- a self-contained instance-polymorphic term @(g a b)@.  The "trick" is that we supply
+-- the instance-polymorphic Haskell function with a modified dictionary (type class instance)
+--
+homfunctor_inv :: (forall g . GArrowSTKC g => g (GArrowUnit g) a -> g (GArrowUnit g) b) ->
+                  (forall g . GArrowSTKC g => g a b)
+homfunctor_inv x = ga_uncancell >>> unPoly (x (Polynomial { unPoly = ga_cancell }))
+
+
+-- $extradoc1
+--
+-- A few more comments are in order.  First of all, the function
+-- @homfunctor@ above really is a hom-functor; its domain is the
+-- category whose objects are Haskell types and whose morphisms a->b
+-- are Haskell terms of type @(GArrow g => g a b)@ -- note how the
+-- term is polymorphic in @g@.
+--
+-- This category is Hask-enriched: for each choice of @a@ and @b@, the
+-- collection of all morphisms a->b happens to be a Hask-object, and
+-- all the other necessary conditions are met.
+--
+-- I use the term "fully enriched" to mean "enriched such that the
+-- hom-functor at the terminal object is a full functor".  For any
+-- morphism f whose domain and codomain are in the range of the
+-- hom-functor, the function homfunctor_inv above will pick out a
+-- morphism in its domain which is sent to f -- it is the witness
+-- to the fact that the functor is full.
+--