X-Git-Url: http://git.megacz.com/?p=ghc-base.git;a=blobdiff_plain;f=GHC%2FHetMet%2FGArrowFullyEnriched.hs;fp=GHC%2FHetMet%2FGArrowFullyEnriched.hs;h=0000000000000000000000000000000000000000;hp=b24c6b6febf14974313968288e0fcdcb99b87d93;hb=e3eef06878b2b39a95ed3ad8378e8130ebef5570;hpb=b56d67eed0e1257af1df83d3314ac82c4921c2d3

diff --git a/GHC/HetMet/GArrowFullyEnriched.hs b/GHC/HetMet/GArrowFullyEnriched.hs
deleted file mode 100644
index b24c6b6..0000000
--- a/GHC/HetMet/GArrowFullyEnriched.hs
+++ /dev/null
@@ -1,163 +0,0 @@
-{-# 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.
---