Handle IO exceptions correctly and fix finalizers

I'm not super convinced the implementation is correct, but it passes the
current tests. I'll need to dig into it more though.

Author: jhgarner

README.md

@@ -1,9 +1,9 @@
 # Theseus
 
-Welcome to the hub for Theseus, an effect system library for Haskell. Theseus is
-an effect system that supports algebraic effects (including Coroutine), many
-higher order effects, and is designed so that semantics do not change when
-effects are reordered.
+Welcome to the hub for Theseus, an experimental effect system library for
+Haskell. Theseus is an effect system that supports algebraic effects (including
+Coroutine), many higher order effects, and is designed so that semantics do not
+change when effects are reordered.
 
 We'll explore how, much like the Ship of Theseus, programs can be deconstructed
 and rebuilt without changing what they are.

src/Theseus/Constraints.hs

@@ -24,6 +24,12 @@ class Anything (f :: Type -> Type)
 
 instance Anything f
 
+-- | A class that no types implement. It acts as a useful upper bound because
+-- it implies all other classes.
+class Nonthing (f :: Type -> Type) where
+  produceIt :: a -> f b
+  consumeIt :: f a -> b
+
 -- | Proof that two types are the equivalent. If you construct an instance of
 -- this type, please make sure the isomorphism holds. For example, `Iso (const
 -- Nothing) (const Nothing)` would be a bad `Iso`. It's better to use the
@@ -100,6 +106,9 @@ class stronger `IsAtLeast` weaker where
 instance lhs `IsAtLeast` Anything where
   implyAtLeast = implying
 
