GHC/HetMet/GArrowKappa.hs

   1 {-# LANGUAGE RankNTypes, FlexibleInstances, UndecidableInstances, TypeFamilies, MultiParamTypeClasses #-}
   2 -----------------------------------------------------------------------------
   3 --
   4 -- | The instance witnessing contextual closure of GArrowSTKC.
   5 --
   6 -- Module      :  GHC.HetMet.GArrowKappa
   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.GArrowKappa (
  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 -- * Contextual Completeness
  44 -- $extradoc2
  45 ) where
  46 import Control.Category ( (>>>) )
  47 import qualified Control.Category
  48 import GHC.HetMet.GArrow
  49
  50 newtype Polynomial g t x y = Polynomial { unPoly :: g (GArrowTensor g x t) y }
  51
  52 instance GArrowSTKC g => Control.Category.Category (Polynomial g t) where
  53   id           = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr }
  54   (.) g f      = Polynomial { unPoly = ga_second ga_copy >>> ga_unassoc >>> ga_first (unPoly f) >>> (unPoly g) }
  55
  56 instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrow (Polynomial g t) (**) u where
  57   ga_first   f =  Polynomial { unPoly = ga_assoc >>> ga_second ga_swap >>> ga_unassoc >>> ga_first (unPoly f)  }
  58   ga_second  f =  Polynomial { unPoly = ga_assoc >>>                                      ga_second (unPoly f) }
  59   ga_cancell   =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_cancell   }
  60   ga_cancelr   =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_cancelr   }
  61   ga_uncancell =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_uncancell }
  62   ga_uncancelr =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_uncancelr }
  63   ga_assoc     =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_assoc     }
  64   ga_unassoc   =  Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_unassoc   }
  65
  66 type instance GArrowUnit   (Polynomial g t) = GArrowUnit   g
  67
  68 type instance GArrowTensor (Polynomial g t) = GArrowTensor g
  69
  70 instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowDrop (Polynomial g t) (**) u
  71  where
  72   ga_drop = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_drop   }
  73
  74 instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowCopy (Polynomial g t) (**) u
  75  where
  76   ga_copy = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_copy   }
  77
  78 instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowSwap (Polynomial g t) (**) u
  79  where
  80   ga_swap = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_swap   }
  81
  82 instance GArrowSTKC g => GArrowSTKC (Polynomial g t)
  83
  84 --
  85 -- | Given an **instance-polymorphic** Haskell function @(g () a)->(g () b)@ we can produce
  86 -- a self-contained instance-polymorphic term @(g a b)@.  The "trick" is that we supply
  87 -- the instance-polymorphic Haskell function with a modified dictionary (type class instance)
  88 --
  89 homfunctor_inv :: (forall g . GArrowSTKC g => g (GArrowUnit g) a -> g (GArrowUnit g) b) ->
  90                   (forall g . GArrowSTKC g => g a b)
  91 homfunctor_inv x = ga_uncancell >>> unPoly (x (Polynomial { unPoly = ga_cancell }))
  92
  93
  94 -- $extradoc1
  95 --
  96 -- A few more comments are in order.  First of all, the function
  97 -- @homfunctor@ above really is a hom-functor; its domain is the
  98 -- category whose objects are Haskell types and whose morphisms a->b
  99 -- are Haskell terms of type @(GArrow g => g a b)@ -- note how the
 100 -- term is polymorphic in @g@.  This category is Hask-enriched: for
 101 -- each choice of @a@ and @b@, the collection of all morphisms a->b
 102 -- happens to be a Hask-object, and all the other necessary conditions
 103 -- are met.
 104 --
 105
 106 -- $extradoc2
 107 --
 108 -- Material below is in flux; take with a grain of salt...
 109 --
 110 -- A category C with a terminal object 1 is *contextually complete* if
 111 -- choosing an object x of C and freely adjoining and "opaque"
 112 -- morphism 1->x to form a __polynomial category__ C[x] it is the case
 113 -- that C[x] can be "represented in" C.  The technical definition of
 114 -- "represented in" is that the inclusion functor C->C[x] have a left
 115 -- adjoint.  This left adjoint kappa_x:C[x]->C has the property that
 116 --
 117 -- >   C(kappa_x(a),b)   \cong   C[x](a,b)
 118 --
 119 -- See Hasegawa, __Decomposing typed lambda calculus into a
 120 -- couple of categorical programming languages__.
 121 --
 122 -- Most notions in category theory come in both ordinary and enriched
 123 -- versions.  I'm not aware of an enriched version of contextual
 124 -- closure, it ought to be something along the lines of saying
 125 -- that, for C a V-enriched category, V(C(1,a),C(x,y)) is isomorphic
 126 -- (as a V-object) to V(1,C(a**x,y)).  When x=1 this is exactly the
 127 -- same thing as saying that hom(1,-):C->V is a full and faithful functor.
 128 --
 129 -- Usually C is monoidal and a morphism a->b in C[x] is "represented
 130 -- by" a morphism (a**x)->b in C where (**) is the monoidal tensor.
 131 -- Contextual closure is a way of saying that the tensor of C can
 132 -- represent contexts -- that a morphism into (a**x) is just as good
 133 -- as a morphism into a in C[x].
 134 --
 135 --
 136 -- Since every contextually complete
 137 --
 138 -- Most notions in category theory come in both ordinary and enriched
 139 -- versions.  I'm not aware of an enriched version of contextual
 140 -- closure, but consider this: if both C and C[x] are Sets-enriched,
 141 -- (i.e., ordinary categories) we know that
 142 --
 143 -- >   C[x](a,b) \sqsubset  Sets( C(1,x) , C(a,b) )
 144 --
 145 -- where \sqsubset means "embeds in" -- in this case, as a
 146 -- Sets-object.  Think about it; the construction of C[x] dictates
 147 -- that its morphisms a->b are nothing more than strategies for
 148 -- building a C-morphism a->b using a free 1->x morphism as a
 149 -- parameter.  You're only allowed to use composition and other
 150 -- categorical tools for putting together this strategy, so the
 151 -- relationship above is just an embedding -- there might be
 152 -- paradoxical mappings from C(1,x) to C(a,b) that don't arise as the
 153 -- result of sensible constructions.
 154 --
 155 -- I claim that the embedding above, with V substituted for Sets,
 156 -- should hold for any sensible definition of enriched contextual
 157 -- completeness:
 158 --
 159 -- > V( 1 , C[x](a,b) )  \sqsubset  V( C(1,x) , C(a,b) )
 160 --
 161 -- substituting the isomorphism above, we get:
 162 --
 163 -- > V( 1 , C(kappa_x(a),b) )  \sqsubset  V( C(1,x) , C(a,b) )
 164 --
 165 -- Now, let a=1 and we have:
 166 --
 167 -- > V( 1 , C(kappa_x(1),b) )  \sqsubset  V( C(1,x) , C(1,b) )
 168 --
 169 -- If kappa_x(1) \cong x then
 170 --
 171 -- > V( 1 , C(x,b) )  \sqsubset  V( C(1,x) , C(1,b) )
 172 --