From 3feb1f34df467291e1e0a118db86e680b37fef96 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Tue, 21 Jun 2011 22:19:52 -0700 Subject: [PATCH] IGArrow: major cleanup, finished instance IKappa (->) --- GHC/HetMet/IGArrow.hs | 312 +++++++++++++++++++------------------------------ 1 file changed, 122 insertions(+), 190 deletions(-) diff --git a/GHC/HetMet/IGArrow.hs b/GHC/HetMet/IGArrow.hs index ea5964c..4846022 100644 --- a/GHC/HetMet/IGArrow.hs +++ b/GHC/HetMet/IGArrow.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RankNTypes, MultiParamTypeClasses, NoMonomorphismRestriction, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts, FlexibleInstances, DatatypeContexts, UndecidableInstances, ScopedTypeVariables #-} +{-# LANGUAGE RankNTypes, MultiParamTypeClasses, TypeOperators, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-} ----------------------------------------------------------------------------- -- | -- Module : GHC.HetMet.IGArrow @@ -29,10 +29,16 @@ module GHC.HetMet.IGArrow ( ) where import Control.Category import GHC.HetMet.GArrow -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 @@ -43,7 +49,7 @@ import Prelude hiding (id, (.)) -- | 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 | 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)) @@ -59,7 +65,7 @@ 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 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)) @@ -85,222 +91,148 @@ class IGArrow g (**) u gg (***) uu => IGArrowReflect g (**) u gg (***) uu r q x -{- --- | This is named "kappa" for its similarity to an operator in --- Hasegawa's kappa-calculus, but there isn't actually a formal --- connection. -class GArrow g (**) u => IKappa g (**) u where - iga_kappa :: forall a b c uu . - (forall gg (***) . (IGArrow g (**) u gg (***) uu, - IGArrowCopy g (**) u gg (***) uu, - IGArrowSwap g (**) u gg (***) uu, - IGArrowDrop g (**) u gg (***) uu) => g (gg uu a) (gg b c)) -> - (forall gg (***) . (IGArrow g (**) u gg (***) uu, - IGArrowCopy g (**) u gg (***) uu, - IGArrowSwap g (**) u gg (***) uu, - IGArrowDrop g (**) u gg (***) uu) => g u (gg (a***b) c)) - -- TO DO: probably need l/r versions of the above +------------------------------------------------------------------------ +-- 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) ---class IGArrow g (**) u gg (***) uu => IGArrowKappa g (**) u gg (***) uu where --- iga_kappa :: g (x**(gg uu a)) (gg b c) -> g x (gg (a***b) c) - -- TO DO: probably need l/r versions of the above +-- +-- | 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 () ------------------------------------------------------------------------------- --- Self-Internal GArrows --- --- | A self-internal GArrow is, well, internal to itself --- ---class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u +------------------------------------------------------------------------ +-- Internalization -- --- | Self-internal GArrows have curry/apply --- --- 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 --- --- --- | Self-internal GArrows have curry/apply +-- | Every GArrow is internal to the GArrow instance on (->) -- --- 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) +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 ------------------------------------------------------------------------------- --- Instances --- --- | 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 -instance GArrowCopy g (**) u => IGArrowCopy (->) (,) () g (**) u where -instance GArrowSwap g (**) u => IGArrowSwap (->) (,) () g (**) u where -instance GArrowDrop g (**) u => IGArrowDrop (->) (,) () g (**) u where --} - -data - In g x y - = In (g x y) -instance GArrow g (**) u => IGArrow (->) (,) () (In g) (**) u where -instance GArrowCopy g (**) u => IGArrowCopy (->) (,) () (In g) (**) u where -instance GArrowSwap g (**) u => IGArrowSwap (->) (,) () (In g) (**) u where -instance GArrowDrop g (**) u => IGArrowDrop (->) (,) () (In g) (**) u where ------------------------------------------------------------------------ --- 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 -data - Ext g x y - = Ext (g x y) + + + +------------------------------------------------------------------------------ +-- Self-Internal GArrows + -- --- | Every IGArrow of (->) is a GArrow +-- | A self-internal GArrow is, well, internal to itself -- -instance IGArrow (->) (,) () g (**) u => Category (Ext g) where - id = Ext (iga_id ()) - (Ext g) . (Ext f) = Ext (iga_comp (f,g)) - -instance IGArrow (->) (,) () g (**) u => GArrow (Ext g) (**) u where --- ga_first (Ext f) = Ext $ iga_first f --- ga_second (Ext f) = Ext $ iga_second f - ga_cancell = Ext $ iga_cancell () - ga_cancelr = Ext $ iga_cancelr () - ga_uncancell = Ext $ iga_uncancell () - ga_uncancelr = Ext $ iga_uncancelr () - ga_assoc = Ext $ iga_assoc () - ga_unassoc = Ext $ iga_unassoc () - -instance IGArrowSwap (->) (,) () g (**) u => GArrowSwap (Ext g) (**) u where -instance IGArrowCopy (->) (,) () g (**) u => GArrowCopy (Ext g) (**) u where -instance IGArrowDrop (->) (,) () g (**) u => GArrowDrop (Ext g) (**) u where - - --- iga_kappa :: forall a b c uu . (forall gg (***) . IGArrow g (**) u gg (***) uu => g (gg uu a) (gg b c)) -> --- (forall gg (***) . IGArrow g (**) u gg (***) uu => g u (gg (a***b) c)) -{- - Could not deduce (GArrowDrop gg (***) uu, - GArrowSwap gg (***) uu, - GArrowCopy gg (***) uu) - arising from a use of `homfunctor_inv' - from the context (IGArrow (->) (,) () gg (***) uu) --} - ---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) +class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u -- --- | Every GArrow is also an IKappa of (->) by virtue of GArrowFullyEnriched +-- | Self-internal GArrows have curry/apply -- -instance IKappa (->) (,) () where --- iga_kappa :: forall a b c u . --- (forall g (**) . (IGArrow (->) (,) () g (**) u, --- IGArrowCopy (->) (,) () g (**) u, --- IGArrowSwap (->) (,) () g (**) u, --- IGArrowDrop (->) (,) () g (**) u) => (g u a) -> (g b c)) -> --- (forall g (**) . (IGArrow (->) (,) () g (**) u, --- IGArrowCopy (->) (,) () g (**) u, --- IGArrowSwap (->) (,) () g (**) u, --- IGArrowDrop (->) (,) () g (**) u) => () -> (g (a**b) c)) - iga_kappa (f :: forall g (**) . - (IGArrow (->) (,) () g (**) u, - IGArrowCopy (->) (,) () g (**) u, - IGArrowDrop (->) (,) () g (**) u, - IGArrowSwap (->) (,) () g (**) u) => - (g u a)->(g b c)) () - = mork $ homfunctor_inv (\y -> case f (In y) of (In q) -> q) - -mork :: forall u a b c . - (forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c) - -> (forall g (**) . (IGArrow (->) (,) () g (**) u, - IGArrowCopy (->) (,) () g (**) u, - IGArrowSwap (->) (,) () g (**) u, - IGArrowDrop (->) (,) () g (**) u) => (g (a**b) c)) -mork = undefined -{- - z :: forall g (**) . IGArrow (->) (,) () g (**) u => g (a**b) c - z = let - qf :: forall g (**) . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c - qf y = f y - in case homfunctor_inv qf of Ext q -> q --} - -{- -instance IGArrow (->) (,) () g (**) u => GArrowSTKC (Ext g) --} - --- 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 - +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" --- | Haskell's function space is self-internal --- instance SelfInternalGArrow (->) (,) () +-- +-- | 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" -- --- x , 1->a |- b ->c --- -------------------------- [Kappa] --- x |- (a,b)->c +-- | Haskell's function space is self-internal -- --- forall a b c x. --- (forall g (**) u gg (***) uu . --- IGArrow g (**) u gg (***) uu => --- g (x**(gg uu a)) (gg b c)) --- -> --- (forall g (**) u gg (***) uu . --- IGArrow g (**) u gg (***) uu => --- g x (gg (a***b) c)) --} \ No newline at end of file +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 (->) (,) () -- 1.7.10.4