+instance Nonthing `IsAtLeast` Traversable where
+  implyAtLeast = Implies \f -> f @[] $ Iso consumeIt produceIt
+
 -- Assuming no one's doing anything bad with `Implies`, this instance should be
 -- equivalent to any others that apply, so we can make it incoherent.
 instance {-# INCOHERENT #-} same `IsAtLeast` same where

src/Theseus/Eff.hs

@@ -4,16 +4,22 @@ module Theseus.Eff (
   -- how Theseus works.
 
   -- * General Effect Machinery
-  Eff (Eff),
+  Eff (Eff, unEff),
+  getFacts,
+  effUn,
+  matchOn,
+  Facts (Facts, bounded),
   ControlFlow (..),
   Anything,
+  Nonthing,
   Implies (..),
   Iso (..),
   IsoSome (..),
   isoSomeId,
   isoImplying,
   IsAtLeast (..),
   implying,
+  transImply,
   Effect,
   Freer (Pure, Impure),
   unrestrict,
@@ -23,7 +29,11 @@ module Theseus.Eff (
   Subset (raising),
   send,
   runEff,
-  (:>),
+  Final (Final),
+  runEffM,
+  (:>) (getProof),
+  IsMember,
+  withProof,
   (:>>),
 
   -- * Handling Effects
@@ -43,6 +53,7 @@ module Theseus.Eff (
   interpretRaw,
   IHandlerRaw,
   interposeRaw,
+  IdentityCf (IdentityCf, runIdentityCf),
 
   -- * Reexports
   Identity,

src/Theseus/EffType.hs

@@ -12,6 +12,8 @@ module Theseus.Effect.Choice (
 import Control.Applicative
 import Control.Monad
 import Control.Monad.Identity
+import Data.Foldable
+import Theseus.Constraints
 import Theseus.Eff
 
 -- # Choice
@@ -38,20 +40,53 @@ data Many eff m a where
     -- need to track that ef remains compatible with our thread specific
     -- `Choice` interpreters. To do that we need to make sure lists are still
     -- valid wrappers and that all the other wrappers will be `Traversable`.
-    [] `IsoSome` ef ->
-    ef `Implies` Traversable ->
+    {unMany :: [] `IsoSome` ub -> ManyItems lb ub es a} ->
+    Many Choice (Eff lb ub es) a
+
+manyUn :: IsoSome [] ub -> Many Choice (Eff lb ub es) a -> ManyItems lb ub es a
+manyUn = flip unMany
+
+data ManyItems lb ub es a where
+  ManyItems ::
+    lb `Implies` Traversable ->
     -- These are the current values across all our threads of computation.
-    Eff ef es [a] ->
+    Eff lb ub es [a] ->
     -- This is the operation we'd like to run on each thread.
-    (a -> Eff ef es b) ->
-    Many Choice (Eff ef es) b
+    (a -> Eff lb ub es b) ->
+    ManyItems lb ub es b
+deriving instance Functor (ManyItems lb ub es)
 
 deriving instance Functor (Many eff m)
 
 instance ControlFlow Many Traversable where
-  Many listIso travProof start go `cfApply` fa = Many listIso travProof start ((<*> fa) . go)
-  Many listIso travProof start go `cfBind` afb = Many listIso travProof start (go >=> afb)
-  cfMap efToOut implication handler (Many listIso _ start go) = Many (isoImplying listIso efToOut) implication (handler start) (handler . go)
+  Many act `cfApply` fa = Many \listIso -> case act listIso of
+    ManyItems travProof start go -> ManyItems travProof start ((<*> fa) . go)
+  Many act `cfBind` afb = Many \listIso -> case act listIso of
+    ManyItems travProof start go -> ManyItems travProof start (go >=> afb)
+  cfMap ub isTrav handler (Many act) = Many \listIso -> case act (isoImplying listIso ub) of
+    ManyItems _ start go -> ManyItems isTrav (handler start) (handler . go)
+  cfOnce @_ @_ @eff implySend member' handler (Many act) = Many \listIso -> case act listIso of
+    many@(ManyItems travProof _ _) -> ManyItems travProof newStart pure
+     where
+      implied = transImply implySend travProof
+      newStart = do
+        matchOn (sequenceA <$> runMany listIso member' many) >>= \case
+          Pure as ->
+            case handler travProof member' $ Many $ const $ ManyItems (transImply implySend travProof) as pure of
+              Many act -> runMany listIso member' $ act listIso
+          Impure eff lb ub lifter next -> Eff \_ -> Impure eff lb ub lifter \imply member x ->
+            cfPutMeIn member (\starts -> runMany listIso member' $ manyUn listIso $ handler @_ @eff travProof member' $ Many \_ -> ManyItems implied starts pure) $ next imply member x
+  cfPutMeIn member f (Many act) = Many \listIso -> case act listIso of
+    many@(ManyItems travProof _ _) -> ManyItems travProof newStart pure
+     where
+      newStart = do
+        matchOn (sequenceA <$> runMany listIso member many) >>= \case
+          -- TODO this is probably bad because I'm flattening the threads.
+          -- I should create some tests to either show why this is fine or show
+          -- why it's bad.
+          Pure as -> fmap pure $ f $ fmap fold as
+          Impure eff lb ub lifter next -> Eff \_ -> Impure eff lb ub lifter \imply member x ->
+            fmap pure $ cfPutMeIn member f $ fmap fold <$> next imply member x
 
   -- Most `Choice` implementations are depth first. They run one thread to
   -- completion, then they run the next. The problem with depth first is that
@@ -62,11 +97,12 @@ instance ControlFlow Many Traversable where
   -- parallel. That means handlers aren't constantly going in and out of scope
   -- because all the threads will join before the interpreter goes out of
   -- scope.
-  cfRun imply@(Implies go) handler many@(Many listIso _ _ _) = Many listIso imply newStart pure
-   where
-    -- We require `Traversable` because we need to know how many threads made
-    -- it past the other interpreter.
-    newStart = go \(Iso lr rl) -> fmap (fmap rl . sequenceA . lr) $ handler $ runMany many
+  cfRun member handler (Many act) = Many \listIso -> case act listIso of
+    many@(ManyItems imply@(Implies go) _ _) -> ManyItems imply newStart pure
+     where
+      -- We require `Traversable` because we need to know how many threads made
+      -- it past the other interpreter.
+      newStart = go \(Iso lr rl) -> fmap (fmap rl . sequenceA . lr) $ handler $ runMany listIso member many
 
 -- There we go! That's how Theseus handles nondeterminism while avoiding the
 -- handler ordering problems.
@@ -76,57 +112,64 @@ instance ControlFlow Many Traversable where
 data Choice :: Effect where
   -- Do these constraints leak unfortunate implementation details? Yes. I don't
   -- know how to get rid of them though.
-  Empty :: (ef [], ef `IsAtLeast` Traversable) => Choice (Eff ef es) a
-  Choose :: (ef [], ef `IsAtLeast` Traversable) => Choice (Eff ef es) Bool
+  Empty :: Choice (Eff lb ub es) a
+  Choose :: Choice (Eff lb ub es) Bool
 
 -- | Runs a choice that causes all other effects to act globally over all the
 -- threads.
 runChoice ::
-  (ef `IsAtLeast` Traversable, ef []) =>
-  Eff ef (Choice : es) a ->
-  Eff ef es [a]
-runChoice = interpretRaw (pure . pure) \cases
-  Empty _ next ->
-    case next $ Many isoSomeId implyAtLeast (pure []) pure of
-      Many listIso travProof start go ->
+  (lb `IsAtLeast` Traversable, ub []) =>
+  Eff lb ub (Choice : es) a ->
+  Eff lb ub es [a]
+runChoice act = Eff \facts@Facts{bounded} -> effUn facts $ with act $ interpretRaw (isoImplying isoSomeId bounded) (pure . pure) \cases
+  Empty lb _ _ next ->
+    case manyUn isoSomeId $ next implyAtLeast (Just getProof) $ Many \_ -> ManyItems (transImply lb implyAtLeast) (pure []) pure of
+      ManyItems travProof start go ->
         join <$> runChoice do
           inits <- start
-          results <- traverse (poseChoice listIso travProof . go) inits
+          results <- traverse (poseChoice isoSomeId travProof . go) inits
           pure $ join results
-  Choose _ next ->
-    case next $ Many isoSomeId implyAtLeast (pure [True, False]) pure of
-      Many listIso travProof start go ->
+  Choose lb _ _ next ->
+    case manyUn isoSomeId $ next implyAtLeast (Just getProof) $ Many \_ -> ManyItems (transImply lb implyAtLeast) (pure [True, False]) pure of
+      ManyItems travProof start go ->
         join <$> runChoice do
           inits <- start
-          results <- traverse (poseChoice listIso travProof . go) inits
+          results <- traverse (poseChoice isoSomeId travProof . go) inits
           pure $ join results
 
 -- | Same as `runChoice`, but modifies a `Choice` that's not at the top of the
 -- stack.
 poseChoice ::
   Choice :> es =>
-  [] `IsoSome` ef ->
-  ef `Implies` Traversable ->
-  Eff ef es a ->
-  Eff ef es [a]
-poseChoice (IsoSome (Iso lg gl)) imply =
-  fmap gl . interposeRaw imply (lg . pure) \cases
-    Empty _ next ->
-      case next $ Many isoSomeId implyAtLeast (pure []) pure of
-        many -> lg <$> runMany many
-    Choose _ next ->
-      case next $ Many isoSomeId implyAtLeast (pure [True, False]) pure of
-        many -> lg <$> runMany many
+  [] `IsoSome` ub ->
+  lb `Implies` Traversable ->
+  Eff lb ub es a ->
+  Eff lb ub es [a]
+poseChoice isoUb imply action = do
+  Facts{bounded} <- getFacts
+  IsoSome (Iso lg gl) <- pure $ isoImplying isoUb bounded
+  fmap gl $ with action $ interposeRaw imply (lg . pure) \cases
+    Empty lb _ _ next ->
+      case manyUn isoUb $ next $ Many \_ -> ManyItems (transImply lb imply) (pure []) pure of
+        many -> lg <$> runMany isoUb (Just getProof) many
+    Choose lb _ _ next ->
+      case manyUn isoUb $ next $ Many \_ -> ManyItems (transImply lb imply) (pure [True, False]) pure of
+        many -> lg <$> runMany isoUb (Just getProof) many
 
 -- | Executes all the threads
-runMany :: Choice :> es => Many Choice (Eff ef es) a -> Eff ef es [a]
-runMany (Many isoSomeId travProof start go) =
-  join <$> poseChoice isoSomeId travProof do
+runMany :: [] `IsoSome` ub -> Maybe (Choice `IsMember` es) -> ManyItems lb ub es a -> Eff lb ub es [a]
+runMany listIso (Just proof) (ManyItems travProof start go) = withProof proof do
+  join <$> poseChoice listIso travProof do
     inits <- start
-    results <- traverse (poseChoice isoSomeId travProof . go) inits
+    results <- traverse (poseChoice listIso travProof . go) inits
     pure $ join results
+-- In this case we know that none of the computations will use `Choice`, so we
+-- don't need to distribute.
+runMany _ Nothing (ManyItems _ start go) = do
+  inits <- start
+  traverse go inits
 
-instance (Choice :> es, ef [], ef `IsAtLeast` Traversable) => Alternative (Eff ef es) where
+instance (Choice :> es, lb [], lb `IsAtLeast` Traversable) => Alternative (Eff lb ub es) where
   empty = send Empty
   a <|> b =
     send Choose >>= \case
@@ -135,12 +178,12 @@ instance (Choice :> es, ef [], ef `IsAtLeast` Traversable) => Alternative (Eff e
 
 -- | A provider for Choices. You can use this to scope the `Choice` threads.
 data Collect :: Effect where
-  Collect :: (ef `IsAtLeast` Traversable, ef []) => Eff ef (Choice : es) a -> Collect (Eff ef es) [a]
+  Collect :: (lb `IsAtLeast` Traversable, ub []) => Eff lb ub (Choice : es) a -> Collect (Eff lb ub es) [a]
 
 -- | Gathers all the threads of computation into a list.
-collect :: (Collect :> es, ef []) => ef `IsAtLeast` Traversable => Eff ef (Choice : es) a -> Eff ef es [a]
+collect :: (Collect :> es, ub [], lb `IsAtLeast` Traversable) => Eff lb ub (Choice : es) a -> Eff lb ub es [a]
 collect action = send $ Collect action
 
 -- | Provides the default `Choice` implementation.
-runCollect :: ef Identity => Eff ef (Collect : es) a -> Eff ef es a
+runCollect :: lb Identity => Eff lb ub (Collect : es) a -> Eff lb ub es a
 runCollect = interpret \_ (Collect action) -> pure $ runChoice action

src/Theseus/Effect/Choice.hs

@@ -15,19 +15,19 @@ data Coroutine a b m c where
   Yield :: a -> Coroutine a b m b
 
 -- | Pauses the computation providing `a` value and waiting on `b`.
-yield :: forall a b ef es. Coroutine a b :> es => a -> Eff ef es b
+yield :: forall a b lb ub es. Coroutine a b :> es => a -> Eff lb ub es b
 yield a = send $ Yield a
 
 -- | Runs a computation until it either completes or pauses. If it pauses, it
 -- can be resumed.
-runCoroutine :: forall a b c ef es. ef (Status ef es a b) => Eff ef (Coroutine a b : es) c -> Eff ef es (Status ef es a b c)
-runCoroutine = interpretRaw (pure . Done) \(Yield a) _ next ->
-  case next $ Yielding pure of
+runCoroutine :: forall a b c lb ub es. lb (Status lb ub es a b) => Eff lb ub (Coroutine a b : es) c -> Eff lb ub es (Status lb ub es a b c)
+runCoroutine = interpretRaw isoSomeId (pure . Done) \(Yield a) _ _ _ next ->
+  case next implying (Just $ getProof @(Coroutine a b)) $ Yielding pure of
     Yielding yielding -> pure $ Yielded a yielding
 
 -- | It is essential that the function provided by `Yielded` be used exactly
 -- once. Otherwise you'll get confusing semantics within your code.
-data Status ef es a b c = Done c | Yielded a (b -> Eff ef (Coroutine a b : es) c)
+data Status lb ub es a b c = Done c | Yielded a (b -> Eff lb ub (Coroutine a b : es) c)
   deriving (Functor)
 
 newtype Yielding b eff m c = Yielding {yielded :: b -> m c}
@@ -36,5 +36,15 @@ newtype Yielding b eff m c = Yielding {yielded :: b -> m c}
 instance ControlFlow (Yielding b) Anything where
   Yielding bmc `cfApply` fa = Yielding \b -> bmc b <*> fa
   Yielding bmc `cfBind` afb = Yielding $ bmc >=> afb
+  cfOnce ogLb member handler (Yielding @_ @eff go) = Yielding \b -> do
+    matchOn (go b) >>= \case
+      Pure a -> runIdentityCf $ handler implying member $ IdentityCf @eff a
+      Impure eff lb ub lifter next -> Eff \_ -> Impure eff lb ub lifter \imply member x ->
+        cfOnce ogLb member handler $ next imply member x
+  cfPutMeIn _ f (Yielding go) = Yielding \b -> do
+    matchOn (go b) >>= \case
+      Pure a -> f a
+      Impure eff lb ub lifter next -> Eff \_ -> Impure eff lb ub lifter \imply member x ->
+        cfPutMeIn member f $ next imply member x
   cfMap _ _ handler (Yielding bmc) = Yielding $ handler . bmc
   cfRun _ handler (Yielding bmc) = Yielding $ handler . bmc