Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add 'Raise' and 'Subsume' #370

Merged
merged 4 commits into from
Jul 29, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 9 additions & 8 deletions src/Polysemy.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,23 +5,23 @@ module Polysemy
, MemberWithError
, Members

-- * Running Sem
-- * Running Sem
, run
, runM
, runFinal

-- * Type synonyms for user convenience
-- * Type synonyms for user convenience
, InterpreterFor

-- * Interoperating With Other Monads
-- ** Embed
-- * Interoperating With Other Monads
-- ** Embed
, Embed (..)
, embed
, embedToFinal

-- ** Final
-- | For advanced uses of 'Final', including creating your own interpreters
-- that make use of it, see "Polysemy.Final"
-- ** Final
-- | For advanced uses of 'Final', including creating your own interpreters
-- that make use of it, see "Polysemy.Final"
, Final
, embedFinal

Expand All @@ -32,6 +32,8 @@ module Polysemy
, raiseUnder3
, raise2Under
, raise3Under
, raise_
, subsume_

-- * Trivial Interpretation
, subsume
Expand Down Expand Up @@ -148,4 +150,3 @@ import Polysemy.Internal.Forklift
import Polysemy.Internal.Kind
import Polysemy.Internal.Tactics
import Polysemy.Internal.TH.Effect

