X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=GHC%2FHetMet%2FGArrow.hs;h=e2dbf95d418d4a35d5df5936d990d6d93c397162;hb=11345faf37729b649dad0c052ee698d7080e40ee;hp=b9bfccf922bd745bb64c6d45d6126e056a05d26a;hpb=3b6276233970210dce8d7c12d72ba5d55644e051;p=ghc-base.git diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs index b9bfccf..e2dbf95 100644 --- a/GHC/HetMet/GArrow.hs +++ b/GHC/HetMet/GArrow.hs @@ -1,4 +1,4 @@ -{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts #-} ----------------------------------------------------------------------------- -- | -- Module : GHC.HetMet.GArrow @@ -30,8 +30,12 @@ module GHC.HetMet.GArrow ( GArrowCurry(..), GArrowApply(..), - GArrowKappa(..), + GArrowTensor, + GArrowUnit, + GArrowExponent, + GArrowSTKC(..), + GArrowSTKCL(..), GArrowSTLC(..), GArrowPCF(..) @@ -77,6 +81,8 @@ ga_swap_second f = + + ------------------------------------------------------------------------ -- Products, Coproducts, etc @@ -101,8 +107,8 @@ 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 + ga_loopr :: g (x**z) (y**z) -> g x y + ga_loopl :: g (z**x) (z**y) -> g x y ------------------------------------------------------------------------ @@ -128,6 +134,8 @@ class GArrow g (**) u => GArrowConstant g (**) u t r where + + ------------------------------------------------------------------------ -- Reify and Reflect, which are "curried" versions of eval/const @@ -143,18 +151,6 @@ class GArrow g (**) u => GArrowReflect g (**) u r q x y where ------------------------------------------------------------------------- --- 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 @@ -170,6 +166,31 @@ class GArrow g (**) u => GArrowCurry g (**) u (~>) where + +------------------------------------------------------------------------ +-- 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 @@ -178,21 +199,36 @@ class GArrow g (**) u => GArrowCurry g (**) u (~>) where -- 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 (~>)