From b7c693b08eb2dcce4666a2c55c7ed52f1e8e7cea Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Tue, 31 May 2011 15:00:04 -0700 Subject: [PATCH] add GArrowKappa --- GHC/HetMet/GArrowKappa.hs | 172 +++++++++++++++++++++++++++++++++++++++++++++ base.cabal | 1 + 2 files changed, 173 insertions(+) create mode 100644 GHC/HetMet/GArrowKappa.hs diff --git a/GHC/HetMet/GArrowKappa.hs b/GHC/HetMet/GArrowKappa.hs new file mode 100644 index 0000000..12b8021 --- /dev/null +++ b/GHC/HetMet/GArrowKappa.hs @@ -0,0 +1,172 @@ +{-# 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 +-- 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) ) +-- diff --git a/base.cabal b/base.cabal index 628b992..dbba7cc 100644 --- a/base.cabal +++ b/base.cabal @@ -59,6 +59,7 @@ Library { GHC.HetMet, GHC.HetMet.CodeTypes, GHC.HetMet.GArrow, + GHC.HetMet.GArrowKappa, GHC.HetMet.GArrowInstances, GHC.HetMet.Private, GHC.HetMet.Arrow, -- 1.7.10.4