+++ /dev/null
-{-# OPTIONS -fwarn-incomplete-patterns #-}
-{-# 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.
---
--- Module : GHC.HetMet.GArrowFullyEnriched
--- Copyright : none
--- License : public domain
---
--- 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:
---
--- > homfunctor :: (GArrow g (,) () => g a b -> (g () a -> g () b))
---
--- ... it's nothing more than the precomposition function:
---
--- > homfunctor = (.)
---
--- however, writing its *inverse* is not so easy:
---
--- > homfunctor_inv :: (GArrow g (,) () => (g () a -> g () b) -> g a b)
---
--- Think about it. This is saying that every way of turning a @(g ()
--- a)@ into a @(g () b)@ is equivalent to precomposition, for some
--- magically-divined value of type @(g a b)@. That's hard to believe!
--- In fact, it's flat out false unless we exploit parametricity. This
--- 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
-
--- * Category Theoretic Background
--- $extradoc1
-
-) where
-import Control.Category
-import GHC.HetMet.GArrow
---import GHC.HetMet.GArrowEnclosure
-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 (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
- (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 (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))
- (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_copy = N ga_copy
-
-instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowDrop (Polynomial g (**) u t) (**) u
- where
- ga_drop = N ga_drop
-
-instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowSwap (Polynomial g (**) u t) (**) u
- where
- ga_swap = N ga_swap
-
---instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u, GArrowLoop g (**) u)
--- => GArrowLoop (Polynomial g (**) u t) (**) u
--- where
--- ga_loopl = error "FIXME: GArrowFullyEnriched loopl not implemented"
--- ga_loopr = error "FIXME: GArrowFullyEnriched loopl not implemented"
-
---instance GArrowEnclosure q g (**) u => GArrowEnclosure (Polynomial q (**) u t) g (**) u where
--- enclose f = N (enclose f)
-
---
--- | 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 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'
- (L f') -> f'
- (R f') -> ga_swap >>> f'
- (B f' _) -> f'
-
---
--- $extradoc1
---
--- A few more comments are in order. First of all, the function
--- @homfunctor@ above really is a hom-functor; its domain is the
--- category whose objects are Haskell types and whose morphisms a->b
--- are Haskell terms of type @(GArrow g => g a b)@ -- note how the
--- term is polymorphic in @g@.
---
--- This category is Hask-enriched: for each choice of @a@ and @b@, the
--- collection of all morphisms a->b happens to be a Hask-object, and
--- all the other necessary conditions are met.
---
--- I use the term "fully enriched" to mean "enriched such that the
--- hom-functor at the terminal object is a full functor". For any
--- morphism f whose domain and codomain are in the range of the
--- hom-functor, the function homfunctor_inv above will pick out a
--- morphism in its domain which is sent to f -- it is the witness
--- to the fact that the functor is full.
---
projects / ghc-base.git / blobdiff