{-# OPTIONS -fwarn-incomplete-patterns #-}
-{-# LANGUAGE RankNTypes, FlexibleInstances, TypeFamilies, MultiParamTypeClasses, GADTs, DatatypeContexts, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE RankNTypes, FlexibleInstances, TypeFamilies, MultiParamTypeClasses, GADTs, DatatypeContexts, TypeOperators #-}
-----------------------------------------------------------------------------
--
-- | The instance witnessing the fact that (forall g . GArrow g => g a b) is fully enriched in Hask.
import GHC.HetMet.GArrow
import Prelude hiding ((.), id)
-data GArrow g (**) u => Polynomial g (**) u t x y
+data (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop 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
+instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop 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
(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
+instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop 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))
-- 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 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 :: forall a b c.
+ (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c) ->
+ (forall g (**) u . (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'