mirror of
https://github.com/polysemy-research/polysemy.git
synced 2024-09-11 10:36:40 +03:00
Membership proof rewrite, membership testing, Bundle effect (#282)
* Union rewrite * Exports, tests, and renamed KnownEffectRow * Got rid of artifacts accidently introduced * More documentation. tryMembership seperate from KnownRow * 'expose' combinator * Applied review suggestions, add Membership module * Fixed a replace-all goof * Scrap expose/Using in favor of interceptUsing/H * Fixed Haddock failure
This commit is contained in:
KingoftheHomeless
GitHub
parent
fc508de2ec
commit
a4868bddd4
@ -76,7 +76,7 @@ data FindConstraint = FindConstraint
|
||||
-- | Given a list of constraints, filter out the 'FindConstraint's.
|
||||
getFindConstraints :: PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
|
||||
getFindConstraints (findClass -> cls) cts = do
|
||||
cd@CDictCan{cc_class = cls', cc_tyargs = [_, r, eff]} <- cts
|
||||
cd@CDictCan{cc_class = cls', cc_tyargs = [_, eff, r]} <- cts
|
||||
guard $ cls == cls'
|
||||
pure $ FindConstraint
|
||||
{ fcLoc = ctLoc cd
|
||||
@ -163,7 +163,7 @@ extractRowFromSem (semTyCon -> sem) ty = do
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Given a list of bogus @r@s, and the wanted constraints, produce bogus
|
||||
-- evidence terms that will prevent @IfStuck (IndexOf r _) _ _@ error messsages.
|
||||
-- evidence terms that will prevent @IfStuck (LocateEffect _ r) _ _@ error messsages.
|
||||
solveBogusError :: PolysemyStuff 'Things -> [Ct] -> [(EvTerm, Ct)]
|
||||
solveBogusError stuff wanteds = do
|
||||
let splitTyConApp_list = maybeToList . splitTyConApp_maybe
|
||||
@ -172,8 +172,8 @@ solveBogusError stuff wanteds = do
|
||||
ct@(CIrredCan ce _) <- wanteds
|
||||
(stuck, [_, _, expr, _, _]) <- splitTyConApp_list $ ctev_pred ce
|
||||
guard $ stuck == ifStuckTyCon stuff
|
||||
(idx, [_, r, _]) <- splitTyConApp_list expr
|
||||
guard $ idx == indexOfTyCon stuff
|
||||
(idx, [_, _, r]) <- splitTyConApp_list expr
|
||||
guard $ idx == locateEffectTyCon stuff
|
||||
guard $ elem @[] (OrdType r) $ coerce bogus
|
||||
pure (error "bogus proof for stuck type family", ct)
|
||||
|
||||
|
||||
@ -23,10 +23,10 @@ import Outputable (pprPanic, empty, text, (<+>), ($$))
|
||||
-- When @l ~ 'Locations@, each of these is just a pair of strings. When @l
|
||||
-- ~ 'Things@, it's actually references to the stuff.
|
||||
data PolysemyStuff (l :: LookupState) = PolysemyStuff
|
||||
{ findClass :: ThingOf l Class
|
||||
, semTyCon :: ThingOf l TyCon
|
||||
, ifStuckTyCon :: ThingOf l TyCon
|
||||
, indexOfTyCon :: ThingOf l TyCon
|
||||
{ findClass :: ThingOf l Class
|
||||
, semTyCon :: ThingOf l TyCon
|
||||
, ifStuckTyCon :: ThingOf l TyCon
|
||||
, locateEffectTyCon :: ThingOf l TyCon
|
||||
}
|
||||
|
||||
|
||||
@ -34,10 +34,10 @@ data PolysemyStuff (l :: LookupState) = PolysemyStuff
|
||||
-- | All of the things we need to lookup.
|
||||
polysemyStuffLocations :: PolysemyStuff 'Locations
|
||||
polysemyStuffLocations = PolysemyStuff
|
||||
{ findClass = ("Polysemy.Internal.Union", "Find")
|
||||
, semTyCon = ("Polysemy.Internal", "Sem")
|
||||
, ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")
|
||||
, indexOfTyCon = ("Polysemy.Internal.Union", "IndexOf")
|
||||
{ findClass = ("Polysemy.Internal.Union", "Find")
|
||||
, semTyCon = ("Polysemy.Internal", "Sem")
|
||||
, ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")
|
||||
, locateEffectTyCon = ("Polysemy.Internal.Union", "LocateEffect")
|
||||
}
|
||||
|
||||
|
||||
|
||||
@ -4,7 +4,7 @@ cabal-version: 1.24
|
||||
--
|
||||
-- see: https://github.com/sol/hpack
|
||||
--
|
||||
-- hash: aac2227e71e3a98458fa5746be7fcbb87da0dc342cdd53913041c95c128871fe
|
||||
-- hash: 582807c5d69a34a9e991a77c6111532c05dbb54a5d7aa6662267b7af2d3047ee
|
||||
|
||||
name: polysemy
|
||||
version: 1.2.3.0
|
||||
@ -48,6 +48,7 @@ library
|
||||
Polysemy
|
||||
Polysemy.Async
|
||||
Polysemy.AtomicState
|
||||
Polysemy.Bundle
|
||||
Polysemy.Embed
|
||||
Polysemy.Embed.Type
|
||||
Polysemy.Error
|
||||
@ -57,6 +58,7 @@ library
|
||||
Polysemy.Fixpoint
|
||||
Polysemy.Input
|
||||
Polysemy.Internal
|
||||
Polysemy.Internal.Bundle
|
||||
Polysemy.Internal.Combinators
|
||||
Polysemy.Internal.CustomErrors
|
||||
Polysemy.Internal.CustomErrors.Redefined
|
||||
@ -72,6 +74,7 @@ library
|
||||
Polysemy.Internal.Writer
|
||||
Polysemy.IO
|
||||
Polysemy.Law
|
||||
Polysemy.Membership
|
||||
Polysemy.NonDet
|
||||
Polysemy.Output
|
||||
Polysemy.Reader
|
||||
@ -134,6 +137,7 @@ test-suite polysemy-test
|
||||
HigherOrderSpec
|
||||
InspectorSpec
|
||||
InterceptSpec
|
||||
KnownRowSpec
|
||||
LawsSpec
|
||||
OutputSpec
|
||||
ThEffectSpec
|
||||
|
||||
76
src/Polysemy/Bundle.hs
Normal file
76
src/Polysemy/Bundle.hs
Normal file
@ -0,0 +1,76 @@
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
module Polysemy.Bundle
|
||||
( -- * Effect
|
||||
Bundle (..)
|
||||
-- * Actions
|
||||
, sendBundle
|
||||
, injBundle
|
||||
-- * Interpretations
|
||||
, runBundle
|
||||
, subsumeBundle
|
||||
-- * Miscellaneous
|
||||
, KnownList
|
||||
) where
|
||||
|
||||
import Polysemy
|
||||
import Polysemy.Internal
|
||||
import Polysemy.Internal.Bundle
|
||||
import Polysemy.Internal.Union
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | An effect for collecting multiple effects into one effect.
|
||||
--
|
||||
-- Useful for effect newtypes -- effects defined through creating a newtype
|
||||
-- over an existing effect, and then defining actions and interpretations on
|
||||
-- the newtype by using 'rewrite' and 'transform'.
|
||||
--
|
||||
-- By making a newtype of 'Bundle', it's possible to wrap multiple effects in
|
||||
-- one newtype.
|
||||
data Bundle r m a where
|
||||
Bundle :: ElemOf e r -> e m a -> Bundle r m a
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Injects an effect into a 'Bundle'. Useful together with 'transform'.
|
||||
injBundle :: forall e r m a. Member e r => e m a -> Bundle r m a
|
||||
injBundle = Bundle membership
|
||||
{-# INLINE injBundle #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Send uses of an effect to a 'Bundle' containing that effect.
|
||||
sendBundle
|
||||
:: forall e r' r a
|
||||
. (Member e r', Member (Bundle r') r)
|
||||
=> Sem (e ': r) a
|
||||
-> Sem r a
|
||||
sendBundle = hoistSem $ \u -> case decomp u of
|
||||
Right (Weaving e s wv ex ins) ->
|
||||
injWeaving $
|
||||
Weaving (Bundle (membership @e @r') e) s (sendBundle @e @r' . wv) ex ins
|
||||
Left g -> hoist (sendBundle @e @r') g
|
||||
{-# INLINE sendBundle #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Run a @'Bundle' r@ by prepending @r@ to the effect stack.
|
||||
runBundle
|
||||
:: forall r' r a
|
||||
. KnownList r'
|
||||
=> Sem (Bundle r' ': r) a
|
||||
-> Sem (Append r' r) a
|
||||
runBundle = hoistSem $ \u -> hoist runBundle $ case decomp u of
|
||||
Right (Weaving (Bundle pr e) s wv ex ins) ->
|
||||
Union (extendMembership @_ @r pr) $ Weaving e s wv ex ins
|
||||
Left g -> weakenList @r' @r g
|
||||
{-# INLINE runBundle #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Run a @'Bundle' r@ if the effect stack contains all effects of @r@.
|
||||
subsumeBundle
|
||||
:: forall r' r a
|
||||
. Members r' r
|
||||
=> Sem (Bundle r' ': r) a
|
||||
-> Sem r a
|
||||
subsumeBundle = hoistSem $ \u -> hoist subsumeBundle $ case decomp u of
|
||||
Right (Weaving (Bundle pr e) s wv ex ins) ->
|
||||
Union (subsumeMembership pr) (Weaving e s wv ex ins)
|
||||
Left g -> g
|
||||
{-# INLINE subsumeBundle #-}
|
||||
@ -12,6 +12,7 @@ module Polysemy.Internal
|
||||
, MemberWithError
|
||||
, Members
|
||||
, send
|
||||
, sendUsing
|
||||
, embed
|
||||
, run
|
||||
, runM
|
||||
@ -20,6 +21,7 @@ module Polysemy.Internal
|
||||
, raiseUnder2
|
||||
, raiseUnder3
|
||||
, subsume
|
||||
, subsumeUsing
|
||||
, Embed (..)
|
||||
, usingSem
|
||||
, liftSem
|
||||
@ -351,8 +353,8 @@ 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 SZ a) = Union SZ a
|
||||
weakenUnder (Union (SS n) a) = Union (SS (SS n)) a
|
||||
weakenUnder (Union Here a) = Union Here a
|
||||
weakenUnder (Union (There n) a) = Union (There (There n)) a
|
||||
{-# INLINE weakenUnder #-}
|
||||
{-# INLINE raiseUnder #-}
|
||||
|
||||
@ -366,14 +368,14 @@ 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 SZ a) = Union SZ a
|
||||
weakenUnder2 (Union (SS n) a) = Union (SS (SS (SS n))) a
|
||||
weakenUnder2 (Union Here a) = Union Here a
|
||||
weakenUnder2 (Union (There n) a) = Union (There (There (There n))) a
|
||||
{-# INLINE weakenUnder2 #-}
|
||||
{-# INLINE raiseUnder2 #-}
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Like 'raise', but introduces two new effects underneath the head of the
|
||||
-- | Like 'raise', but introduces three new effects underneath the head of the
|
||||
-- list.
|
||||
--
|
||||
-- @since 1.2.0.0
|
||||
@ -381,8 +383,8 @@ raiseUnder3 :: ∀ e2 e3 e4 e1 r a. Sem (e1 ': r) a -> Sem (e1 ': e2 ': e3 ': e4
|
||||
raiseUnder3 = hoistSem $ hoist raiseUnder3 . weakenUnder3
|
||||
where
|
||||
weakenUnder3 :: ∀ m x. Union (e1 ': r) m x -> Union (e1 ': e2 ': e3 ': e4 ': r) m x
|
||||
weakenUnder3 (Union SZ a) = Union SZ a
|
||||
weakenUnder3 (Union (SS n) a) = Union (SS (SS (SS (SS n)))) a
|
||||
weakenUnder3 (Union Here a) = Union Here a
|
||||
weakenUnder3 (Union (There n) a) = Union (There (There (There (There n)))) a
|
||||
{-# INLINE weakenUnder3 #-}
|
||||
{-# INLINE raiseUnder3 #-}
|
||||
|
||||
@ -396,11 +398,37 @@ raiseUnder3 = hoistSem $ hoist raiseUnder3 . weakenUnder3
|
||||
--
|
||||
-- @since 1.2.0.0
|
||||
subsume :: Member e r => Sem (e ': r) a -> Sem r a
|
||||
subsume = hoistSem $ \u -> hoist subsume $ case decomp u of
|
||||
Right w -> injWeaving w
|
||||
Left g -> g
|
||||
subsume = subsumeUsing membership
|
||||
{-# INLINE subsume #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Interprets an effect in terms of another identical effect, given an
|
||||
-- explicit proof that the effect exists in @r@.
|
||||
--
|
||||
-- This is useful in conjunction with 'Polysemy.Membership.tryMembership'
|
||||
-- in order to conditionally make use of effects. For example:
|
||||
--
|
||||
-- @
|
||||
-- tryListen :: 'Polysemy.Membership.KnownRow' r => 'Sem' r a -> Maybe ('Sem' r ([Int], a))
|
||||
-- tryListen m = case 'Polysemy.Membership.tryMembership' @('Polysemy.Writer.Writer' [Int]) of
|
||||
-- Just pr -> Just $ 'subsumeUsing' pr ('Polysemy.Writer.listen' ('raise' m))
|
||||
-- _ -> Nothing
|
||||
-- @
|
||||
--
|
||||
-- @since TODO
|
||||
subsumeUsing :: forall 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 = hoistSem $ \u -> hoist go $ case decomp u of
|
||||
Right w -> Union pr w
|
||||
Left g -> g
|
||||
{-# INLINE go #-}
|
||||
in
|
||||
go
|
||||
{-# INLINE subsumeUsing #-}
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Embed an effect into a 'Sem'. This is used primarily via
|
||||
-- 'Polysemy.makeSem' to implement smart constructors.
|
||||
@ -408,6 +436,16 @@ 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@.
|
||||
--
|
||||
-- This is useful in conjunction with 'Polysemy.Membership.tryMembership',
|
||||
-- in order to conditionally make use of effects.
|
||||
sendUsing :: ElemOf e r -> e (Sem r) a -> Sem r a
|
||||
sendUsing pr = liftSem . injUsing pr
|
||||
{-# INLINE[3] sendUsing #-}
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Embed a monadic action @m@ in 'Sem'.
|
||||
|
||||
55
src/Polysemy/Internal/Bundle.hs
Normal file
55
src/Polysemy/Internal/Bundle.hs
Normal file
@ -0,0 +1,55 @@
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
|
||||
{-# OPTIONS_HADDOCK not-home #-}
|
||||
|
||||
module Polysemy.Internal.Bundle where
|
||||
|
||||
import Data.Proxy
|
||||
import Polysemy
|
||||
import Polysemy.Internal.Union
|
||||
|
||||
type family Append l r where
|
||||
Append (a ': l) r = a ': (Append l r)
|
||||
Append '[] r = r
|
||||
|
||||
extendMembership :: forall r r' e. ElemOf e r -> ElemOf e (Append r r')
|
||||
extendMembership Here = Here
|
||||
extendMembership (There e) = There (extendMembership @_ @r' e)
|
||||
{-# INLINE extendMembership #-}
|
||||
|
||||
subsumeMembership :: forall r r' e. Members r r' => ElemOf e r -> ElemOf e r'
|
||||
subsumeMembership Here = membership @e @r'
|
||||
subsumeMembership (There (pr :: ElemOf e r'')) = subsumeMembership @r'' @r' pr
|
||||
{-# INLINE subsumeMembership #-}
|
||||
|
||||
weakenList :: forall r' r m a
|
||||
. KnownList r'
|
||||
=> Union r m a
|
||||
-> Union (Append r' r) m a
|
||||
weakenList u = unconsKnownList @_ @r' u (\_ (_ :: Proxy r'') -> weaken (weakenList @r'' u))
|
||||
{-# INLINE weakenList #-}
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | A class for type-level lists with a known spine.
|
||||
--
|
||||
-- This constraint is eventually satisfied as @r@ is instantied to a
|
||||
-- concrete list.
|
||||
class KnownList (l :: [k]) where
|
||||
unconsKnownList :: (l ~ '[] => a)
|
||||
-> ( forall x r
|
||||
. (l ~ (x ': r), KnownList r)
|
||||
=> Proxy x
|
||||
-> Proxy r
|
||||
-> a
|
||||
)
|
||||
-> a
|
||||
|
||||
instance KnownList '[] where
|
||||
unconsKnownList b _ = b
|
||||
{-# INLINE unconsKnownList #-}
|
||||
|
||||
instance KnownList r => KnownList (x ': r) where
|
||||
unconsKnownList _ b = b Proxy Proxy
|
||||
{-# INLINE unconsKnownList #-}
|
||||
|
||||
@ -19,6 +19,10 @@ module Polysemy.Internal.Combinators
|
||||
, reinterpret2H
|
||||
, reinterpret3H
|
||||
|
||||
-- * Conditional
|
||||
, interceptUsing
|
||||
, interceptUsingH
|
||||
|
||||
-- * Statefulness
|
||||
, stateful
|
||||
, lazilyStateful
|
||||
@ -281,13 +285,55 @@ interceptH
|
||||
-> Sem r a
|
||||
-- ^ Unlike 'interpretH', 'interceptH' does not consume any effects.
|
||||
-> Sem r a
|
||||
interceptH f (Sem m) = Sem $ \k -> m $ \u ->
|
||||
case prj u of
|
||||
Just (Weaving e s d y v) ->
|
||||
usingSem k $ fmap y $ runTactics s (raise . d) v $ f e
|
||||
Nothing -> k $ hoist (interceptH f) u
|
||||
interceptH = interceptUsingH membership
|
||||
{-# INLINE interceptH #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | A variant of 'intercept' that accepts an explicit proof that the effect
|
||||
-- is in the effect stack rather then requiring a 'Member' constraint.
|
||||
--
|
||||
-- This is useful in conjunction with 'Polysemy.Membership.tryMembership'
|
||||
-- in order to conditionally perform 'intercept'.
|
||||
interceptUsing
|
||||
:: FirstOrder e "interceptUsing"
|
||||
=> ElemOf e r
|
||||
-- ^ A proof that the handled effect exists in @r@.
|
||||
-- This can be retrieved through 'Polysemy.Membership.membership' or
|
||||
-- 'Polysemy.Membership.tryMembership'.
|
||||
-> (∀ x m. e m x -> Sem r x)
|
||||
-- ^ A natural transformation from the handled effect to other effects
|
||||
-- already in 'Sem'.
|
||||
-> Sem r a
|
||||
-- ^ Unlike 'interpret', 'intercept' does not consume any effects.
|
||||
-> Sem r a
|
||||
interceptUsing pr f = interceptUsingH pr $ \(e :: e m x) -> liftT @m $ f e
|
||||
{-# INLINE interceptUsing #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | A variant of 'interceptH' that accepts an explicit proof that the effect
|
||||
-- is in the effect stack rather then requiring a 'Member' constraint.
|
||||
--
|
||||
-- This is useful in conjunction with 'Polysemy.Membership.tryMembership'
|
||||
-- in order to conditionally perform 'interceptH'.
|
||||
--
|
||||
-- See the notes on 'Tactical' for how to use this function.
|
||||
interceptUsingH
|
||||
:: ElemOf e r
|
||||
-- ^ A proof that the handled effect exists in @r@.
|
||||
-- This can be retrieved through 'Polysemy.Membership.membership' or
|
||||
-- 'Polysemy.Membership.tryMembership'.
|
||||
-> (∀ x m. e m x -> Tactical e m r x)
|
||||
-- ^ A natural transformation from the handled effect to other effects
|
||||
-- already in 'Sem'.
|
||||
-> Sem r a
|
||||
-- ^ Unlike 'interpretH', 'interceptUsingH' does not consume any effects.
|
||||
-> Sem r a
|
||||
interceptUsingH pr f (Sem m) = Sem $ \k -> m $ \u ->
|
||||
case prjUsing pr u of
|
||||
Just (Weaving e s d y v) ->
|
||||
usingSem k $ fmap y $ runTactics s (raise . d) v $ f e
|
||||
Nothing -> k $ hoist (interceptUsingH pr f) u
|
||||
{-# INLINE interceptUsingH #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Rewrite an effect @e1@ directly into @e2@, and put it on the top of the
|
||||
@ -302,7 +348,7 @@ rewrite
|
||||
rewrite f (Sem m) = Sem $ \k -> m $ \u ->
|
||||
k $ hoist (rewrite f) $ case decompCoerce u of
|
||||
Left x -> x
|
||||
Right (Weaving e s d n y) -> injWeaving $ Weaving (f e) s d n y
|
||||
Right (Weaving e s d n y) -> Union Here $ Weaving (f e) s d n y
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
@ -76,7 +76,7 @@ type AmbigousEffectMessage (rstate :: EffectRowCtor)
|
||||
% " " <> PrettyPrintList vs <> " directly, or activate polysemy-plugin which"
|
||||
% " can usually infer the type correctly."
|
||||
|
||||
type AmbiguousSend r e =
|
||||
type AmbiguousSend e r =
|
||||
(IfStuck r
|
||||
(AmbiguousSendError 'TyVarR r e)
|
||||
(Pure (AmbiguousSendError (UnstuckRState r) r e)))
|
||||
|
||||
@ -100,7 +100,7 @@ getInitialStateT = send @(Tactics _ m (e ': r)) GetInitialState
|
||||
--
|
||||
-- ==== Example
|
||||
--
|
||||
-- We can use the result of 'getInspectT' to "undo" 'pureT' (or any of the other
|
||||
-- We can use the result of 'getInspectorT' to "undo" 'pureT' (or any of the other
|
||||
-- 'Tactical' functions):
|
||||
--
|
||||
-- @
|
||||
|
||||
@ -1,8 +1,10 @@
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE EmptyCase #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE FunctionalDependencies #-}
|
||||
{-# LANGUAGE InstanceSigs #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE StrictData #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
@ -20,24 +22,30 @@ module Polysemy.Internal.Union
|
||||
, hoist
|
||||
-- * Building Unions
|
||||
, inj
|
||||
, injUsing
|
||||
, injWeaving
|
||||
, weaken
|
||||
-- * Using Unions
|
||||
, decomp
|
||||
, prj
|
||||
, prjUsing
|
||||
, extract
|
||||
, absurdU
|
||||
, decompCoerce
|
||||
-- * Witnesses
|
||||
, SNat (..)
|
||||
, Nat (..)
|
||||
, ElemOf (..)
|
||||
, membership
|
||||
, sameMember
|
||||
-- * Checking membership
|
||||
, KnownRow
|
||||
, tryMembership
|
||||
) where
|
||||
|
||||
import Control.Monad
|
||||
import Data.Functor.Compose
|
||||
import Data.Functor.Identity
|
||||
import Data.Kind
|
||||
import Data.Type.Equality
|
||||
import Data.Typeable
|
||||
import Polysemy.Internal.Kind
|
||||
|
||||
#ifndef NO_ERROR_MESSAGES
|
||||
@ -51,10 +59,10 @@ import Polysemy.Internal.CustomErrors
|
||||
data Union (r :: EffectRow) (m :: Type -> Type) a where
|
||||
Union
|
||||
:: -- A proof that the effect is actually in @r@.
|
||||
SNat n
|
||||
ElemOf e r
|
||||
-- The effect to wrap. The functions 'prj' and 'decomp' can help
|
||||
-- retrieve this value later.
|
||||
-> Weaving (IndexOf r n) m a
|
||||
-> Weaving e m a
|
||||
-> Union r m a
|
||||
|
||||
instance Functor (Union r m) where
|
||||
@ -129,74 +137,118 @@ type Member e r = MemberNoError e r
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Like 'Member', but will produce an error message if the types are
|
||||
-- ambiguous.
|
||||
-- ambiguous. This is the constraint used for actions generated by
|
||||
-- 'Polysemy.makeSem'.
|
||||
--
|
||||
-- @since TODO
|
||||
-- /Be careful with this./ Due to quirks of 'GHC.TypeLits.TypeError',
|
||||
-- the custom error messages emitted by this can potentially override other,
|
||||
-- more helpful error messages.
|
||||
-- See the discussion in
|
||||
-- <https://github.com/polysemy-research/polysemy/issues/227 Issue #227>.
|
||||
--
|
||||
-- @since 1.2.3.0
|
||||
type MemberWithError e r =
|
||||
( MemberNoError e r
|
||||
#ifndef NO_ERROR_MESSAGES
|
||||
-- NOTE: The plugin explicitly pattern matches on
|
||||
-- `WhenStuck (IndexOf r _) _`, so if you change this, make sure to change
|
||||
-- `WhenStuck (LocateEffect _ r) _`, so if you change this, make sure to change
|
||||
-- the corresponding implementation in
|
||||
-- Polysemy.Plugin.Fundep.solveBogusError
|
||||
, WhenStuck (IndexOf r (Found r e)) (AmbiguousSend r e)
|
||||
, WhenStuck (LocateEffect e r) (AmbiguousSend e r)
|
||||
#endif
|
||||
)
|
||||
|
||||
type MemberNoError e r =
|
||||
( Find r e
|
||||
, e ~ IndexOf r (Found r e)
|
||||
( Find e r
|
||||
#ifndef NO_ERROR_MESSAGES
|
||||
, LocateEffect e r ~ '()
|
||||
#endif
|
||||
)
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | A proof that @e@ is an element of @r@.
|
||||
--
|
||||
-- Due to technical reasons, @'ElemOf' e r@ is not powerful enough to
|
||||
-- prove @'Member' e r@; however, it can still be used send actions of @e@
|
||||
-- into @r@ by using 'Polysemy.Internal.subsumeUsing'.
|
||||
data ElemOf e r where
|
||||
-- | @e@ is located at the head of the list.
|
||||
Here :: ElemOf e (e ': r)
|
||||
-- | @e@ is located somewhere in the tail of the list.
|
||||
There :: ElemOf e r -> ElemOf e (e' ': r)
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | The kind of type-level natural numbers.
|
||||
data Nat = Z | S Nat
|
||||
-- | Checks if two membership proofs are equal. If they are, then that means
|
||||
-- that the effects for which membership is proven must also be equal.
|
||||
sameMember :: forall e e' r
|
||||
. ElemOf e r
|
||||
-> ElemOf e' r
|
||||
-> Maybe (e :~: e')
|
||||
sameMember Here Here =
|
||||
Just Refl
|
||||
sameMember (There pr) (There pr') =
|
||||
sameMember @e @e' pr pr'
|
||||
sameMember (There _) _ =
|
||||
Nothing
|
||||
sameMember _ _ =
|
||||
Nothing
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | A singleton for 'Nat'.
|
||||
data SNat :: Nat -> Type where
|
||||
SZ :: SNat 'Z
|
||||
SS :: SNat n -> SNat ('S n)
|
||||
|
||||
instance TestEquality SNat where
|
||||
testEquality SZ SZ = Just Refl
|
||||
testEquality (SS _) SZ = Nothing
|
||||
testEquality SZ (SS _) = Nothing
|
||||
testEquality (SS n) (SS m) =
|
||||
case testEquality n m of
|
||||
Nothing -> Nothing
|
||||
Just Refl -> Just Refl
|
||||
{-# INLINE testEquality #-}
|
||||
|
||||
|
||||
type family IndexOf (ts :: [k]) (n :: Nat) :: k where
|
||||
IndexOf (k ': ks) 'Z = k
|
||||
IndexOf (k ': ks) ('S n) = IndexOf ks n
|
||||
|
||||
|
||||
type family Found (ts :: [k]) (t :: k) :: Nat where
|
||||
-- | Used to detect ambiguous uses of effects. If @r@ isn't concrete,
|
||||
-- and we haven't been given @'LocateEffect' e r ~ '()@ from a
|
||||
-- @'Member' e r@ constraint, then @'LocateEffect' e r@ will get stuck.
|
||||
type family LocateEffect (t :: k) (ts :: [k]) :: () where
|
||||
#ifndef NO_ERROR_MESSAGES
|
||||
Found '[] t = UnhandledEffect t
|
||||
LocateEffect t '[] = UnhandledEffect t
|
||||
#endif
|
||||
Found (t ': ts) t = 'Z
|
||||
Found (u ': ts) t = 'S (Found ts t)
|
||||
LocateEffect t (t ': ts) = '()
|
||||
LocateEffect t (u ': ts) = LocateEffect t ts
|
||||
|
||||
class Find (t :: k) (r :: [k]) where
|
||||
membership' :: ElemOf t r
|
||||
|
||||
class Find (r :: [k]) (t :: k) where
|
||||
finder :: SNat (Found r t)
|
||||
instance {-# OVERLAPPING #-} Find t (t ': z) where
|
||||
membership' = Here
|
||||
{-# INLINE membership' #-}
|
||||
|
||||
instance {-# OVERLAPPING #-} Find (t ': z) t where
|
||||
finder = SZ
|
||||
{-# INLINE finder #-}
|
||||
instance Find t z => Find t (_1 ': z) where
|
||||
membership' = There $ membership' @_ @t @z
|
||||
{-# INLINE membership' #-}
|
||||
|
||||
instance ( Find z t
|
||||
, Found (_1 ': z) t ~ 'S (Found z t)
|
||||
) => Find (_1 ': z) t where
|
||||
finder = SS $ finder @_ @z @t
|
||||
{-# INLINE finder #-}
|
||||
------------------------------------------------------------------------------
|
||||
-- | A class for effect rows whose elements are inspectable.
|
||||
--
|
||||
-- This constraint is eventually satisfied as @r@ is instantied to a
|
||||
-- monomorphic list.
|
||||
-- (E.g when @r@ becomes something like
|
||||
-- @'['Polysemy.State.State' Int, 'Polysemy.Output.Output' String, 'Polysemy.Embed' IO]@)
|
||||
class KnownRow r where
|
||||
tryMembership' :: forall e. Typeable e => Maybe (ElemOf e r)
|
||||
|
||||
instance KnownRow '[] where
|
||||
tryMembership' = Nothing
|
||||
{-# INLINE tryMembership' #-}
|
||||
|
||||
instance (Typeable e, KnownRow r) => KnownRow (e ': r) where
|
||||
tryMembership' :: forall e'. Typeable e' => Maybe (ElemOf e' (e ': r))
|
||||
tryMembership' = case eqT @e @e' of
|
||||
Just Refl -> Just Here
|
||||
_ -> There <$> tryMembership' @r @e'
|
||||
{-# INLINE tryMembership' #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Given @'Member' e r@, extract a proof that @e@ is an element of @r@.
|
||||
membership :: Member e r => ElemOf e r
|
||||
membership = membership'
|
||||
{-# INLINE membership #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Extracts a proof that @e@ is an element of @r@ if that
|
||||
-- is indeed the case; otherwise returns @Nothing@.
|
||||
tryMembership :: forall e r. (Typeable e, KnownRow r) => Maybe (ElemOf e r)
|
||||
tryMembership = tryMembership' @r @e
|
||||
{-# INLINE tryMembership #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Decompose a 'Union'. Either this union contains an effect @e@---the head
|
||||
@ -204,29 +256,28 @@ instance ( Find z t
|
||||
decomp :: Union (e ': r) m a -> Either (Union r m a) (Weaving e m a)
|
||||
decomp (Union p a) =
|
||||
case p of
|
||||
SZ -> Right a
|
||||
SS n -> Left $ Union n a
|
||||
Here -> Right a
|
||||
There pr -> Left $ Union pr a
|
||||
{-# INLINE decomp #-}
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Retrieve the last effect in a 'Union'.
|
||||
extract :: Union '[e] m a -> Weaving e m a
|
||||
extract (Union SZ a) = a
|
||||
extract _ = error "impossible"
|
||||
extract (Union Here a) = a
|
||||
extract (Union (There g) _) = case g of {}
|
||||
{-# INLINE extract #-}
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | An empty union contains nothing, so this function is uncallable.
|
||||
absurdU :: Union '[] m a -> b
|
||||
absurdU = absurdU
|
||||
absurdU (Union pr _) = case pr of {}
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Weaken a 'Union' so it is capable of storing a new sort of effect.
|
||||
weaken :: forall e r m a. Union r m a -> Union (e ': r) m a
|
||||
weaken (Union n a) = Union (SS n) a
|
||||
weaken (Union pr a) = Union (There pr) a
|
||||
{-# INLINE weaken #-}
|
||||
|
||||
|
||||
@ -241,10 +292,22 @@ inj e = injWeaving $
|
||||
(Just . runIdentity)
|
||||
{-# INLINE inj #-}
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Lift an effect @e@ into a 'Union' capable of holding it,
|
||||
-- given an explicit proof that the effect exists in @r@
|
||||
injUsing :: forall e r m a. Functor m => ElemOf e r -> e m a -> Union r m a
|
||||
injUsing pr e = Union pr $
|
||||
Weaving e (Identity ())
|
||||
(fmap Identity . runIdentity)
|
||||
runIdentity
|
||||
(Just . runIdentity)
|
||||
{-# INLINE injUsing #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Lift a @'Weaving' e@ into a 'Union' capable of holding it.
|
||||
injWeaving :: forall e r m a. Member e r => Weaving e m a -> Union r m a
|
||||
injWeaving = Union (finder @_ @r @e)
|
||||
injWeaving = Union membership
|
||||
{-# INLINE injWeaving #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
@ -254,12 +317,19 @@ prj :: forall e r m a
|
||||
)
|
||||
=> Union r m a
|
||||
-> Maybe (Weaving e m a)
|
||||
prj (Union sn a) =
|
||||
case testEquality sn (finder @_ @r @e) of
|
||||
Nothing -> Nothing
|
||||
Just Refl -> Just a
|
||||
prj = prjUsing membership
|
||||
{-# INLINE prj #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Attempt to take an @e@ effect out of a 'Union', given an explicit
|
||||
-- proof that the effect exists in @r@.
|
||||
prjUsing
|
||||
:: forall e r m a
|
||||
. ElemOf e r
|
||||
-> Union r m a
|
||||
-> Maybe (Weaving e m a)
|
||||
prjUsing pr (Union sn a) = (\Refl -> a) <$> sameMember pr sn
|
||||
{-# INLINE prjUsing #-}
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Like 'decomp', but allows for a more efficient
|
||||
@ -269,6 +339,6 @@ decompCoerce
|
||||
-> Either (Union (f ': r) m a) (Weaving e m a)
|
||||
decompCoerce (Union p a) =
|
||||
case p of
|
||||
SZ -> Right a
|
||||
SS n -> Left (Union (SS n) a)
|
||||
Here -> Right a
|
||||
There pr -> Left (Union (There pr) a)
|
||||
{-# INLINE decompCoerce #-}
|
||||
|
||||
17
src/Polysemy/Membership.hs
Normal file
17
src/Polysemy/Membership.hs
Normal file
@ -0,0 +1,17 @@
|
||||
module Polysemy.Membership
|
||||
( -- * Witnesses
|
||||
ElemOf (..)
|
||||
, membership
|
||||
, sameMember
|
||||
-- * Checking membership
|
||||
, KnownRow
|
||||
, tryMembership
|
||||
-- * Using membership
|
||||
, subsumeUsing
|
||||
, interceptUsing
|
||||
, interceptUsingH
|
||||
) where
|
||||
|
||||
import Polysemy.Internal
|
||||
import Polysemy.Internal.Combinators
|
||||
import Polysemy.Internal.Union
|
||||
@ -80,7 +80,7 @@ untag
|
||||
-- Once GHC 8.10 rolls out, I will benchmark and compare.
|
||||
untag = hoistSem $ \u -> case decompCoerce u of
|
||||
Right (Weaving (Tagged e) s wv ex ins) ->
|
||||
Union SZ (Weaving e s (untag . wv) ex ins)
|
||||
Union Here (Weaving e s (untag . wv) ex ins)
|
||||
Left g -> hoist untag g
|
||||
{-# INLINE untag #-}
|
||||
|
||||
|
||||
35
test/KnownRowSpec.hs
Normal file
35
test/KnownRowSpec.hs
Normal file
@ -0,0 +1,35 @@
|
||||
module KnownRowSpec where
|
||||
|
||||
import Polysemy
|
||||
import Polysemy.Error
|
||||
import Polysemy.State
|
||||
import Polysemy.Internal
|
||||
import Polysemy.Internal.Union
|
||||
|
||||
import Test.Hspec
|
||||
|
||||
-- | A variant of 'runState' that uses 'stateToIO' if @r@ contains @Embed IO@.
|
||||
-- (Can also be extended to check for @Final IO@)
|
||||
runState' :: forall s r a. KnownRow r => s -> Sem (State s ': r) a -> Sem r (s, a)
|
||||
runState' s sem = case tryMembership @(Embed IO) of
|
||||
Just proof -> subsumeUsing proof (stateToIO s (raiseUnder sem))
|
||||
_ -> runState s sem
|
||||
|
||||
|
||||
test :: (Member (Error ()) r, KnownRow r)
|
||||
=> Sem r String
|
||||
test = fmap fst $ runState' "" $ do
|
||||
put "local state"
|
||||
_ <- (put "global state" >> throw ()) `catch` \() -> return ()
|
||||
return ()
|
||||
|
||||
spec :: Spec
|
||||
spec = parallel $ describe "tryMembership" $ do
|
||||
it "should return a valid proof when the targeted \
|
||||
\ effect is part of the row" $ do
|
||||
res <- runM . runError @() $ test
|
||||
res `shouldBe` Right "global state"
|
||||
it "should not return a valid proof when the targeted \
|
||||
\ effect is not part of the row" $ do
|
||||
let res = run . runError @() $ test
|
||||
res `shouldBe` Right "local state"
|
||||
Loading…
Reference in New Issue
Block a user