+++ /dev/null
-{-# LANGUAGE RankNTypes, MultiParamTypeClasses, TypeOperators, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
------------------------------------------------------------------------------
--- |
--- Module : GHC.HetMet.IGArrow
--- Copyright : none
--- License : public domain
---
--- Maintainer : Adam Megacz <megacz@acm.org>
--- Stability : experimental
--- Portability : portable
-
-module GHC.HetMet.IGArrow (
- IGArrow(..),
- IGArrowDrop(..),
- IGArrowCopy(..),
- IGArrowSwap(..),
- IGArrowLoop(..),
-
- IGArrowEval(..),
- IGArrowConstant(..),
- IGArrowLiteral(..),
-
- IGArrowReify(..),
- IGArrowReflect(..),
-
- -- IGArrowSum(..), ga_inl, ga_inr,
- -- IGArrowProd(..),
-
-) where
-import Control.Category
-import GHC.HetMet.GArrow
-import GHC.HetMet.GArrowFullyEnriched
-import Prelude hiding (id, (.))
-
---
--- Importing GHC.HetMet.Arrow leads to overlapping instances; that's
--- why you see (GArrow (->) (,) () => ...) below in many places
--- instead of simply providing the instance defined in
--- GHC.HetMet.Arrow.
---
---import GHC.HetMet.Arrow
-
-
-
-
-------------------------------------------------------------------------
--- Internal GArrows
---
--- | An "internal generalized arrow" is a GArrow except that it uses
--- some *other* GArrow in place of Haskell's function space.
---
-class GArrow g (**) u => IGArrow g (**) u gg (***) uu | g -> (**), (**) -> u, gg -> (***), (***) -> uu where
- iga_id :: g u (gg x x)
- iga_comp :: g ((gg x y) ** (gg y z)) (gg x z)
- iga_first :: g (gg x y) (gg (x *** z) (y *** z))
- iga_second :: g (gg x y) (gg (z *** x) (z *** y))
- iga_cancell :: g u (gg (uu***x) x)
- iga_cancelr :: g u (gg (x***uu) x)
- iga_uncancell :: g u (gg x (uu***x))
- iga_uncancelr :: g u (gg x (x***uu))
- iga_assoc :: g u (gg ((x*** y)***z ) ( x***(y ***z)))
- iga_unassoc :: g u (gg ( x***(y ***z)) ((x*** y)***z ))
-
-class IGArrow g (**) u gg (***) uu => IGArrowCopy g (**) u gg (***) uu where
- iga_copy :: g u (gg x (x***x))
-
-class IGArrow g (**) u gg (***) uu => IGArrowDrop g (**) u gg (***) uu where
- iga_drop :: g u (gg x uu)
-
-class IGArrow g (**) u gg (***) uu => IGArrowSwap g (**) u gg (***) uu where
- iga_swap :: g u (gg (x***y) (y***x))
-
-class IGArrow g (**) u gg (***) uu => IGArrowLoop g (**) u gg (***) uu where
- iga_loopr :: g (gg (x***z) (y***z)) (gg x y)
- iga_loopl :: g (gg (z***x) (z***y)) (gg x y)
-
-class IGArrow g (**) u gg (***) uu => IGArrowLiteral g (**) u gg (***) uu t r where
- iga_literal :: g t (gg uu r)
-
-class IGArrow g (**) u gg (***) uu => IGArrowEval g (**) u gg (***) uu r t where
- iga_eval :: g (gg uu r) t
-
-class IGArrow g (**) u gg (***) uu => IGArrowConstant g (**) u gg (***) uu t r where
- iga_constant :: g t (gg uu r)
-
-class IGArrow g (**) u gg (***) uu => IGArrowReify g (**) u gg (***) uu x y r q where
- iga_reify :: g (g x y) (gg r q)
-
-class IGArrow g (**) u gg (***) uu => IGArrowReflect g (**) u gg (***) uu r q x y where
- iga_reflect :: g (gg r q) (g x y)
-
-
-
-------------------------------------------------------------------------
--- Externalization
---
--- | An IGArrow may be "externalized" to form a normal generalized
--- arrow. If the IGArrow was an instance of class IGArrowXX, the
--- externalization will be an instance of GArrowYY.
---
--- TODO: I should be one level deeper here: assuming an (IGArrow
--- (IGArrow g)), create an (IGArrow g).
---
-
-newtype Ex g x y = Ex (g x y)
-
---
--- | Every IGArrow of (->) is a GArrow
---
-instance IGArrow (->) (,) () g (**) u => Category (Ex g) where
- id = Ex (iga_id ())
- (Ex g) . (Ex f) = Ex (iga_comp (f,g))
-
-instance IGArrow (->) (,) () g (**) u => GArrow (Ex g) (**) u where
- ga_first (Ex f) = Ex $ iga_first f
- ga_second (Ex f) = Ex $ iga_second f
- ga_cancell = Ex $ iga_cancell ()
- ga_cancelr = Ex $ iga_cancelr ()
- ga_uncancell = Ex $ iga_uncancell ()
- ga_uncancelr = Ex $ iga_uncancelr ()
- ga_assoc = Ex $ iga_assoc ()
- ga_unassoc = Ex $ iga_unassoc ()
-
-instance IGArrowCopy (->) (,) () g (**) u => GArrowCopy (Ex g) (**) u where
- ga_copy = Ex $ iga_copy ()
-instance IGArrowDrop (->) (,) () g (**) u => GArrowDrop (Ex g) (**) u where
- ga_drop = Ex $ iga_drop ()
-instance IGArrowSwap (->) (,) () g (**) u => GArrowSwap (Ex g) (**) u where
- ga_swap = Ex $ iga_swap ()
-
-
-
-
-
-------------------------------------------------------------------------
--- Internalization
---
--- | Every GArrow is internal to the GArrow instance on (->)
---
-
-newtype In g x y = In (g x y)
-
-instance (GArrow (->) (,) (), GArrow g (**) u) => IGArrow (->) (,) () (In g) (**) u where
- iga_id _ = In $ id
- iga_comp (In f,In g) = In $ f >>> g
- iga_first (In f) = In $ ga_first f
- iga_second (In f) = In $ ga_second f
- iga_cancell _ = In $ ga_cancell
- iga_cancelr _ = In $ ga_cancelr
- iga_uncancell _ = In $ ga_uncancell
- iga_uncancelr _ = In $ ga_uncancelr
- iga_assoc _ = In $ ga_assoc
- iga_unassoc _ = In $ ga_unassoc
-instance (GArrow (->) (,) (), GArrowCopy g (**) u) => IGArrowCopy (->) (,) () (In g) (**) u where
- iga_copy _ = In $ ga_copy
-instance (GArrow (->) (,) (), GArrowDrop g (**) u) => IGArrowDrop (->) (,) () (In g) (**) u where
- iga_drop _ = In $ ga_drop
-instance (GArrow (->) (,) (), GArrowSwap g (**) u) => IGArrowSwap (->) (,) () (In g) (**) u where
- iga_swap _ = In $ ga_swap
-
-
-
-
-
-------------------------------------------------------------------------
--- Kappa
---
--- | This is named "kappa" for its similarity to an operator in
--- Hasegawa's kappa-calculus, but the formal connection is a bit of
--- a stretch; the method iga_kappa below is used by the flattener to
--- implement the typing rule for abstraction in Kappa-calculus.
---
--- x , 1->a |- b ->c
--- -------------------------- [Kappa]
--- x |- (a,b)->c
---
---
-class GArrow g (**) u => IKappa g (**) u where
- iga_kappa :: forall a b c .
- (forall gg (***) uu . (IGArrowCopy g (**) u gg (***) uu,
- IGArrowDrop g (**) u gg (***) uu,
- IGArrowSwap g (**) u gg (***) uu) =>
- g (gg uu a) (gg b c)) ->
- (forall gg (***) uu . (IGArrowCopy g (**) u gg (***) uu,
- IGArrowDrop g (**) u gg (***) uu,
- IGArrowSwap g (**) u gg (***) uu) =>
- g u (gg (a***b) c))
- -- TO DO: change the above to iga_kappal, add iga_kappar
-
---
--- | The (->) GArrow has the Kappa property.
---
-instance GArrow (->) (,) () => IKappa (->) (,) () where
- iga_kappa f = case (homfunctor_inv (\x -> case f (In x) of In x' -> x')) of Ex x -> \() -> x
-
-
-
-
-
-
-------------------------------------------------------------------------------
--- Self-Internal GArrows
-
---
--- | A self-internal GArrow is, well, internal to itself
---
-class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
-
---
--- | Self-internal GArrows have curry/apply
---
-instance SelfInternalGArrow g (**) u => GArrowApply g (**) u g where
- ga_applyl = error "FIXME: SelfInternalGArrow => GArrowApply not implemented yet"
- ga_applyr = error "FIXME: SelfInternalGArrow => GArrowApply not implemented yet"
-
---
--- | Self-internal GArrows have curry/apply
---
-instance SelfInternalGArrow g (**) u => GArrowCurry g (**) u g where
- ga_curryl = error "FIXME: SelfInternalGArrow => GArrowCurry not implemented yet"
- ga_curryr = error "FIXME: SelfInternalGArrow => GArrowCurry not implemented yet"
-
---
--- | Haskell's function space is self-internal
---
-instance GArrow (->) (,) () => IGArrow (->) (,) () (->) (,) () where
- iga_id _ = id
- iga_comp (f,g) = f >>> g
- iga_first = ga_first
- iga_second = ga_second
- iga_cancell _ = ga_cancell
- iga_cancelr _ = ga_cancelr
- iga_uncancell _ = ga_uncancell
- iga_uncancelr _ = ga_uncancelr
- iga_assoc _ = ga_assoc
- iga_unassoc _ = ga_unassoc
-
---instance GArrow (->) (,) () => SelfInternalGArrow (->) (,) ()
projects / ghc-base.git / blobdiff