-{-# 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
-- Maintainer : Adam Megacz <megacz@acm.org>
-- 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:
-- 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
) 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
projects / ghc-base.git / commitdiff