GHC/HetMet/GArrowFullyEnriched.hs

   1 {-# OPTIONS -fwarn-incomplete-patterns #-}
   2 {-# LANGUAGE RankNTypes, FlexibleInstances, TypeFamilies, MultiParamTypeClasses, GADTs, DatatypeContexts, TypeOperators #-}
   3 -----------------------------------------------------------------------------
   4 --
   5 -- | The instance witnessing the fact that (forall g . GArrow g => g a b) is fully enriched in Hask.
   6 --
   7 -- Module      :  GHC.HetMet.GArrowFullyEnriched
   8 -- Copyright   :  none
   9 -- License     :  public domain
  10 --
  11 -- Maintainer  :  Adam Megacz <megacz@acm.org>
  12 -- Stability   :  experimental
  13 -- Portability :  portable
  14 --
  15 -- TO DO: not entirely sure that when ga_first/ga_second are applied
  16 -- to a (B f f') that it's always necessarily the right idea to toss
  17 -- out the half which would force us to do a swap.  What if the thing
  18 -- being firsted contains only unit wires?  That might not be
  19 -- possible, since B's necessarily use their argument.
  20 --
  21
  22 module GHC.HetMet.GArrowFullyEnriched (
  23 -- | It's easy to write a function with this type:
  24 --
  25 -- >  homfunctor :: (GArrow g (,) () => g a b -> (g () a -> g () b))
  26 --
  27 -- ... it's nothing more than the precomposition function:
  28 --
  29 -- >  homfunctor = (.)
  30 --
  31 -- however, writing its *inverse* is not so easy:
  32 --
  33 -- >  homfunctor_inv :: (GArrow g (,) () => (g () a -> g () b) -> g a b)
  34 --
  35 -- Think about it.  This is saying that every way of turning a @(g ()
  36 -- a)@ into a @(g () b)@ is equivalent to precomposition, for some
  37 -- magically-divined value of type @(g a b)@.  That's hard to believe!
  38 -- In fact, it's flat out false unless we exploit parametricity.  This
  39 -- module does that, and wraps up all of the magic in an easy-to-use
  40 -- implementation of homfunctor_inv.
  41 --
  42 -- This module actually provides something slightly more general:
  43 --
  44 -- >  homfunctor_inv :: (GArrow g (**) u => (g u a -> g x b) -> g (a**x) b)
  45 --
  46 -- ... where the actual "hom functor" case has x=u
  47 --
  48 -- Note that @homfunctor_inv@ needs instances of @GArrowDrop@,
  49 -- @GArrowCopy@, and @GArrowSwap@ in order to work this magic.
  50 -- However, ga_drop/ga_copy/ga_swap will only be used if necessary.
  51 --
  52
  53  homfunctor_inv
  54
  55 -- * Category Theoretic Background
  56 -- $extradoc1
  57
  58 ) where
  59 import Control.Category ( (>>>) )
  60 import Control.Category
  61 import GHC.HetMet.GArrow
  62 import Prelude hiding ((.), id)
  63
  64 data (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u)  => Polynomial g (**) u t x y
  65     = L (g (t**x) y)                            -- uses t, wants it as the left arg
  66     | R (g (x**t) y)                            -- uses t, wants it as the right arg
  67     | B (g (t**x) y) (g (x**t) y) -- uses t, doesn't care which arg
  68     | N (g                  x  y)                            -- doesn't use t
  69
  70 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u)  => Category (Polynomial g (**) u t) where
  71   id                  = N id
  72   (N g)    . (N f)    = N $ g . f
  73   (N g)    . (L f)    = L $ g . f
  74   (N g)    . (R f)    = R $ g . f
  75   (N g)    . (B f f') = B (f >>> g) (f' >>> g)
  76   (L g)    . (N f)    = L $ g . ga_second f
  77   (R g)    . (N f)    = R $ g . ga_first  f
  78   (B g g') . (N f)    = B (ga_second f >>> g) (ga_first f >>> g')
  79   (L g)    . (L f)    = L $ ga_first  ga_copy >>> ga_assoc   >>> ga_second              f  >>> g
  80   (L g)    . (B f f') = L $ ga_first  ga_copy >>> ga_assoc   >>> ga_second              f  >>> g
  81   (R g)    . (R f)    = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first               f  >>> g
  82   (B g g') . (R f)    = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first               f  >>> g'
  83   (B g g') . (L f)    = L $ ga_first  ga_copy >>> ga_assoc   >>> ga_second              f  >>> g
  84   (R g)    . (B f f') = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first               f' >>> g
  85   (R g)    . (L f)    = L $ ga_first  ga_copy >>> ga_assoc   >>> ga_second f >>> ga_swap >>> g
  86   (L g)    . (R f)    = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first  f >>> ga_swap >>> g
  87   (B g g') . (B f f') = B (ga_first  ga_copy >>> ga_assoc   >>> ga_second              f  >>> g)
  88                           (ga_second ga_copy >>> ga_unassoc >>> ga_first               f' >>> g')
  89
  90 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrow (Polynomial g (**) u t) (**) u where
  91   ga_first   (N f)   = N $ ga_first f
  92   ga_first   (L f)   = L $ ga_unassoc >>> ga_first f
  93   ga_first   (R f)   = B  (ga_unassoc >>> ga_first (ga_swap >>> f))
  94                           (ga_assoc >>> ga_second ga_swap >>> ga_unassoc >>> ga_first f)
  95   ga_first   (B f _) = L $ ga_unassoc >>> ga_first f
  96   ga_second  (N g)   = N $ ga_second g
  97   ga_second  (L f)   = B  (ga_unassoc   >>> ga_first ga_swap >>> ga_assoc >>> ga_second f)
  98                           (ga_assoc >>> ga_second (ga_swap >>> f))
  99   ga_second  (R g)   = R $ ga_assoc   >>> ga_second g
 100   ga_second  (B _ g) = R $ ga_assoc   >>> ga_second g
 101   ga_cancell         =  N ga_cancell
 102   ga_cancelr         =  N ga_cancelr
 103   ga_uncancell       =  N ga_uncancell
 104   ga_uncancelr       =  N ga_uncancelr
 105   ga_assoc           =  N ga_assoc
 106   ga_unassoc         =  N ga_unassoc
 107
 108 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u)  => GArrowCopy (Polynomial g (**) u t) (**) u
 109  where
 110   ga_copy = N ga_copy
 111
 112 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u)  => GArrowDrop (Polynomial g (**) u t) (**) u
 113  where
 114   ga_drop = N ga_drop
 115
 116 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u)  => GArrowSwap (Polynomial g (**) u t) (**) u
 117  where
 118   ga_swap = N ga_swap
 119
 120 --
 121 -- | Given an **instance-polymorphic** Haskell function @(g () a)->(g b c)@ we can produce
 122 -- a self-contained instance-polymorphic term @(g (a**b) c)@.  The "trick" is that we supply
 123 -- the instance-polymorphic Haskell function with a modified dictionary (type class instance)
 124 --
 125 homfunctor_inv :: forall a b c.
 126     (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c) ->
 127     (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c)
 128 homfunctor_inv f =
 129   case f (B ga_cancelr ga_cancell) of
 130     (N f')   -> ga_first ga_drop >>> ga_cancell >>> f'
 131     (L f')   -> f'
 132     (R f')   -> ga_swap >>> f'
 133     (B f' _) -> f'
 134
 135 --
 136 -- $extradoc1
 137 --
 138 -- A few more comments are in order.  First of all, the function
 139 -- @homfunctor@ above really is a hom-functor; its domain is the
 140 -- category whose objects are Haskell types and whose morphisms a->b
 141 -- are Haskell terms of type @(GArrow g => g a b)@ -- note how the
 142 -- term is polymorphic in @g@.
 143 --
 144 -- This category is Hask-enriched: for each choice of @a@ and @b@, the
 145 -- collection of all morphisms a->b happens to be a Hask-object, and
 146 -- all the other necessary conditions are met.
 147 --
 148 -- I use the term "fully enriched" to mean "enriched such that the
 149 -- hom-functor at the terminal object is a full functor".  For any
 150 -- morphism f whose domain and codomain are in the range of the
 151 -- hom-functor, the function homfunctor_inv above will pick out a
 152 -- morphism in its domain which is sent to f -- it is the witness
 153 -- to the fact that the functor is full.
 154 --