132 changes: 96 additions & 36 deletions src/Polysemy/Internal.hs
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_HADDOCK not-home #-}
Expand All @@ -16,12 +17,16 @@ module Polysemy.Internal
, embed
, run
, runM
, raise_
, Raise (..)
, raise
, raiseUnder
, raiseUnder2
, raiseUnder3
, raise2Under
, raise3Under
, subsume_
, Subsume (..)
, subsume
, subsumeUsing
, Embed (..)
Expand All @@ -43,6 +48,7 @@ import Data.Kind
import Polysemy.Embed.Type
import Polysemy.Fail.Type
import Polysemy.Internal.Fixpoint
import Polysemy.Internal.Kind
import Polysemy.Internal.NonDet
import Polysemy.Internal.PluginLookup
import Polysemy.Internal.Union
Expand Down Expand Up @@ -294,7 +300,7 @@ instance (Member Fail r) => MonadFail (Sem r) where
-- | This instance will only lift 'IO' actions. If you want to lift into some
-- other 'MonadIO' type, use this instance, and handle it via the
-- 'Polysemy.IO.embedToMonadIO' interpretation.
instance (Member (Embed IO) r) => MonadIO (Sem r) where
instance Member (Embed IO) r => MonadIO (Sem r) where
liftIO = embed
{-# INLINE liftIO #-}

Expand All @@ -316,22 +322,51 @@ hoistSem nat (Sem m) = Sem $ \k -> m $ \u -> k $ nat u
{-# INLINE hoistSem #-}


------------------------------------------------------------------------------
-- | Introduce an arbitrary number of effects on top of the effect stack. This
-- function is highly polymorphic, so it may be good idea to use its more
-- concrete versions (like 'raise') or type annotations to avoid vague errors
-- in ambiguous contexts.
--
-- @since 1.4.0.0
raise_ :: ∀ r r' a. Raise r r' => Sem r a -> Sem r' a
raise_ = hoistSem $ hoist raise_ . raiseUnion
{-# INLINE raise #-}


-- | See 'raise''.
--
-- @since 1.4.0.0
class Raise (r :: EffectRow) (r' :: EffectRow) where
raiseUnion :: Union r m a -> Union r' m a

instance {-# overlapping #-} Raise r r where
raiseUnion = id
{-# INLINE raiseUnion #-}

instance (r' ~ (_0 ': r''), Raise r r'') => Raise r r' where
raiseUnion = (\(Union n w) -> Union (There n) w) . raiseUnion
{-# INLINE raiseUnion #-}


------------------------------------------------------------------------------
-- | Introduce an effect into 'Sem'. Analogous to
-- 'Control.Monad.Class.Trans.lift' in the mtl ecosystem
-- 'Control.Monad.Class.Trans.lift' in the mtl ecosystem. For a variant that
-- can introduce an arbitrary number of effects, see 'raise_'.
raise :: ∀ e r a. Sem r a -> Sem (e ': r) a
raise = hoistSem $ hoist raise . weaken
{-# INLINE raise #-}
raise = raise_
{-# INLINE raise_ #-}


------------------------------------------------------------------------------
-- | Like 'raise', but introduces a new effect underneath the head of the
-- list.
-- list. See 'raiseUnder2' or 'raiseUnder3' for introducing more effects. If
-- you need to introduce even more of them, check out 'subsume_'.
--
-- 'raiseUnder' can be used in order to turn transformative interpreters
-- into reinterpreters. This is especially useful if you're writing an interpreter
-- which introduces an intermediary effect, and then want to use an existing
-- interpreter on that effect.
-- into reinterpreters. This is especially useful if you're writing an
-- interpreter which introduces an intermediary effect, and then want to use
-- an existing interpreter on that effect.
--
-- For example, given:
--
Expand All @@ -352,12 +387,7 @@ raise = hoistSem $ hoist raise . weaken
--
-- @since 1.2.0.0
raiseUnder :: ∀ e2 e1 r a. Sem (e1 ': r) a -> Sem (e1 ': e2 ': r) a
raiseUnder = hoistSem $ hoist raiseUnder . weakenUnder
where
weakenUnder :: ∀ m x. Union (e1 ': r) m x -> Union (e1 ': e2 ': r) m x
weakenUnder (Union Here a) = Union Here a
weakenUnder (Union (There n) a) = Union (There (There n)) a
{-# INLINE weakenUnder #-}
raiseUnder = subsume_
{-# INLINE raiseUnder #-}


Expand All @@ -367,12 +397,7 @@ raiseUnder = hoistSem $ hoist raiseUnder . weakenUnder
--
-- @since 1.2.0.0
raiseUnder2 :: ∀ e2 e3 e1 r a. Sem (e1 ': r) a -> Sem (e1 ': e2 ': e3 ': r) a
raiseUnder2 = hoistSem $ hoist raiseUnder2 . weakenUnder2
where
weakenUnder2 :: ∀ m x. Union (e1 ': r) m x -> Union (e1 ': e2 ': e3 ': r) m x
weakenUnder2 (Union Here a) = Union Here a
weakenUnder2 (Union (There n) a) = Union (There (There (There n))) a
{-# INLINE weakenUnder2 #-}
raiseUnder2 = subsume_
{-# INLINE raiseUnder2 #-}


Expand All @@ -382,12 +407,7 @@ raiseUnder2 = hoistSem $ hoist raiseUnder2 . weakenUnder2
--
-- @since 1.2.0.0
raiseUnder3 :: ∀ e2 e3 e4 e1 r a. Sem (e1 ': r) a -> Sem (e1 ': e2 ': e3 ': e4 ': r) a
raiseUnder3 = hoistSem $ hoist raiseUnder3 . weakenUnder3
where
weakenUnder3 :: ∀ m x. Union (e1 ': r) m x -> Union (e1 ': e2 ': e3 ': e4 ': r) m x
weakenUnder3 (Union Here a) = Union Here a
weakenUnder3 (Union (There n) a) = Union (There (There (There (There n)))) a
{-# INLINE weakenUnder3 #-}
raiseUnder3 = subsume_
{-# INLINE raiseUnder3 #-}


Expand Down Expand Up @@ -423,6 +443,40 @@ raise3Under = hoistSem $ hoist raise3Under . weaken3Under
{-# INLINE weaken3Under #-}
{-# INLINE raise3Under #-}


------------------------------------------------------------------------------
-- | Allows reordering and adding known effects on top of the effect stack, as
-- long as the polymorphic "tail" of new stack is a 'raise'-d version of the
-- original one. This function is highly polymorphic, so it may be a good idea
-- to use its more concrete version ('subsume'), fitting functions from the
-- 'raise' family or type annotations to avoid vague errors in ambiguous
-- contexts.
--
-- @since 1.4.0.0
subsume_ :: ∀ r r' a. Subsume r r' => Sem r a -> Sem r' a
subsume_ = hoistSem $ hoist subsume_ . subsumeUnion
{-# INLINE subsume_ #-}


-- | See 'subsume_'.
--
-- @since 1.4.0.0
class Subsume (r :: EffectRow) (r' :: EffectRow) where
subsumeUnion :: Union r m a -> Union r' m a

instance {-# incoherent #-} Raise r r' => Subsume r r' where
subsumeUnion = raiseUnion
{-# INLINE subsumeUnion #-}

instance (Member e r', Subsume r r') => Subsume (e ': r) r' where
subsumeUnion = either subsumeUnion injWeaving . decomp
{-# INLINE subsumeUnion #-}

instance Subsume '[] r where
subsumeUnion = absurdU
{-# INLINE subsumeUnion #-}


------------------------------------------------------------------------------
-- | Interprets an effect in terms of another identical effect.
--
Expand All @@ -431,11 +485,15 @@ raise3Under = hoistSem $ hoist raise3Under . weaken3Under
-- Using such an interpreter recursively may result in duplicate effects,
-- which may then be eliminated using 'subsume'.
--
-- For a version that can introduce an arbitrary number of new effects and
-- reorder existing ones, see 'subsume_'.
--
-- @since 1.2.0.0
subsume :: Member e r => Sem (e ': r) a -> Sem r a
subsume = subsumeUsing membership
subsume :: ∀ e r a. Member e r => Sem (e ': r) a -> Sem r a
subsume = subsume_
{-# INLINE subsume #-}


------------------------------------------------------------------------------
-- | Interprets an effect in terms of another identical effect, given an
-- explicit proof that the effect exists in @r@.
Expand All @@ -451,10 +509,10 @@ subsume = subsumeUsing membership
-- @
--
-- @since 1.3.0.0
subsumeUsing :: forall e r a. ElemOf e r -> Sem (e ': r) a -> Sem r a
subsumeUsing :: e r a. ElemOf e r -> Sem (e ': r) a -> Sem r a
subsumeUsing pr =
let
go :: forall x. Sem (e ': r) x -> Sem r x
go :: x. Sem (e ': r) x -> Sem r x
go = hoistSem $ \u -> hoist go $ case decomp u of
Right w -> Union pr w
Left g -> g
Expand All @@ -471,6 +529,7 @@ send :: Member e r => e (Sem r) a -> Sem r a
send = liftSem . inj
{-# INLINE[3] send #-}


------------------------------------------------------------------------------
-- | Embed an effect into a 'Sem', given an explicit proof
-- that the effect exists in @r@.
Expand Down Expand Up @@ -509,6 +568,7 @@ runM (Sem m) = m $ \z ->
pure $ f $ a <$ s
{-# INLINE runM #-}


------------------------------------------------------------------------------
-- | Type synonym for interpreters that consume an effect without changing the
-- return value. Offered for user convenience.
Expand All @@ -519,7 +579,8 @@ runM (Sem m) = m $ \z ->
-- teletypeToIO :: 'Member' (Embed IO) r
-- => 'InterpreterFor' Teletype r
-- @
type InterpreterFor e r = forall a. Sem (e ': r) a -> Sem r a
type InterpreterFor e r = ∀ a. Sem (e ': r) a -> Sem r a


------------------------------------------------------------------------------
-- | Some interpreters need to be able to lower down to the base monad (often
Expand Down Expand Up @@ -582,4 +643,3 @@ infixl 8 .@
-> m (f z)
f .@@ g = f . g f
infixl 8 .@@