X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=GHC%2FHetMet%2FGArrow.hs;h=9878a4d5842e4947449c873392f5cef26819058d;hb=fe3e9a061c212b2c9f83e31632236afcaacacb81;hp=93d2886784fabc794d760c2c84c5e4432181cacd;hpb=a223a71a0d40523d2fb3a6b84b5da37d9fc719b8;p=ghc-base.git diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs index 93d2886..9878a4d 100644 --- a/GHC/HetMet/GArrow.hs +++ b/GHC/HetMet/GArrow.hs @@ -1,4 +1,4 @@ -{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances #-} +{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFunctionalDependencies -XTypeFamilies -XFlexibleContexts #-} ----------------------------------------------------------------------------- -- | -- Module : GHC.HetMet.GArrow @@ -14,83 +14,234 @@ module GHC.HetMet.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(..), + + GArrowTensor, + GArrowUnit, + GArrowExponent, + + GArrowSTKC(..), + GArrowSTKCL(..), + GArrowSTLC(..), + GArrowPCF(..) + ) where -import Control.Arrow +import Control.Category hiding ((.)) +import Prelude hiding (id) + +------------------------------------------------------------------------ +-- The main GArrow class -class GArrow g (**) where - ga_id :: g x x - ga_comp :: g x y -> g y z -> g x z +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 - ga_swap :: g (x**y) (y**x) +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_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_loopr :: g (x**z) (y**z) -> g x y + ga_loopl :: g (z**x) (z**y) -> g x y --- implementation of ga_second for GArrowSwap instances -ga_swap_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 +------------------------------------------------------------------------ +-- 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 (**) => GArrowLiteral g (**) a where - ga_literal :: a -> g () a +class GArrow g (**) u => GArrowLiteral g (**) u t r where + ga_literal :: t -> g u r --- not sure -- subject to change -class GArrow g (**) => GArrowReify g (**) where - ga_reify :: (x -> y) -> g x y --- not sure -- subject to change -class GArrow g (**) => GArrowReflect g (**) where - ga_reflect :: g x y -> (x -> y) +------------------------------------------------------------------------ +-- Constant and Run, which are dual to each other ------------------------------------------------------------------------------- --- GArrow instances for Control.Arrow +class GArrow g (**) u => GArrowEval g (**) u r t where + ga_eval :: g u r -> t -instance Arrow a => GArrow a (,) where - ga_id = arr Prelude.id - ga_comp = (>>>) - ga_first = first - ga_second = second - ga_cancell = arr (\((),x) -> x) - ga_cancelr = arr (\(x,()) -> x) - ga_uncancell = arr (\x -> ((),x)) - ga_uncancelr = arr (\x -> (x,())) - ga_assoc = arr (\((x,y),z) -> (x,(y,z))) - ga_unassoc = arr (\(x,(y,z)) -> ((x,y),z)) - -instance Arrow a => GArrowDrop a (,) where - ga_drop = arr (\x -> ()) +class GArrow g (**) u => GArrowConstant g (**) u t r where + ga_constant :: t -> g u r -instance Arrow a => GArrowCopy a (,) where - ga_copy = arr (\x -> (x,x)) -instance Arrow a => GArrowSwap a (,) where - ga_swap = arr (\(x,y) -> (y,x)) -instance Arrow a => GArrowLiteral a (,) where - ga_literal x = arr (\() -> x) -instance Arrow a => GArrowReify a (,) where - ga_reify = arr -instance ArrowLoop a => GArrowLoop a (,) where - ga_loop = loop +------------------------------------------------------------------------ +-- 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) + + + + + +------------------------------------------------------------------------ +-- 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) + + + + + +------------------------------------------------------------------------ +-- 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