From 79a3cdc8b8015f9e6825b88401d0bbdd1d2d8ac4 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 20 Jun 2011 20:04:02 -0700 Subject: [PATCH] GArrowFullyEnriched: better algorithm, avoids drop/copy/swap --- GHC/HetMet/GArrowFullyEnriched.hs | 120 +++++++++++++++++++++++++------------ 1 file changed, 82 insertions(+), 38 deletions(-) diff --git a/GHC/HetMet/GArrowFullyEnriched.hs b/GHC/HetMet/GArrowFullyEnriched.hs index a18d9a5..66b1ab7 100644 --- a/GHC/HetMet/GArrowFullyEnriched.hs +++ b/GHC/HetMet/GArrowFullyEnriched.hs @@ -1,7 +1,8 @@ -{-# LANGUAGE RankNTypes, FlexibleInstances, UndecidableInstances, TypeFamilies, MultiParamTypeClasses #-} +{-# OPTIONS -fwarn-incomplete-patterns #-} +{-# LANGUAGE RankNTypes, FlexibleInstances, TypeFamilies, MultiParamTypeClasses, GADTs, DatatypeContexts, TypeOperators, UndecidableInstances #-} ----------------------------------------------------------------------------- -- --- | The instance witnessing contextual closure of GArrowSTKC. +-- | The instance witnessing the fact that (forall g . GArrow g => g a b) is fully enriched in Hask. -- -- Module : GHC.HetMet.GArrowFullyEnriched -- Copyright : none @@ -10,6 +11,13 @@ -- Maintainer : Adam Megacz -- Stability : experimental -- Portability : portable +-- +-- TO DO: not entirely sure that when ga_first/ga_second are applied +-- to a (B f f') that it's always necessarily the right idea to toss +-- out the half which would force us to do a swap. What if the thing +-- being firsted contains only unit wires? That might not be +-- possible, since B's necessarily use their argument. +-- module GHC.HetMet.GArrowFullyEnriched ( -- | It's easy to write a function with this type: @@ -31,8 +39,15 @@ module GHC.HetMet.GArrowFullyEnriched ( -- module does that, and wraps up all of the magic in an easy-to-use -- implementation of homfunctor_inv. -- +-- This module actually provides something slightly more general: +-- +-- > homfunctor_inv :: (GArrow g (**) u => (g u a -> g x b) -> g (a**x) b) +-- +-- ... where the actual "hom functor" case has x=u +-- -- Note that @homfunctor_inv@ needs instances of @GArrowDrop@, -- @GArrowCopy@, and @GArrowSwap@ in order to work this magic. +-- However, ga_drop/ga_copy/ga_swap will only be used if necessary. -- homfunctor_inv @@ -42,53 +57,82 @@ module GHC.HetMet.GArrowFullyEnriched ( ) where import Control.Category ( (>>>) ) -import qualified Control.Category +import 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 +import Prelude hiding ((.), id) + +data GArrow g (**) u => Polynomial g (**) u t x y + = L (g (t**x) y) -- uses t, wants it as the left arg + | R (g (x**t) y) -- uses t, wants it as the right arg + | B (g (t**x) y) (g (x**t) y) -- uses t, doesn't care which arg + | N (g x y) -- doesn't use t + +instance (GArrowCopy g (**) u, GArrowSwap g (**) u) => Category (Polynomial g (**) u t) where + id = N id + (N g) . (N f) = N $ g . f + (N g) . (L f) = L $ g . f + (N g) . (R f) = R $ g . f + (N g) . (B f f') = B (f >>> g) (f' >>> g) + (L g) . (N f) = L $ g . ga_second f + (R g) . (N f) = R $ g . ga_first f + (B g g') . (N f) = B (ga_second f >>> g) (ga_first f >>> g') + (L g) . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g + (L g) . (B f f') = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g + (R g) . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> g + (B g g') . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> g' + (B g g') . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g + (R g) . (B f f') = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f' >>> g + (R g) . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> ga_swap >>> g + (L g) . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> ga_swap >>> g + (B g g') . (B f f') = B (ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g) + (ga_second ga_copy >>> ga_unassoc >>> ga_first f' >>> g') + +instance (GArrowCopy g (**) u, GArrowSwap g (**) u) => GArrow (Polynomial g (**) u t) (**) u where + ga_first (N f) = N $ ga_first f + ga_first (L f) = L $ ga_unassoc >>> ga_first f + ga_first (R f) = B (ga_unassoc >>> ga_first (ga_swap >>> f)) + (ga_assoc >>> ga_second ga_swap >>> ga_unassoc >>> ga_first f) + ga_first (B f _) = L $ ga_unassoc >>> ga_first f + ga_second (N g) = N $ ga_second g + ga_second (L f) = B (ga_unassoc >>> ga_first ga_swap >>> ga_assoc >>> ga_second f) + (ga_assoc >>> ga_second (ga_swap >>> f)) + ga_second (R g) = R $ ga_assoc >>> ga_second g + ga_second (B _ g) = R $ ga_assoc >>> ga_second g + ga_cancell = N ga_cancell + ga_cancelr = N ga_cancelr + ga_uncancell = N ga_uncancell + ga_uncancelr = N ga_uncancelr + ga_assoc = N ga_assoc + ga_unassoc = N ga_unassoc + +instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowCopy (Polynomial g (**) u t) (**) u where - ga_drop = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_drop } + ga_copy = N ga_copy -instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowCopy (Polynomial g t) (**) u +instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowDrop (Polynomial g (**) u t) (**) u where - ga_copy = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_copy } + ga_drop = N ga_drop -instance (GArrowSTKC g, (GArrowTensor g) ~ (**), (GArrowUnit g) ~ u) => GArrowSwap (Polynomial g t) (**) u +instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowSwap (Polynomial g (**) u t) (**) u where - ga_swap = Polynomial { unPoly = ga_second ga_drop >>> ga_cancelr >>> ga_swap } - -instance GArrowSTKC g => GArrowSTKC (Polynomial g t) + ga_swap = N ga_swap -- --- | 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 +-- | Given an **instance-polymorphic** Haskell function @(g () a)->(g b c)@ we can produce +-- a self-contained instance-polymorphic term @(g (a**b) c)@. 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 })) - +homfunctor_inv :: forall a b c u . + (forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c) -> + (forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c) +homfunctor_inv f = + case f (B ga_cancelr ga_cancell) of + (N f') -> ga_first ga_drop >>> ga_cancell >>> f' + (L f') -> f' + (R f') -> ga_swap >>> f' + (B f' _) -> f' +-- -- $extradoc1 -- -- A few more comments are in order. First of all, the function -- 1.7.10.4