diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,4 @@
+#!/usr/bin/env runghc
+
+> import Distribution.Simple
+> main = defaultMain
diff --git a/computations.cabal b/computations.cabal
new file mode 100644
--- /dev/null
+++ b/computations.cabal
@@ -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
diff --git a/src/Control/Computation.hs b/src/Control/Computation.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Computation.hs
@@ -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
diff --git a/src/Control/Computation/Resourceful.hs b/src/Control/Computation/Resourceful.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Computation/Resourceful.hs
@@ -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