-{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts #-}
-----------------------------------------------------------------------------
-- |
-- Module : GHC.HetMet.GArrow
GArrowCurry(..),
GArrowApply(..),
+ GArrowTensor,
+ GArrowUnit,
+ GArrowExponent,
+
GArrowSTKC(..),
+ GArrowSTKCL(..),
GArrowSTLC(..),
GArrowPCF(..)
) where
-import Control.Category
+import Control.Category hiding ((.))
+import Prelude hiding (id)
------------------------------------------------------------------------
-- The main GArrow class
+
+
------------------------------------------------------------------------
-- Products, Coproducts, etc
-- 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
+ ga_loopr :: g (x**z) (y**z) -> g x y
+ ga_loopl :: g (z**x) (z**y) -> g x y
------------------------------------------------------------------------
+
+
------------------------------------------------------------------------
--- Reify and Reflect, which are "curried" versions
+-- 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
+
------------------------------------------------------------------------
-- Apply and Curry
+
+------------------------------------------------------------------------
+-- Type Families
+
+--
+-- The GArrow and GArrow{Copy,Drop,Swap} classes brandish their tensor
+-- and unit types; this is important because we might want to have
+-- both "instance GArrow g X Y" and "instance GArrow g Z Q" -- in
+-- fact, this is exactly how sums and pairs are defined.
+--
+-- However, in daily practice it's a pain to have all those extra type
+-- variables floating around. If you'd like to hide them, you can use
+-- the type families below to do so; see the definition of class
+-- GArrowSTKC for an example. Keep in mind, however, that any given
+-- type may only have a single instance declared using the type
+-- families.
+--
+
+type family GArrowTensor g :: * -> * -> * -- (**)
+type family GArrowUnit g :: * -- ()
+type family GArrowExponent g :: * -> * -> * -- (~>)
+
+
+
+
------------------------------------------------------------------------
-- Commonly Implemented Collections of Classes
-- 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
+
+class (GArrowDrop g (GArrowTensor g) (GArrowUnit g),
+ GArrowCopy g (GArrowTensor g) (GArrowUnit g),
+ GArrowSwap g (GArrowTensor g) (GArrowUnit g)) =>
+ GArrowSTKC g
+
+class (GArrowDrop g (GArrowTensor g) (GArrowUnit g),
+ GArrowCopy g (GArrowTensor g) (GArrowUnit g),
+ GArrowSwap g (GArrowTensor g) (GArrowUnit g),
+ GArrowLoop g (GArrowTensor g) (GArrowUnit g)) =>
+ GArrowSTKCL g
-- The simply typed LAMBDA calculus
-class (GArrowSTKC g (**) u,
- GArrowCurry g (**) u (~>),
- GArrowApply g (**) u (~>)) =>
- GArrowSTLC g (**) u (~>)
+class (GArrowDrop g (GArrowTensor g) (GArrowUnit g),
+ GArrowCopy g (GArrowTensor g) (GArrowUnit g),
+ GArrowSwap g (GArrowTensor g) (GArrowUnit g),
+ GArrowCurry g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
+ GArrowApply g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g)
+ ) =>
+ GArrowSTLC g
-- Programming Language for Computable Functions (w/o integers and booleans)
-class (GArrowSTLC g (**) u (~>),
- GArrowLoop g (**) u) =>
- GArrowPCF g (**) u (~>)
+class (GArrowDrop g (GArrowTensor g) (GArrowUnit g),
+ GArrowCopy g (GArrowTensor g) (GArrowUnit g),
+ GArrowSwap g (GArrowTensor g) (GArrowUnit g),
+ GArrowCurry g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
+ GArrowApply g (GArrowTensor g) (GArrowUnit g) (GArrowExponent g),
+ GArrowLoop g (GArrowTensor g) (GArrowUnit g)
+ ) =>
+ GArrowPCF g (**) u (~>)