packages feed

computations (empty) → 0.0.0.0

raw patch · 5 files changed

+1005/−0 lines, 5 filesdep +basesetup-changed

Dependencies added: base

Files

+ LICENSE view
@@ -0,0 +1,27 @@+Copyright © 2012–2015 Wolfgang Jeltsch+All rights reserved.++Redistribution and use in source and binary forms, with or without modification,+are permitted provided that the following conditions are met:++    • Redistributions of source code must retain the above copyright notice,+      this list of conditions and the following disclaimer.++    • Redistributions in binary form must reproduce the above copyright notice,+      this list of conditions and the following disclaimer in the documentation+      and/or other materials provided with the distribution.++    • Neither the name of the copyright holders nor the names of the+      contributors may be used to endorse or promote products derived from this+      software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS “AS IS” AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR+TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF+THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.lhs view
@@ -0,0 +1,4 @@+#!/usr/bin/env runghc++> import Distribution.Simple+> main = defaultMain
+ computations.cabal view
@@ -0,0 +1,54 @@+Name:          computations+Version:       0.0.0.0+Cabal-Version: >= 1.16+Build-Type:    Simple+License:       BSD3+License-File:  LICENSE+Copyright:     © 2012–2015 Wolfgang Jeltsch+Author:        Wolfgang Jeltsch+Maintainer:    wolfgang@cs.ioc.ee+Stability:     provisional+Homepage:      http://darcs.wolfgang.jeltsch.info/haskell/computations+Package-URL:   http://hackage.haskell.org/packages/archive/computations/0.0.0.0/computations-0.0.0.0.tar.gz+Synopsis:      Advanced notions of computation+Description:   This package provides a framework for computations with certain+               consistency constraints. Based on this framework, it implements+               resourceful computations, which are an alternative to the @IO@+               mondad. In the case of resourceful computations, the consistency+               constraint is a single-use policy, also known as linearity.+Category:      Control+Tested-With:   GHC == 7.8.3++Source-Repository head+    Type:     darcs+    Location: http://darcs.wolfgang.jeltsch.info/haskell/computations/main++Source-Repository this+    Type:     darcs+    Location: http://darcs.wolfgang.jeltsch.info/haskell/computations/main+    Tag:      computations-0.0.0.0++Library++    Build-Depends: base >= 3.0 && < 5++    Default-Language: Haskell2010++    Default-Extensions: ConstraintKinds+                        ExistentialQuantification+                        FlexibleContexts+                        FlexibleInstances+                        GeneralizedNewtypeDeriving+                        MultiParamTypeClasses+                        Rank2Types+                        TypeFamilies+                        TypeOperators++    if impl(ghc >= 7.8) {+        Default-Extensions: AutoDeriveTypeable+    }++    Exposed-Modules: Control.Computation+                     Control.Computation.Resourceful++    HS-Source-Dirs: src
+ src/Control/Computation.hs view
@@ -0,0 +1,372 @@+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
+ src/Control/Computation/Resourceful.hs view
@@ -0,0 +1,548 @@+module Control.Computation.Resourceful (++    -- * Computations++    module Control.Computation,++    -- * Resourceful computations++    type (~>),+    type Resourceful,+    type Blank,+    type (**),+    type (-:),++    -- * Resources++    Resource (anchor),+    type Anchor (Anchor),++    -- * Attributes++    type Attr,+    unsafeToAttr,+    type Property (Property),+    (^>),+    (>^),+    (^^>),+    (>^^),+    unsafeToProperty,+    ResourceFunction (get),++    -- * Resource values++    type ResourceValue (annotate),+    type Annotator,++    -- * Atomic resources++    type AtomicResource,+    unsafeToResourceConv,+    fromResourceConv,+    toUnitResource,+    fromUnitResource,+    toPairResource,+    fromPairResource++) where++{-FIXME:+    Make this module work well with Safe Haskell, which possibly includes moving+    the two unsafe functions into a separate module.+-}++-- Prelude++import Prelude hiding (id, (.), curry, uncurry)++-- Control++import Control.Category+import Control.Arrow+import Control.Computation+import Control.Applicative++-- Data++import Data.Monoid+import Data.Traversable++-- System++import System.IO.Unsafe++-- Fixities++infixr 0 ~>+infixr 7 **+infixr 1 -:+infixr 1 ^>+infixr 1 >^+infixr 1 ^^>+infixr 1 >^^++-- * Resourceful computations++newtype a ~> b = Resourceful (a -> b) deriving (Category, Arrow, ArrowChoice)++type Resourceful = (~>)++data Blank = Blank { fromBlank :: Shredder }+{-NOTE:+    We have to use data instead of newtype, since otherwise the user could+    trigger the I/O via seq.+-}++newtype a ** b = ResourcefulPair { stdPair :: (a, b) }++newtype a -: b = ResourcefulFunction { stdFunction :: a -> b }++instance Computation Resourceful where++    type Unit Resourceful = Blank++    type Pair Resourceful = (**)++    type Function Resourceful = (-:)++    type DropResult Resourceful a = ResourceValue a++    Resourceful fun1 ### Resourceful fun2 = Resourceful $ stdPair         >>>+                                                          fun1 ### fun2   >>>+                                                          ResourcefulPair++    assocLeft = Resourceful $ stdPair                >>>+                              mapSnd stdPair         >>>+                              assocLeft              >>>+                              mapFst ResourcefulPair >>>+                              ResourcefulPair++    assocRight = Resourceful $ stdPair                >>>+                               mapFst stdPair         >>>+                               assocRight             >>>+                               mapSnd ResourcefulPair >>>+                               ResourcefulPair++    padFst = Resourceful $ const (Blank mempty) &&& id >>>+                           ResourcefulPair++    padSnd = Resourceful $ id &&& const (Blank mempty) >>>+                           ResourcefulPair++    dropFst = Resourceful $ stdPair                >>>+                            mapFst fromBlank       >>>+                            uncurry insertShredder++    dropSnd = Resourceful $ stdPair                       >>>+                            mapSnd fromBlank              >>>+                            uncurry (flip insertShredder)++    swap = Resourceful $ stdPair         >>>+                         swap            >>>+                         ResourcefulPair++    curry (Resourceful fun) = Resourceful $ curry (ResourcefulPair >>> fun) >>>+                                            ResourcefulFunction++    apply = Resourceful $ stdPair            >>>+                          mapFst stdFunction >>>+                          apply++-- * Connection to pure computations++instance Connected Pure Resourceful where++    data (Pure ==> Resourceful) a = Up {+                                        shredder :: Shredder,+                                        value    :: a+                                    }++    newtype (Pure <== Resourceful) b = Down { fromDown :: Shredder -> b }++    inject val = Down $ \ shredder -> Up shredder val++    extract = Resourceful fun where++        fun (Up shredder (Down toVal)) = toVal shredder++instance Link (Pure ==> Resourceful) where++    type Source (Pure ==> Resourceful) = Pure++    type Target (Pure ==> Resourceful) = Resourceful++    linkMap comp = Resourceful fun where++        fun (Up shredder val) = Up shredder (comp val)++    unitInside = Resourceful fun where++        fun (Blank shredder) = Up shredder ()++    pairInside = Resourceful $ stdPair >>> fun where++        fun (Up shredder1 val1, Up shredder2 val2) = Up (shredder1 <> shredder2)+                                                        (val1, val2)++instance Link (Pure <== Resourceful) where++    type Source (Pure <== Resourceful) = Resourceful++    type Target (Pure <== Resourceful) = Pure++    linkMap (Resourceful fun) = comp where++        comp (Down toVal) = Down (toVal >>> fun)++    unitInside _ = Down Blank++    pairInside (Down toVal1, Down toVal2) = Down toVal' where++        toVal' shredder = ResourcefulPair (toVal1 shredder, toVal2 shredder)++-- * Resources++class ResourceFunction a => Resource a where++    anchor :: Anchor a++data Anchor a = forall h . Anchor (a ~> AtomicResource h)+                                  (AtomicResource h ~> a)++instance Resource (AtomicResource h) where++    anchor = Anchor id id++instance Resource Blank where++    anchor = Anchor toUnitResource fromUnitResource++instance (Resource a, Resource b) => Resource (a ** b) where++    anchor = case (anchor, anchor) of+        (Anchor toAtomic1 fromAtomic1, Anchor toAtomic2 fromAtomic2)+            -> Anchor (toAtomic1 ### toAtomic2 >>> toPairResource)+                      (fromPairResource >>> fromAtomic1 ### fromAtomic2)++-- * Attributes++type Attr a v = Property a a v++unsafeToAttr :: (h -> IO v) -> Attr (AtomicResource h) v+unsafeToAttr attrIOFun = unsafeToProperty $ \ hdl -> do+    val <- attrIOFun hdl+    return (val, hdl)++newtype Property a b v = Property (forall h . (v -> (b ~> AtomicResource h)) ->+                                              (a ~> AtomicResource h))++instance Functor (Property a b) where++    fmap fun (Property contPassing) = prop where++        prop = Property (\ cont -> contPassing (cont . fun))++(^>) :: (a -> b) -> Property b c v -> Property a c v+fun ^> prop = arr fun ^^> prop++(>^) :: Property a b v -> (b -> c) -> Property a c v+prop >^ fun = prop >^^ arr fun++(^^>) :: (a ~> b) -> Property b c v -> Property a c v+comp ^^> Property contPassing = prop where++    prop = Property (\ cont -> comp >>> contPassing cont)++(>^^) :: Property a b v -> (b ~> c) -> Property a c v+Property contPassing >^^ comp = prop where++    prop = Property (\ cont -> contPassing ((comp >>>) . cont))++unsafeToProperty :: (h -> IO (v, k))+                 -> Property (AtomicResource h) (AtomicResource k) v+unsafeToProperty propIOFun = prop where++    prop = Property (\ valDependent -> unsafeToResourceConv (\ hdl -> do+        (val, hdl') <- propIOFun hdl+        fromResourceConv (valDependent val) hdl'))++class ResourceFunction r where++    get :: Property a b v -> (v -> (b ~> r)) -> (a ~> r)++instance ResourceFunction (AtomicResource h) where++    get = resourceGet++instance ResourceFunction Blank where++    get = resourceGet++instance (Resource a, Resource b) => ResourceFunction (a ** b) where++    get = resourceGet++instance ResourceFunction b => ResourceFunction (a -: b) where++    get prop valDependent = Resourceful (ResourcefulFunction . ctxFun) where++        ctxFun res ctx = fun res where++            Resourceful fun = get prop $+                              \ val -> valDependent val              >>>+                                       arr (stdFunction >>> ($ ctx))++resourceGet :: Resource r => Property a b v -> (v -> (b ~> r)) -> (a ~> r)+resourceGet (Property contPassing) valDependent = case anchor of+    Anchor toAtomic fromAtomic -> result where++        result = contPassing (valDependent >>> (>>> toAtomic)) >>> fromAtomic++-- * Resource values++class ResourceValue a where++    annotate :: a -> Annotator a+    annotate = pure++newtype Annotator a = Annotator { fromAnnotator :: Shredder -> a }+                      deriving (Functor, Applicative)++{-NOTE:+    Here we define instances for all Prelude types that are unrelated to I/O.+-}++instance ResourceValue (AtomicResource h) where++    annotate = withShredder >>> Annotator where++        withShredder (AtomicResource gen) shredder = AtomicResource gen' where++            gen' = fromShredder shredder *> gen++instance ResourceValue Blank where++    annotate = withShredder >>> Annotator where++        withShredder (Blank shredder) shredder' = Blank (shredder' <> shredder)++instance ResourceValue a => ResourceValue (a ** b) where++    annotate = withShredder >>> Annotator where++        withShredder pair shredder = ResourcefulPair $+                                     (insertShredder shredder val1, val2) where++            (val1, val2) = stdPair pair++instance ResourceValue b => ResourceValue (a -: b) where++    annotate = withShredder >>> Annotator where++        withShredder fun shredder = ResourcefulFunction $+                                    stdFunction fun         >>>+                                    insertShredder shredder++instance ResourceValue ((Pure ==> Resourceful) a) where++    annotate = withShredder >>> Annotator where++        withShredder (Up shredder val) shredder' = Up (shredder' <> shredder)+                                                      val++instance ResourceValue Bool++instance ResourceValue a => ResourceValue (Maybe a) where++    annotate = traverse annotate++instance (ResourceValue a, ResourceValue b) => ResourceValue (Either a b) where++    annotate (Left  val1) = Left  <$> annotate val1+    annotate (Right val2) = Right <$> annotate val2++instance ResourceValue Ordering++instance ResourceValue Char++instance ResourceValue Int++instance ResourceValue Integer++instance ResourceValue Float++instance ResourceValue Double++instance ResourceValue Rational++instance ResourceValue a => ResourceValue [a] where++    annotate = traverse annotate++instance ResourceValue ()++instance (ResourceValue a, ResourceValue b) => ResourceValue (a, b) where++    annotate (val1, val2) = (,) <$> annotate val1 <*> annotate val2++instance (ResourceValue a, ResourceValue b, ResourceValue c) =>+         ResourceValue (a, b, c) where++    annotate (val1, val2, val3) = (,,) <$> annotate val1+                                       <*> annotate val2+                                       <*> annotate val3++instance (ResourceValue a, ResourceValue b, ResourceValue c, ResourceValue d) =>+         ResourceValue (a, b, c, d) where++    annotate (val1, val2, val3, val4) = (,,,) <$> annotate val1+                                              <*> annotate val2+                                              <*> annotate val3+                                              <*> annotate val4++instance (ResourceValue a,+          ResourceValue b,+          ResourceValue c,+          ResourceValue d,+          ResourceValue e) =>+         ResourceValue (a, b, c, d, e) where++    annotate (val1, val2, val3, val4, val5) = (,,,,) <$> annotate val1+                                                     <*> annotate val2+                                                     <*> annotate val3+                                                     <*> annotate val4+                                                     <*> annotate val5++instance (ResourceValue a,+          ResourceValue b,+          ResourceValue c,+          ResourceValue d,+          ResourceValue e,+          ResourceValue f) =>+         ResourceValue (a, b, c, d, e, f) where++    annotate (val1, val2, val3, val4, val5, val6) = (,,,,,) <$> annotate val1+                                                            <*> annotate val2+                                                            <*> annotate val3+                                                            <*> annotate val4+                                                            <*> annotate val5+                                                            <*> annotate val6++instance (ResourceValue a, ResourceValue b) => ResourceValue (a -> b)+{-NOTE:+    This instance declaration is correct, because we have this non-standard+    definition of (->) in the Resourceful category, where α -> β for a resource+    type R corresponds to ∀ Q . α Q → β Q. This is independent of R, and for+    every r : Q → R, the morphism (α -> β) r is just the identity.+-}++insertShredder :: ResourceValue a => Shredder -> a -> a+insertShredder = flip (fromAnnotator . annotate)++-- * Atomic resources++data AtomicResource h = AtomicResource (Gen h)+{-NOTE:+    Note that we have to use data instead of newtype, since otherwise the user+    could trigger the I/O via seq.+-}++{-# NOINLINE unsafeToResourceConv #-}+unsafeToResourceConv :: (h -> IO k) -> (AtomicResource h ~> AtomicResource k)+unsafeToResourceConv ioFun = Resourceful fun where++    fun (AtomicResource gen) = AtomicResource $+                               unsafePerformIO $+                               case gen of Gen hdl -> Gen <$> ioFun hdl++{-NOTE:++    Regarding unsafePerformIO:++      • We hope that putting the application of unsafePerformIO into a where+        clause does not cause harm due to inlining or such.++      • We have not disabled common subexpression elimination for this module,+        as we do not see how CSE could cause harm in connection with our use of+        unsafePerformIO. However if we were to add another function that uses+        unsafePerformIO, we should check whether this is still safe.++    Regarding Gen being no monad:++      • It looks like Gen could be a monad. Then we could just implement a+        conversion from IO to Gen and implement unsafeToResourceConv in terms of+        (>>=) of the Gen monad. However, the second argument of (>>=) would be a+        generator that does not refer to the initial resource set, but to the+        one that is left by the first argument. This is in contradiction with+        the idea that generators generate resources from the initial resource+        set. (However, we do not have the approach anymore that Gen refers to+        some “initial” resource set, but that every Gen value refers to some+        specific resource set.)+-}++fromResourceConv :: (AtomicResource h ~> AtomicResource k) -> (h -> IO k)+fromResourceConv (Resourceful fun) hdl = io where++    io = do+             AtomicResource (Gen hdl') <- return $+                                          fun (AtomicResource (pure hdl))+             return hdl'++toUnitResource :: Blank ~> AtomicResource ()+toUnitResource = Resourceful fun where++    fun (Blank shredder) = AtomicResource (fromShredder shredder)++fromUnitResource :: AtomicResource () ~> Blank+fromUnitResource = Resourceful fun where++    fun (AtomicResource gen) = Blank (toShredder gen)++toPairResource :: AtomicResource h ** AtomicResource k ~> AtomicResource (h, k)+toPairResource = Resourceful $ stdPair >>> fun where++    fun (AtomicResource gen1, AtomicResource gen2) = AtomicResource $+                                                     (,) <$> gen1 <*> gen2++fromPairResource :: AtomicResource (h, k) ~> AtomicResource h ** AtomicResource k+fromPairResource = Resourceful $ fun >>> ResourcefulPair where++    fun (AtomicResource gen) = (AtomicResource gen1, AtomicResource gen2) where++        gen1 = fst <$> gen++        gen2 = snd <$> gen++-- * Generators++data Gen h = Gen h+{-NOTE:+    A value of type Gen h denotes a morphism in the resource category from some+    Q to h. The Q is not visible in the type, but every value of type Gen h has+    an associated Q. The implementation of this module has to make sure that Gen+    is only used in type-safe ways regarding the Qs.+-}++instance Functor Gen where++    fmap fun (Gen hdl) = Gen (fun hdl)++instance Applicative Gen where++    pure = Gen++    Gen fun <*> Gen arg = Gen (fun arg)++data Shredder = Shredder++toShredder :: Gen () -> Shredder+toShredder (Gen _) = Shredder++fromShredder :: Shredder -> Gen ()+fromShredder Shredder = Gen ()++instance Monoid Shredder where++    mempty = Shredder++    Shredder `mappend` Shredder = Shredder