--- /dev/null
+{-# LANGUAGE RankNTypes, FlexibleInstances, UndecidableInstances, TypeFamilies, MultiParamTypeClasses #-}
+-----------------------------------------------------------------------------
+--
+-- | The instance witnessing contextual closure of GArrowSTKC.
+--
+-- Module : GHC.HetMet.GArrowKappa
+-- Copyright : none
+-- License : public domain
+--
+-- Maintainer : Adam Megacz <megacz@acm.org>
+-- Stability : experimental
+-- Portability : portable
+
+module GHC.HetMet.GArrowKappa (
+-- | 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
+
+-- * Contextual Completeness
+-- $extradoc2
+) 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.
+--
+
+-- $extradoc2
+--
+-- Material below is in flux; take with a grain of salt...
+--
+-- A category C with a terminal object 1 is *contextually complete* if
+-- choosing an object x of C and freely adjoining and "opaque"
+-- morphism 1->x to form a __polynomial category__ C[x] it is the case
+-- that C[x] can be "represented in" C. The technical definition of
+-- "represented in" is that the inclusion functor C->C[x] have a left
+-- adjoint. This left adjoint kappa_x:C[x]->C has the property that
+--
+-- > C(kappa_x(a),b) \cong C[x](a,b)
+--
+-- See Hasegawa, __Decomposing typed lambda calculus into a
+-- couple of categorical programming languages__.
+--
+-- Most notions in category theory come in both ordinary and enriched
+-- versions. I'm not aware of an enriched version of contextual
+-- closure, it ought to be something along the lines of saying
+-- that, for C a V-enriched category, V(C(1,a),C(x,y)) is isomorphic
+-- (as a V-object) to V(1,C(a**x,y)). When x=1 this is exactly the
+-- same thing as saying that hom(1,-):C->V is a full and faithful functor.
+--
+-- Usually C is monoidal and a morphism a->b in C[x] is "represented
+-- by" a morphism (a**x)->b in C where (**) is the monoidal tensor.
+-- Contextual closure is a way of saying that the tensor of C can
+-- represent contexts -- that a morphism into (a**x) is just as good
+-- as a morphism into a in C[x].
+--
+--
+-- Since every contextually complete
+--
+-- Most notions in category theory come in both ordinary and enriched
+-- versions. I'm not aware of an enriched version of contextual
+-- closure, but consider this: if both C and C[x] are Sets-enriched,
+-- (i.e., ordinary categories) we know that
+--
+-- > C[x](a,b) \sqsubset Sets( C(1,x) , C(a,b) )
+--
+-- where \sqsubset means "embeds in" -- in this case, as a
+-- Sets-object. Think about it; the construction of C[x] dictates
+-- that its morphisms a->b are nothing more than strategies for
+-- building a C-morphism a->b using a free 1->x morphism as a
+-- parameter. You're only allowed to use composition and other
+-- categorical tools for putting together this strategy, so the
+-- relationship above is just an embedding -- there might be
+-- paradoxical mappings from C(1,x) to C(a,b) that don't arise as the
+-- result of sensible constructions.
+--
+-- I claim that the embedding above, with V substituted for Sets,
+-- should hold for any sensible definition of enriched contextual
+-- completeness:
+--
+-- > V( 1 , C[x](a,b) ) \sqsubset V( C(1,x) , C(a,b) )
+--
+-- substituting the isomorphism above, we get:
+--
+-- > V( 1 , C(kappa_x(a),b) ) \sqsubset V( C(1,x) , C(a,b) )
+--
+-- Now, let a=1 and we have:
+--
+-- > V( 1 , C(kappa_x(1),b) ) \sqsubset V( C(1,x) , C(1,b) )
+--
+-- If kappa_x(1) \cong x then
+--
+-- > V( 1 , C(x,b) ) \sqsubset V( C(1,x) , C(1,b) )
+--
projects / ghc-base.git / commitdiff