1 {-# OPTIONS -fwarn-incomplete-patterns #-}
2 {-# LANGUAGE RankNTypes, FlexibleInstances, TypeFamilies, MultiParamTypeClasses, GADTs, DatatypeContexts, TypeOperators #-}
3 -----------------------------------------------------------------------------
5 -- | The instance witnessing the fact that (forall g . GArrow g => g a b) is fully enriched in Hask.
7 -- Module : GHC.HetMet.GArrowFullyEnriched
9 -- License : public domain
11 -- Maintainer : Adam Megacz <megacz@acm.org>
12 -- Stability : experimental
13 -- Portability : portable
15 -- TO DO: not entirely sure that when ga_first/ga_second are applied
16 -- to a (B f f') that it's always necessarily the right idea to toss
17 -- out the half which would force us to do a swap. What if the thing
18 -- being firsted contains only unit wires? That might not be
19 -- possible, since B's necessarily use their argument.
22 module GHC.HetMet.GArrowFullyEnriched (
23 -- | It's easy to write a function with this type:
25 -- > homfunctor :: (GArrow g (,) () => g a b -> (g () a -> g () b))
27 -- ... it's nothing more than the precomposition function:
31 -- however, writing its *inverse* is not so easy:
33 -- > homfunctor_inv :: (GArrow g (,) () => (g () a -> g () b) -> g a b)
35 -- Think about it. This is saying that every way of turning a @(g ()
36 -- a)@ into a @(g () b)@ is equivalent to precomposition, for some
37 -- magically-divined value of type @(g a b)@. That's hard to believe!
38 -- In fact, it's flat out false unless we exploit parametricity. This
39 -- module does that, and wraps up all of the magic in an easy-to-use
40 -- implementation of homfunctor_inv.
42 -- This module actually provides something slightly more general:
44 -- > homfunctor_inv :: (GArrow g (**) u => (g u a -> g x b) -> g (a**x) b)
46 -- ... where the actual "hom functor" case has x=u
48 -- Note that @homfunctor_inv@ needs instances of @GArrowDrop@,
49 -- @GArrowCopy@, and @GArrowSwap@ in order to work this magic.
50 -- However, ga_drop/ga_copy/ga_swap will only be used if necessary.
55 -- * Category Theoretic Background
59 import Control.Category ( (>>>) )
60 import Control.Category
61 import GHC.HetMet.GArrow
62 import Prelude hiding ((.), id)
64 data (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => Polynomial g (**) u t x y
65 = L (g (t**x) y) -- uses t, wants it as the left arg
66 | R (g (x**t) y) -- uses t, wants it as the right arg
67 | B (g (t**x) y) (g (x**t) y) -- uses t, doesn't care which arg
68 | N (g x y) -- doesn't use t
70 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => Category (Polynomial g (**) u t) where
72 (N g) . (N f) = N $ g . f
73 (N g) . (L f) = L $ g . f
74 (N g) . (R f) = R $ g . f
75 (N g) . (B f f') = B (f >>> g) (f' >>> g)
76 (L g) . (N f) = L $ g . ga_second f
77 (R g) . (N f) = R $ g . ga_first f
78 (B g g') . (N f) = B (ga_second f >>> g) (ga_first f >>> g')
79 (L g) . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g
80 (L g) . (B f f') = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g
81 (R g) . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> g
82 (B g g') . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> g'
83 (B g g') . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g
84 (R g) . (B f f') = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f' >>> g
85 (R g) . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> ga_swap >>> g
86 (L g) . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> ga_swap >>> g
87 (B g g') . (B f f') = B (ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g)
88 (ga_second ga_copy >>> ga_unassoc >>> ga_first f' >>> g')
90 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrow (Polynomial g (**) u t) (**) u where
91 ga_first (N f) = N $ ga_first f
92 ga_first (L f) = L $ ga_unassoc >>> ga_first f
93 ga_first (R f) = B (ga_unassoc >>> ga_first (ga_swap >>> f))
94 (ga_assoc >>> ga_second ga_swap >>> ga_unassoc >>> ga_first f)
95 ga_first (B f _) = L $ ga_unassoc >>> ga_first f
96 ga_second (N g) = N $ ga_second g
97 ga_second (L f) = B (ga_unassoc >>> ga_first ga_swap >>> ga_assoc >>> ga_second f)
98 (ga_assoc >>> ga_second (ga_swap >>> f))
99 ga_second (R g) = R $ ga_assoc >>> ga_second g
100 ga_second (B _ g) = R $ ga_assoc >>> ga_second g
101 ga_cancell = N ga_cancell
102 ga_cancelr = N ga_cancelr
103 ga_uncancell = N ga_uncancell
104 ga_uncancelr = N ga_uncancelr
105 ga_assoc = N ga_assoc
106 ga_unassoc = N ga_unassoc
108 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowCopy (Polynomial g (**) u t) (**) u
112 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowDrop (Polynomial g (**) u t) (**) u
116 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowSwap (Polynomial g (**) u t) (**) u
121 -- | Given an **instance-polymorphic** Haskell function @(g () a)->(g b c)@ we can produce
122 -- a self-contained instance-polymorphic term @(g (a**b) c)@. The "trick" is that we supply
123 -- the instance-polymorphic Haskell function with a modified dictionary (type class instance)
125 homfunctor_inv :: forall a b c.
126 (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c) ->
127 (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c)
129 case f (B ga_cancelr ga_cancell) of
130 (N f') -> ga_first ga_drop >>> ga_cancell >>> f'
132 (R f') -> ga_swap >>> f'
138 -- A few more comments are in order. First of all, the function
139 -- @homfunctor@ above really is a hom-functor; its domain is the
140 -- category whose objects are Haskell types and whose morphisms a->b
141 -- are Haskell terms of type @(GArrow g => g a b)@ -- note how the
142 -- term is polymorphic in @g@.
144 -- This category is Hask-enriched: for each choice of @a@ and @b@, the
145 -- collection of all morphisms a->b happens to be a Hask-object, and
146 -- all the other necessary conditions are met.
148 -- I use the term "fully enriched" to mean "enriched such that the
149 -- hom-functor at the terminal object is a full functor". For any
150 -- morphism f whose domain and codomain are in the range of the
151 -- hom-functor, the function homfunctor_inv above will pick out a
152 -- morphism in its domain which is sent to f -- it is the witness
153 -- to the fact that the functor is full.