X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=GHC%2FHetMet%2FGArrow.hs;h=b9bfccf922bd745bb64c6d45d6126e056a05d26a;hb=3b6276233970210dce8d7c12d72ba5d55644e051;hp=d31436c58ca51a9e39d4c8cbc528c1045e8dbd9f;hpb=3ad8f1f62daf9614a2edbf97ac6e64191c31d2de;p=ghc-base.git

diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs
index d31436c..b9bfccf 100644
--- a/GHC/HetMet/GArrow.hs
+++ b/GHC/HetMet/GArrow.hs
@@ -1,48 +1,211 @@
-{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators #-}
+{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  GHC.HetMet.GArrow
+-- Copyright   :  none
+-- License     :  public domain
+--
+-- Maintainer  :  Adam Megacz <megacz@acm.org>
+-- Stability   :  experimental
+-- Portability :  portable
+
 module GHC.HetMet.GArrow (
   GArrow(..),
   GArrowDrop(..),
   GArrowCopy(..),
   GArrowSwap(..),
+
   GArrowLoop(..),
+
+  GArrowEval(..),
+  GArrowConstant(..),
+  GArrowLiteral(..),   -- should be implemented, but never invoked, by user code
+
+  GArrowSum(..),  ga_inl, ga_inr,
+  GArrowProd(..),
+
   GArrowReify(..),
-  GArrowReflect(..)
+  GArrowReflect(..),
+
+  GArrowCurry(..),
+  GArrowApply(..),
+
+  GArrowKappa(..),
+  GArrowSTKC(..),
+  GArrowSTLC(..),
+  GArrowPCF(..)
+
 ) where
+import Control.Category hiding ((.))
+import Prelude          hiding (id)
 
-class GArrow g (**) where
-  ga_id        :: g x x
-  ga_comp      :: g x y -> g y z -> g x z
+------------------------------------------------------------------------
+-- The main GArrow class
+
+class Category g => GArrow g (**) u | (**) -> u, u -> (**) where
+--id           :: g x x
+--comp         :: g x y -> g y z -> g x z
   ga_first     :: g x y -> g (x ** z) (y ** z)
   ga_second    :: g x y -> g (z ** x) (z ** y)
-  ga_cancell   :: g (()**x) x
-  ga_cancelr   :: g (x**()) x
-  ga_uncancell :: g x       (()**x)
-  ga_uncancelr :: g x       (x**())
-  ga_assoc     :: g ((x**y)**z) (x**(y**z))
-  ga_unassoc   :: g (x**(y**z)) ((x**y)**z)
+  ga_cancell   :: g (u**x)         x
+  ga_cancelr   :: g    (x**u)      x
+  ga_uncancell :: g     x      (u**x)
+  ga_uncancelr :: g     x         (x**u)
+  ga_assoc     :: g ((x** y)**z ) ( x**(y **z))
+  ga_unassoc   :: g ( x**(y **z)) ((x** y)**z )
+
 
-class GArrow g (**) => GArrowDrop g (**) where
-  ga_drop      :: g x ()
+------------------------------------------------------------------------
+-- The three context-manipulation classes
 
-class GArrow g (**) => GArrowCopy g (**) where
+class GArrow g (**) u => GArrowCopy g (**) u where
   ga_copy      :: g x (x**x)
 
-class GArrow g (**) => GArrowSwap g (**) where
+class GArrow g (**) u => GArrowDrop g (**) u where
+  ga_drop      :: g x u
+
+class GArrow g (**) u => GArrowSwap g (**) u where
   ga_swap      :: g (x**y) (y**x)
-  --ga_second  f =  ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
 
-class GArrow g (**) => GArrowLoop g (**) where
-  ga_loop      :: g (x**z) (y**z) -> g x y
+ga_swap_second f =
+   ga_swap >>> ga_first f >>> ga_swap
+   -- implementation of ga_second for GArrowSwap
+   -- See also
+   -- http://haskell.org/haskellwiki/Class_system_extension_proposal
+   -- "Allowing superclass methods to be overridden in derived classes";
+   -- if we had this we could do a better job here
+
+
+
+------------------------------------------------------------------------
+-- Products, Coproducts, etc
+
+
+class (GArrowDrop g (<*>) u,
+       GArrowCopy g (<*>) u) =>
+       GArrowProd g (<*>) u
+
+class GArrow     g (<+>) u =>
+      GArrowSum  g (<+>) u where
+  ga_merge :: g (x<+>x) x
+  ga_never :: g u       x
+
+ga_inl :: GArrowSum g (<+>) u => g x (x<+>y)
+ga_inl = ga_uncancelr >>> ga_second ga_never
+
+ga_inr :: GArrowSum g (<+>) u => g x (y<+>x)
+ga_inr = ga_uncancell >>> ga_first  ga_never
+
+
+------------------------------------------------------------------------
+-- Loop
+
+class GArrow g (**) u => GArrowLoop g (**) u where
+  ga_loopl    :: g (x**z) (y**z) -> g x y
+  ga_loopr    :: g (z**x) (z**y) -> g x y
+
+
+------------------------------------------------------------------------
+-- Literal.  Note that ga_literal should never appear in (unflattened)
+-- Haskell programs, though the user may wish to write implementations
+-- of this function (I haven't yet found a way to enforce this
+-- restriction using exports)
+
+class GArrow g (**) u => GArrowLiteral g (**) u t r where
+  ga_literal  :: t -> g u r
+
+
+
+
+------------------------------------------------------------------------
+-- Constant and Run, which are dual to each other
+
+class GArrow g (**) u => GArrowEval g (**) u r t where
+  ga_eval      :: g u r -> t
+
+class GArrow g (**) u => GArrowConstant g (**) u t r where
+  ga_constant  :: t -> g u r
+
+
+
+------------------------------------------------------------------------
+-- Reify and Reflect, which are "curried" versions of eval/const
+
+-- If you have this for R the identity map on types, you're basically
+-- a Control.Arrow; you can also define essentially all the other
+-- methods of GArrow, GArrowDrop, GArrowCopy, etc in terms of this.
+class GArrow g (**) u => GArrowReify g (**) u x y r q where
+  ga_reify     :: (x -> y) -> g r q
+
+class GArrow g (**) u => GArrowReflect g (**) u r q x y where
+  ga_reflect   :: g r q -> (x -> y)
+
+
+
+
+------------------------------------------------------------------------
+-- The Kappa adjunction
+--
+-- See Hasegawa, Decomposing Typed Lambda Calculus into a Couple of
+-- Categorical Programming Languages) section 3, rule $(\times L)$
+
+class GArrow g (**) u => GArrowKappa g (**) u where
+  ga_kappa :: (g u x -> g u y) -> g x y
+
+
+
+
+
+------------------------------------------------------------------------
+-- Apply and Curry
+
+class GArrow g (**) u => GArrowApply g (**) u (~>) where
+  ga_applyl    :: g (x**(x~>y)   ) y
+  ga_applyr    :: g (   (x~>y)**x) y
+
+class GArrow g (**) u => GArrowCurry g (**) u (~>) where
+  ga_curryl    :: g (x**y) z  ->  g x (y~>z)
+  ga_curryr    :: g (x**y) z  ->  g y (x~>z)
+
+
+
+
+------------------------------------------------------------------------
+-- Commonly Implemented Collections of Classes
+
+--
+-- The simply typed KAPPA calculus; see Hasegawa, __Decomposing Typed
+-- Lambda Calculus into a Couple of Categorical Programming
+-- Languages__, http://dx.doi.org/10.1007/3-540-60164-3_28
+-- 
+class (GArrowDrop  g (**) u,
+       GArrowCopy  g (**) u,
+       GArrowSwap  g (**) u) =>
+       GArrowSTKC  g (**) u
+
+-- The simply typed LAMBDA calculus
+class (GArrowSTKC  g (**) u,
+       GArrowCurry g (**) u (~>),
+       GArrowApply g (**) u (~>)) =>
+       GArrowSTLC  g (**) u (~>)
+
+-- Programming Language for Computable Functions (w/o integers and booleans)
+class (GArrowSTLC  g (**) u (~>),
+       GArrowLoop  g (**) u) =>
+       GArrowPCF   g (**) u (~>)
+
+
 
-class GArrow g (**) => GArrowLiteral g (**) a where
-  ga_literal   :: a -> g () a
 
--- not sure
-class GArrow g (**) => GArrowReify g (**) where
-  ga_reify     :: (x -> y) -> g x y
 
--- not sure
-class GArrow g (**) => GArrowReflect g (**) where
-  ga_reflect   :: g x y -> (x -> y)
+------------------------------------------------------------------------
+-- Experimental, Not Yet Exported
 
+-- See Lindley, Wadler, and Yallop '08 -- except that here ga_force
+-- is primitive since there is no "arr" to define it in terms of.
+class GArrow g (**) u => GArrowStatic g (**) u (~>) where
+  ga_delay :: g a b      -> g u (a~>b)
+  ga_force :: g u (a~>b) -> g a b
+  -- "ga_static/force_delay"   forall a . force (delay a) = a
+  -- "ga_static/delay_force"   forall a . delay (force a) = a