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 GHC.HetMet.GArrow
  61 import Prelude hiding ((.), id)
  62
  63 data GArrow g (**) u => Polynomial g (**) u t x y
  64     = L (g (t**x) y)                            -- uses t, wants it as the left arg
  65     | R (g (x**t) y)                            -- uses t, wants it as the right arg
  66     | B (g (t**x) y) (g (x**t) y) -- uses t, doesn't care which arg
  67     | N (g                  x  y)                            -- doesn't use t
  68
  69 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u)  => Category (Polynomial g (**) u t) where
  70   id                  = N id
  71   (N g)    . (N f)    = N $ g . f
  72   (N g)    . (L f)    = L $ g . f
  73   (N g)    . (R f)    = R $ g . f
  74   (N g)    . (B f f') = B (f >>> g) (f' >>> g)
  75   (L g)    . (N f)    = L $ g . ga_second f
  76   (R g)    . (N f)    = R $ g . ga_first  f
  77   (B g g') . (N f)    = B (ga_second f >>> g) (ga_first f >>> g')
  78   (L g)    . (L f)    = L $ ga_first  ga_copy >>> ga_assoc   >>> ga_second              f  >>> g
  79   (L g)    . (B f f') = L $ ga_first  ga_copy >>> ga_assoc   >>> ga_second              f  >>> g
  80   (R g)    . (R f)    = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first               f  >>> g
  81   (B g g') . (R f)    = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first               f  >>> g'
  82   (B g g') . (L f)    = L $ ga_first  ga_copy >>> ga_assoc   >>> ga_second              f  >>> g
  83   (R g)    . (B f f') = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first               f' >>> g
  84   (R g)    . (L f)    = L $ ga_first  ga_copy >>> ga_assoc   >>> ga_second f >>> ga_swap >>> g
  85   (L g)    . (R f)    = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first  f >>> ga_swap >>> g
  86   (B g g') . (B f f') = B (ga_first  ga_copy >>> ga_assoc   >>> ga_second              f  >>> g)
  87                           (ga_second ga_copy >>> ga_unassoc >>> ga_first               f' >>> g')
  88
  89 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrow (Polynomial g (**) u t) (**) u where
  90   ga_first   (N f)   = N $ ga_first f
  91   ga_first   (L f)   = L $ ga_unassoc >>> ga_first f
  92   ga_first   (R f)   = B  (ga_unassoc >>> ga_first (ga_swap >>> f))
  93                           (ga_assoc >>> ga_second ga_swap >>> ga_unassoc >>> ga_first f)
  94   ga_first   (B f _) = L $ ga_unassoc >>> ga_first f
  95   ga_second  (N g)   = N $ ga_second g
  96   ga_second  (L f)   = B  (ga_unassoc   >>> ga_first ga_swap >>> ga_assoc >>> ga_second f)
  97                           (ga_assoc >>> ga_second (ga_swap >>> f))
  98   ga_second  (R g)   = R $ ga_assoc   >>> ga_second g
  99   ga_second  (B _ g) = R $ ga_assoc   >>> ga_second g
 100   ga_cancell         =  N ga_cancell
 101   ga_cancelr         =  N ga_cancelr
 102   ga_uncancell       =  N ga_uncancell
 103   ga_uncancelr       =  N ga_uncancelr
 104   ga_assoc           =  N ga_assoc
 105   ga_unassoc         =  N ga_unassoc
 106
 107 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u)  => GArrowCopy (Polynomial g (**) u t) (**) u
 108  where
 109   ga_copy = N ga_copy
 110
 111 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u)  => GArrowDrop (Polynomial g (**) u t) (**) u
 112  where
 113   ga_drop = N ga_drop
 114
 115 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u)  => GArrowSwap (Polynomial g (**) u t) (**) u
 116  where
 117   ga_swap = N ga_swap
 118
 119 --
 120 -- | Given an **instance-polymorphic** Haskell function @(g () a)->(g b c)@ we can produce
 121 -- a self-contained instance-polymorphic term @(g (a**b) c)@.  The "trick" is that we supply
 122 -- the instance-polymorphic Haskell function with a modified dictionary (type class instance)
 123 --
 124 homfunctor_inv :: forall a b c.
 125     (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c) ->
 126     (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c)
 127 homfunctor_inv f =
 128   case f (B ga_cancelr ga_cancell) of
 129     (N f')   -> ga_first ga_drop >>> ga_cancell >>> f'
 130     (L f')   -> f'
 131     (R f')   -> ga_swap >>> f'
 132     (B f' _) -> f'
 133
 134 --
 135 -- $extradoc1
 136 --
 137 -- A few more comments are in order.  First of all, the function
 138 -- @homfunctor@ above really is a hom-functor; its domain is the
 139 -- category whose objects are Haskell types and whose morphisms a->b
 140 -- are Haskell terms of type @(GArrow g => g a b)@ -- note how the
 141 -- term is polymorphic in @g@.
 142 --
 143 -- This category is Hask-enriched: for each choice of @a@ and @b@, the
 144 -- collection of all morphisms a->b happens to be a Hask-object, and
 145 -- all the other necessary conditions are met.
 146 --
 147 -- I use the term "fully enriched" to mean "enriched such that the
 148 -- hom-functor at the terminal object is a full functor".  For any
 149 -- morphism f whose domain and codomain are in the range of the
 150 -- hom-functor, the function homfunctor_inv above will pick out a
 151 -- morphism in its domain which is sent to f -- it is the witness
 152 -- to the fact that the functor is full.
 153 --