--
-- | The instance witnessing contextual closure of GArrowSTKC.
--
--- Module : GHC.HetMet.GArrowKappa
+-- Module : GHC.HetMet.GArrowFullyEnriched
-- Copyright : none
-- License : public domain
--
-- Stability : experimental
-- Portability : portable
-module GHC.HetMet.GArrowKappa (
+module GHC.HetMet.GArrowFullyEnriched (
-- | It's easy to write a function with this type:
--
-- > homfunctor :: (GArrow g (,) () => g a b -> (g () a -> g () b))
-- * Category Theoretic Background
-- $extradoc1
--- * Contextual Completeness
--- $extradoc2
) where
import Control.Category ( (>>>) )
import qualified Control.Category
-- @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) )
+-- 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.
+--
+-- I use the term "fully enriched" to mean "enriched such that the
+-- hom-functor at the terminal object is a full functor". For any
+-- morphism f whose domain and codomain are in the range of the
+-- hom-functor, the function homfunctor_inv above will pick out a
+-- morphism in its domain which is sent to f -- it is the witness
+-- to the fact that the functor is full.
--
projects / ghc-base.git / commitdiff