module Control.Computation ( -- * Arrows module Control.Arrow, -- * Computations Computation ( type Unit, type Pair, type Function, type DropResult, (###), assocLeft, assocRight, padFst, padSnd, dropFst, dropSnd, swap, curry, apply ), mapFst, mapSnd, precomp, postcomp, uncurry, inFst, inSnd, outFst, outSnd, -- * Nested pairs map1, map2, map3, map4, in1, in2, in3, in4, out1, out2, out3, out4, construct, destruct, (+:+), (-:-), -- * Pure computations Pure, -- * Links between computation types Link (type Source, type Target, linkMap, unitInside, pairInside), -- * Connected computation types Connected (type (==>), type (<==), inject, extract), up, down ) where -- Prelude import Prelude hiding (id, (.), curry, uncurry) import qualified Prelude -- Control import Control.Category import Control.Arrow -- GHC import GHC.Exts (Constraint) -- Fixities infixr 3 ### infixr 5 +:+ infixr 5 -:- -- * Computations class ArrowChoice p => Computation p where type Unit p :: * type Pair p :: * -> * -> * type Function p :: * -> * -> * type DropResult p a :: Constraint (###) :: (a `p` c) -> (b `p` d) -> (Pair p a b `p` Pair p c d) assocLeft :: Pair p a (Pair p b c) `p` Pair p (Pair p a b) c assocRight :: Pair p (Pair p a b) c `p` Pair p a (Pair p b c) padFst :: a `p` (Pair p (Unit p) a) padSnd :: a `p` (Pair p a (Unit p)) dropFst :: DropResult p a => Pair p (Unit p) a `p` a dropSnd :: DropResult p a => Pair p a (Unit p) `p` a swap :: Pair p a b `p` Pair p b a curry :: Pair p a b `p` c -> a `p` Function p b c apply :: Pair p (Function p a b) a `p` b {-FIXME: We do not have a curry operator for (->). This decision was first made for simplicity. However, it has a more important justification. We cannot implement a curry operator for (->) in the case of Resourceful. A morphism of type α ~> β is a natural transformation of type ∀ R . α R → β R, if we mean ∀ to stand for natural transformation. A value of type α -> β inside the Resourceful category is also of such a type. More precisely, a value of type α -> β for a resource type R is of type ∀ Q . α Q → β Q, and so its type is independent of R. Application (realized by arr apply) is still possible with this. However, currying is not, as it would have to have the following type: (∀ R . α R × β R → γ R) → (∀ R . α R → (∀ Q . β Q → γ Q)) This is not possible. If (->) inside Resourceful would properly correspond to an end, then we could turn a (α → β) R into an (α → β) Q for every r : Q → R by using A r, but with ∀ Q, we would have to transform also to such (α → β) Q where there is no r : Q → R. What structure do we still have for (->)? Is (->) even a contravariant and covariant functor? In any case, we have distributivity, since we can generate the canonical distributivity transformations from the corresponding transformations for (->) via arr. Are these so-gained transformations correct? -} {-FIXME: Consider adding rules for the Computation class, like it is done for the Arrow class. To make the rules actually fire, we have to make this module Trustworthy. -} mapFst :: Computation p => a `p` b -> Pair p a c `p` Pair p b c mapFst comp1 = comp1 ### id mapSnd :: Computation p => b `p` c -> Pair p a b `p` Pair p a c mapSnd comp2 = id ### comp2 precomp :: Computation p => a `p` b -> Function p b c `p` Function p a c precomp comp = curry (mapSnd comp >>> apply) postcomp :: Computation p => b `p` c -> Function p a b `p` Function p a c postcomp comp = curry (apply >>> comp) uncurry :: Computation p => a `p` Function p b c -> Pair p a b `p` c uncurry comp = mapFst comp >>> apply inFst :: Computation p => a `p` Function p b c -> Pair p a b `p` c inFst comp = uncurry comp inSnd :: Computation p => b `p` Function p a c -> Pair p a b `p` c inSnd comp = swap >>> uncurry comp outFst :: Computation p => Pair p a b `p` c -> a `p` Function p b c outFst comp = curry comp outSnd :: Computation p => Pair p a b `p` c -> b `p` Function p a c outSnd comp = curry (swap >>> comp) -- * Nested pairs map1 :: Computation p => a `p` b -> Pair p a t `p` Pair p b t map1 = mapFst map2 :: Computation p => b `p` c -> Pair p a (Pair p b t) `p` Pair p a (Pair p c t) map2 = mapSnd . mapFst map3 :: Computation p => c `p` d -> Pair p a (Pair p b (Pair p c t)) `p` Pair p a (Pair p b (Pair p d t)) map3 = mapSnd . mapSnd . mapFst map4 :: Computation p => d `p` e -> Pair p a (Pair p b (Pair p c (Pair p d t))) `p` Pair p a (Pair p b (Pair p c (Pair p e t))) map4 = mapSnd . mapSnd . mapSnd . mapFst in1 :: Computation p => a `p` Function p t r -> Pair p a t `p` r in1 = inFst in2 :: Computation p => b `p` Function p t (Function p a r) -> Pair p a (Pair p b t) `p` r in2 = inSnd . inFst in3 :: Computation p => c `p` Function p t (Function p b (Function p a r)) -> Pair p a (Pair p b (Pair p c t)) `p` r in3 = inSnd . inSnd . inFst in4 :: Computation p => d `p` Function p t (Function p c (Function p b (Function p a r))) -> Pair p a (Pair p b (Pair p c (Pair p d t))) `p` r in4 = inSnd . inSnd . inSnd . inFst out1 :: Computation p => Pair p a t `p` r -> a `p` Function p t r out1 = outFst out2 :: Computation p => Pair p a (Pair p b t) `p` r -> b `p` Function p t (Function p a r) out2 = outFst . outSnd out3 :: Computation p => Pair p a (Pair p b (Pair p c t)) `p` r -> c `p` Function p t (Function p b (Function p a r)) out3 = outFst . outSnd . outSnd out4 :: Computation p => Pair p a (Pair p b (Pair p c (Pair p d t))) `p` r -> d `p` Function p t (Function p c (Function p b (Function p a r))) out4 = outFst . outSnd . outSnd . outSnd construct :: Computation p => (Unit p `p` a) -> (b `p` Pair p a b) construct constructor = padFst >>> mapFst constructor destruct :: (Computation p, DropResult p b) => (a `p` Unit p) -> (Pair p a b `p` b) destruct destructor = mapFst destructor >>> dropFst (+:+) :: Computation p => (Unit p `p` a) -> (b `p` t) -> (b `p` Pair p a t) constructor +:+ comp = comp >>> construct constructor (-:-) :: (Computation p, DropResult p t) => (a `p` Unit p) -> (t `p` b) -> (Pair p a t `p` b) destructor -:- comp = destruct destructor >>> comp -- * Pure computations type Pure = (->) instance Computation Pure where type Unit Pure = () type Pair Pure = (,) type Function Pure = (->) type DropResult Pure a = () (###) = (***) assocLeft ~(val1, ~(val2, val3)) = ((val1, val2), val3) assocRight ~(~(val1, val2), val3) = (val1, (val2, val3)) padFst val = ((), val) padSnd val = (val, ()) dropFst ~(_, val) = val dropSnd ~(val, _) = val swap ~(val1, val2) = (val2, val1) curry = Prelude.curry apply = Prelude.uncurry ($) -- * Links between computation types class (Computation (Source l), Computation (Target l)) => Link l where type Source l :: * -> * -> * type Target l :: * -> * -> * linkMap :: Source l a b -> Target l (l a) (l b) unitInside :: Target l (Unit (Target l)) (l (Unit (Source l))) pairInside :: Target l (Pair (Target l) (l a) (l b)) (l (Pair (Source l) a b)) -- * Connected computation types {-NOTE: For the temporal case, we not only need a subclass of Computation, but also subclasses of Connected and Link. The one for Connected, would probably differ only from Connected by additional constraints of (==>) and (<==) being instances of the temporal Link class, and by informally stated additional laws that describe the interaction between processes and the adjunction. -} class (Link (p ==> q), Source (p ==> q) ~ p, Target (p ==> q) ~ q, Link (p <== q), Source (p <== q) ~ q, Target (p <== q) ~ p) => Connected p q where data p ==> q :: * -> * data p <== q :: * -> * inject :: a `p` (p <== q) ((p ==> q) a) extract :: (p ==> q) ((p <== q) b) `q` b up :: Connected p q => a `p` (p <== q) b -> (p ==> q) a `q` b up comp1 = linkMap comp1 >>> extract down :: Connected p q => (p ==> q) a `q` b -> a `p` (p <== q) b down comp2 = inject >>> linkMap comp2 instance Computation p => Connected p p where newtype (p ==> p) a = SelfUp { unSelfUp :: a } newtype (p <== p) a = SelfDown { unSelfDown :: a } inject = arr (SelfUp >>> SelfDown) extract = arr (unSelfUp >>> unSelfDown) instance Computation p => Link (p ==> p) where type Source (p ==> p) = p type Target (p ==> p) = p linkMap comp = arr unSelfUp >>> comp >>> arr SelfUp unitInside = arr SelfUp pairInside = arr unSelfUp ### arr unSelfUp >>> arr SelfUp instance Computation p => Link (p <== p) where type Source (p <== p) = p type Target (p <== p) = p linkMap comp = arr unSelfDown >>> comp >>> arr SelfDown unitInside = arr SelfDown pairInside = arr unSelfDown ### arr unSelfDown >>> arr SelfDown