From fe3e9a061c212b2c9f83e31632236afcaacacb81 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 19 Jun 2011 19:01:02 -0700 Subject: [PATCH] rename GArrowKappa to GArrowFullyEnriched --- GHC/HetMet/GArrow.hs | 15 +--- .../{GArrowKappa.hs => GArrowFullyEnriched.hs} | 90 +++----------------- base.cabal | 2 +- 3 files changed, 17 insertions(+), 90 deletions(-) rename GHC/HetMet/{GArrowKappa.hs => GArrowFullyEnriched.hs} (57%) diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs index 8b88b9b..9878a4d 100644 --- a/GHC/HetMet/GArrow.hs +++ b/GHC/HetMet/GArrow.hs @@ -34,7 +34,6 @@ module GHC.HetMet.GArrow ( GArrowUnit, GArrowExponent, - GArrowKappa(..), GArrowSTKC(..), GArrowSTKCL(..), GArrowSTLC(..), @@ -135,6 +134,8 @@ class GArrow g (**) u => GArrowConstant g (**) u t r where + + ------------------------------------------------------------------------ -- Reify and Reflect, which are "curried" versions of eval/const @@ -150,18 +151,6 @@ class GArrow g (**) u => GArrowReflect g (**) u r q x y where ------------------------------------------------------------------------- --- The Kappa adjunction --- --- See Hasegawa, Decomposing Typed Lambda Calculus into a Couple of --- Categorical Programming Languages) section 3, rule $(\times L)$ - -class GArrow g (**) u => GArrowKappa g (**) u where - ga_kappa :: (g u x -> g u y) -> g x y - - - - ------------------------------------------------------------------------ -- Apply and Curry diff --git a/GHC/HetMet/GArrowKappa.hs b/GHC/HetMet/GArrowFullyEnriched.hs similarity index 57% rename from GHC/HetMet/GArrowKappa.hs rename to GHC/HetMet/GArrowFullyEnriched.hs index 12b8021..a18d9a5 100644 --- a/GHC/HetMet/GArrowKappa.hs +++ b/GHC/HetMet/GArrowFullyEnriched.hs @@ -3,7 +3,7 @@ -- -- | The instance witnessing contextual closure of GArrowSTKC. -- --- Module : GHC.HetMet.GArrowKappa +-- Module : GHC.HetMet.GArrowFullyEnriched -- Copyright : none -- License : public domain -- @@ -11,7 +11,7 @@ -- 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)) @@ -40,8 +40,6 @@ module GHC.HetMet.GArrowKappa ( -- * Category Theoretic Background -- $extradoc1 --- * Contextual Completeness --- $extradoc2 ) where import Control.Category ( (>>>) ) import qualified Control.Category @@ -97,76 +95,16 @@ homfunctor_inv x = ga_uncancell >>> unPoly (x (Polynomial { unPoly = ga_cancell -- @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. -- diff --git a/base.cabal b/base.cabal index e53a282..258c142 100644 --- a/base.cabal +++ b/base.cabal @@ -59,9 +59,9 @@ Library { GHC.HetMet, GHC.HetMet.CodeTypes, GHC.HetMet.GArrow, - GHC.HetMet.GArrowKappa, GHC.HetMet.GArrowFullyEnriched, GHC.HetMet.GuestLanguage, + GHC.HetMet.IGArrow, GHC.HetMet.Private, GHC.HetMet.Arrow, GHC.MVar, -- 1.7.10.4