-{-# LANGUAGE RankNTypes, MultiParamTypeClasses, NoMonomorphismRestriction, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts, FlexibleInstances, DatatypeContexts #-}
+{-# LANGUAGE RankNTypes, MultiParamTypeClasses, TypeOperators, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module : GHC.HetMet.IGArrow
-- IGArrowProd(..),
) where
-import Control.Category hiding ((.))
+import Control.Category
import GHC.HetMet.GArrow
-import Prelude hiding (id)
-import GHC.HetMet.Arrow
+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
-- | An "internal generalized arrow" is a GArrow except that it uses
-- some *other* GArrow in place of Haskell's function space.
--
-class IGArrow g (**) u gg (***) uu where
+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_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 u)
+ 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))
-
-
-------------------------------------------------------------------------------
--- Self-Internal GArrows
-
---
--- | A self-internal GArrow is, well, internal to itself
+------------------------------------------------------------------------
+-- Externalization
--
-class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
-
+-- | 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.
--
--- | Self-internal GArrows have curry/apply
+-- TODO: I should be one level deeper here: assuming an (IGArrow
+-- (IGArrow g)), create an (IGArrow g).
--
--- instance SelfInternalGArrow g (**) u => GArrowApply g (**) u gg where
--- ga_applyl = :: g (x**(g x y) ) y
--- ga_applyr :: g ( (g x y)**x) y
---
+
+newtype Ex g x y = Ex (g x y)
+
--
--- | Self-internal GArrows have curry/apply
+-- | Every IGArrow of (->) is a GArrow
--
--- instance SelfInternalGArrow g (**) u gg (***) uu => GArrowCurry g (**) u gg where
--- ga_curryl :: g (x**y) z -> g x (g y z)
--- ga_curryr :: g (x**y) z -> g y (g x z)
+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 ()
-------------------------------------------------------------------------------
--- Instances
+
+------------------------------------------------------------------------
+-- Internalization
--
-- | Every GArrow is internal to the GArrow instance on (->)
--
-instance GArrow g (**) u => IGArrow (->) (,) () g (**) u 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
+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
------------------------------------------------------------------------
--- Externalization
+-- Kappa
--
--- | 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.
+-- | 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.
--
--- TODO: I should be one level deeper here: assuming an (IGArrow
--- (IGArrow g)), create an (IGArrow g).
+-- 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
+
+
-newtype
- IGArrow g (**) u q (***) uu =>
- Ext g (**) u q (***) uu x y
- = Ext { unExt :: g u (q x y) }
-
--- instance IGArrow g (**) u gg (***) uu => GArrowCopy g (**) u gg (***) uu where
--- iga_copy = undefined
---
--- instance IGArrow g (**) u gg (***) uu => GArrowDrop g (**) u gg (***) uu where
--- iga_drop = undefined
---
--- instance IGArrow g (**) u gg (***) uu => GArrowSwap g (**) u gg (***) uu where
--- iga_swap = undefined
---
--- instance IGArrow g (**) u gg (***) uu => GArrowLoop g (**) u gg (***) uu where
--- iga_loopr = undefined
--- iga_loopl = undefined
---
--- instance IGArrow g (**) u gg (***) uu => GArrowLiteral g (**) u gg (***) uu t r where
--- iga_literal = undefined
---
--- instance IGArrow g (**) u gg (***) uu => GArrowEval g (**) u gg (***) uu r t where
--- iga_eval = undefined
---
--- instance IGArrow g (**) u gg (***) uu => GArrowConstant g (**) u gg (***) uu t r where
--- iga_constant = undefined
---
--- instance IGArrow g (**) u gg (***) uu => GArrowReify g (**) u gg (***) uu x y r q where
--- iga_reify = undefined
---
--- instance IGArrow g (**) u gg (***) uu => GArrowReflect g (**) u gg (***) uu r q x y where
--- iga_reflect = undefined
+
+
+
+------------------------------------------------------------------------------
+-- 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