X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=GHC%2FHetMet%2FGArrow.hs;h=8b88b9b759a1647b9cd15bf47fe1cfedcbcac586;hb=9404945188d8f4e4daf851c0bc53a61c80b8fdfc;hp=88f84fbaa5fa1d0eb3df44010c7dd943aa1c9b90;hpb=1c5d86f9ab468292f9a52b079e25578ac83d07e2;p=ghc-base.git diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs index 88f84fb..8b88b9b 100644 --- a/GHC/HetMet/GArrow.hs +++ b/GHC/HetMet/GArrow.hs @@ -1,4 +1,4 @@ -{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances -XFunctionalDependencies #-} +{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies -XTypeFamilies -XFlexibleContexts #-} ----------------------------------------------------------------------------- -- | -- Module : GHC.HetMet.GArrow @@ -21,21 +21,33 @@ module GHC.HetMet.GArrow ( GArrowConstant(..), GArrowLiteral(..), -- should be implemented, but never invoked, by user code - GArrowSum(..), + GArrowSum(..), ga_inl, ga_inr, GArrowProd(..), GArrowReify(..), GArrowReflect(..), GArrowCurry(..), - GArrowApply(..) + GArrowApply(..), + + GArrowTensor, + GArrowUnit, + GArrowExponent, + + GArrowKappa(..), + GArrowSTKC(..), + GArrowSTKCL(..), + GArrowSTLC(..), + GArrowPCF(..) + ) where -import Control.Category +import Control.Category hiding ((.)) +import Prelude hiding (id) ------------------------------------------------------------------------ -- The main GArrow class -class Category g => GArrow g (**) u | (**) -> u where +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) @@ -70,32 +82,34 @@ ga_swap_second f = + + ------------------------------------------------------------------------ -- Products, Coproducts, etc -class (GArrow g (**) u, - GArrow g (<*>) u) => - GArrowProd g (**) u (<*>) where - ga_prod_copy :: g x (x<*>x) - ga_prod_drop :: g x u +class (GArrowDrop g (<*>) u, + GArrowCopy g (<*>) u) => + GArrowProd g (<*>) u -class (GArrow g (**) u, - GArrow g (<+>) v) => - GArrowSum g (**) u v (<+>) where - ga_merge :: g (x**x) x - ga_never :: g v x - +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 + ga_loopr :: g (x**z) (y**z) -> g x y + ga_loopl :: g (z**x) (z**y) -> g x y ------------------------------------------------------------------------ @@ -122,7 +136,7 @@ class GArrow g (**) u => GArrowConstant g (**) u t r where ------------------------------------------------------------------------ --- 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 @@ -137,6 +151,19 @@ 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 class GArrow g (**) u => GArrowApply g (**) u (~>) where @@ -146,3 +173,86 @@ class GArrow g (**) u => GArrowApply g (**) u (~>) where 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) + + + + + +------------------------------------------------------------------------ +-- 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 + +-- +-- 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 (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 (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 (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 (~>) + + + + + +------------------------------------------------------------------------ +-- 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 +