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 GHC.HetMet.GArrow
61 import Prelude hiding ((.), id)
63 data GArrow g (**) u => Polynomial g (**) u t x y
64 = L (g (t**x) y) -- uses t, wants it as the left arg
65 | R (g (x**t) y) -- uses t, wants it as the right arg
66 | B (g (t**x) y) (g (x**t) y) -- uses t, doesn't care which arg
67 | N (g x y) -- doesn't use t
69 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => Category (Polynomial g (**) u t) where
71 (N g) . (N f) = N $ g . f
72 (N g) . (L f) = L $ g . f
73 (N g) . (R f) = R $ g . f
74 (N g) . (B f f') = B (f >>> g) (f' >>> g)
75 (L g) . (N f) = L $ g . ga_second f
76 (R g) . (N f) = R $ g . ga_first f
77 (B g g') . (N f) = B (ga_second f >>> g) (ga_first f >>> g')
78 (L g) . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g
79 (L g) . (B f f') = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g
80 (R g) . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> g
81 (B g g') . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> g'
82 (B g g') . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g
83 (R g) . (B f f') = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f' >>> g
84 (R g) . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> ga_swap >>> g
85 (L g) . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> ga_swap >>> g
86 (B g g') . (B f f') = B (ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g)
87 (ga_second ga_copy >>> ga_unassoc >>> ga_first f' >>> g')
89 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrow (Polynomial g (**) u t) (**) u where
90 ga_first (N f) = N $ ga_first f
91 ga_first (L f) = L $ ga_unassoc >>> ga_first f
92 ga_first (R f) = B (ga_unassoc >>> ga_first (ga_swap >>> f))
93 (ga_assoc >>> ga_second ga_swap >>> ga_unassoc >>> ga_first f)
94 ga_first (B f _) = L $ ga_unassoc >>> ga_first f
95 ga_second (N g) = N $ ga_second g
96 ga_second (L f) = B (ga_unassoc >>> ga_first ga_swap >>> ga_assoc >>> ga_second f)
97 (ga_assoc >>> ga_second (ga_swap >>> f))
98 ga_second (R g) = R $ ga_assoc >>> ga_second g
99 ga_second (B _ g) = R $ ga_assoc >>> ga_second g
100 ga_cancell = N ga_cancell
101 ga_cancelr = N ga_cancelr
102 ga_uncancell = N ga_uncancell
103 ga_uncancelr = N ga_uncancelr
104 ga_assoc = N ga_assoc
105 ga_unassoc = N ga_unassoc
107 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowCopy (Polynomial g (**) u t) (**) u
111 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowDrop (Polynomial g (**) u t) (**) u
115 instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowSwap (Polynomial g (**) u t) (**) u
120 -- | Given an **instance-polymorphic** Haskell function @(g () a)->(g b c)@ we can produce
121 -- a self-contained instance-polymorphic term @(g (a**b) c)@. The "trick" is that we supply
122 -- the instance-polymorphic Haskell function with a modified dictionary (type class instance)
124 homfunctor_inv :: forall a b c.
125 (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c) ->
126 (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c)
128 case f (B ga_cancelr ga_cancell) of
129 (N f') -> ga_first ga_drop >>> ga_cancell >>> f'
131 (R f') -> ga_swap >>> f'
137 -- A few more comments are in order. First of all, the function
138 -- @homfunctor@ above really is a hom-functor; its domain is the
139 -- category whose objects are Haskell types and whose morphisms a->b
140 -- are Haskell terms of type @(GArrow g => g a b)@ -- note how the
141 -- term is polymorphic in @g@.
143 -- This category is Hask-enriched: for each choice of @a@ and @b@, the
144 -- collection of all morphisms a->b happens to be a Hask-object, and
145 -- all the other necessary conditions are met.
147 -- I use the term "fully enriched" to mean "enriched such that the
148 -- hom-functor at the terminal object is a full functor". For any
149 -- morphism f whose domain and codomain are in the range of the
150 -- hom-functor, the function homfunctor_inv above will pick out a
151 -- morphism in its domain which is sent to f -- it is the witness
152 -- to the fact that the functor is full.