GHC/HetMet/GArrowFullyEnriched.hs

   1 {-# LANGUAGE RankNTypes, FlexibleInstances, UndecidableInstances, TypeFamilies, MultiParamTypeClasses #-}
   2 -----------------------------------------------------------------------------
   3 --
   4 -- | The instance witnessing contextual closure of GArrowSTKC.
   5 --
   6 -- Module      :  GHC.HetMet.GArrowFullyEnriched
   7 -- Copyright   :  none
   8 -- License     :  public domain
   9 --
  10 -- Maintainer  :  Adam Megacz <megacz@acm.org>
  11 -- Stability   :  experimental
  12 -- Portability :  portable
  13
  14 module GHC.HetMet.GArrowFullyEnriched (
  15 -- | It's easy to write a function with this type:
  16 --
  17 -- >  homfunctor :: (GArrow g (,) () => g a b -> (g () a -> g () b))
  18 --
  19 -- ... it's nothing more than the precomposition function:
  20 --
  21 -- >  homfunctor = (.)
  22 --
  23 -- however, writing its *inverse* is not so easy:
  24 --
  25 -- >  homfunctor_inv :: (GArrow g (,) () => (g () a -> g () b) -> g a b)
  26 --
  27 -- Think about it.  This is saying that every way of turning a @(g ()
  28 -- a)@ into a @(g () b)@ is equivalent to precomposition, for some
  29 -- magically-divined value of type @(g a b)@.  That's hard to believe!
  30 -- In fact, it's flat out false unless we exploit parametricity.  This
  31 -- module does that, and wraps up all of the magic in an easy-to-use
  32 -- implementation of homfunctor_inv.
  33 --
  34 -- Note that @homfunctor_inv@ needs instances of @GArrowDrop@,
  35 -- @GArrowCopy@, and @GArrowSwap@ in order to work this magic.
  36 --
  37
  38  homfunctor_inv
  39
  40 -- * Category Theoretic Background
  41 -- $extradoc1
  42
  43 ) where
  44 import Control.Category ( (>>>) )
  45 import qualified Control.Category
  46 import GHC.HetMet.GArrow
  47
  48 newtype Polynomial g t x y = Polynomial { unPoly :: g (GArrowTensor g x t) y }
  49
  50 instance GArrowSTKC g => Control.Category.Category (Polynomial g t) where
  51   id           = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr }
  52   (.) g f      = Polynomial { unPoly = ga_second ga_copy >>> ga_unassoc >>> ga_first (unPoly f) >>> (unPoly g) }
  53
  54 instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrow (Polynomial g t) (**) u where
  55   ga_first   f =  Polynomial { unPoly = ga_assoc >>> ga_second ga_swap >>> ga_unassoc >>> ga_first (unPoly f)  }
  56   ga_second  f =  Polynomial { unPoly = ga_assoc >>>                                      ga_second (unPoly f) }
  57   ga_cancell   =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_cancell   }
  58   ga_cancelr   =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_cancelr   }
  59   ga_uncancell =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_uncancell }
  60   ga_uncancelr =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_uncancelr }
  61   ga_assoc     =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_assoc     }
  62   ga_unassoc   =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_unassoc   }
  63
  64 type instance GArrowUnit   (Polynomial g t) = GArrowUnit   g
  65
  66 type instance GArrowTensor (Polynomial g t) = GArrowTensor g
  67
  68 instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowDrop (Polynomial g t) (**) u
  69  where
  70   ga_drop = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_drop   }
  71
  72 instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowCopy (Polynomial g t) (**) u
  73  where
  74   ga_copy = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_copy   }
  75
  76 instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowSwap (Polynomial g t) (**) u
  77  where
  78   ga_swap = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_swap   }
  79
  80 instance GArrowSTKC g => GArrowSTKC (Polynomial g t)
  81
  82 --
  83 -- | Given an **instance-polymorphic** Haskell function @(g () a)->(g () b)@ we can produce
  84 -- a self-contained instance-polymorphic term @(g a b)@.  The "trick" is that we supply
  85 -- the instance-polymorphic Haskell function with a modified dictionary (type class instance)
  86 --
  87 homfunctor_inv :: (forall g . GArrowSTKC g => g (GArrowUnit g) a -> g (GArrowUnit g) b) ->
  88                   (forall g . GArrowSTKC g => g a b)
  89 homfunctor_inv x = ga_uncancell >>> unPoly (x (Polynomial { unPoly = ga_cancell }))
  90
  91
  92 -- $extradoc1
  93 --
  94 -- A few more comments are in order.  First of all, the function
  95 -- @homfunctor@ above really is a hom-functor; its domain is the
  96 -- category whose objects are Haskell types and whose morphisms a->b
  97 -- are Haskell terms of type @(GArrow g => g a b)@ -- note how the
  98 -- term is polymorphic in @g@.
  99 --
 100 -- This category is Hask-enriched: for each choice of @a@ and @b@, the
 101 -- collection of all morphisms a->b happens to be a Hask-object, and
 102 -- all the other necessary conditions are met.
 103 --
 104 -- I use the term "fully enriched" to mean "enriched such that the
 105 -- hom-functor at the terminal object is a full functor".  For any
 106 -- morphism f whose domain and codomain are in the range of the
 107 -- hom-functor, the function homfunctor_inv above will pick out a
 108 -- morphism in its domain which is sent to f -- it is the witness
 109 -- to the fact that the functor is full.
 110 --