Add insertAt

A combinator that allows adding effects at a specified index into the
effect stack

ChangeLog.md

@@ -4,6 +4,7 @@
 
 * Deprecate `traceToIO` and replace it with `traceToStdout` and `traceToStderr`
 * Support GHC 9.0.1
+* Added the combinator `insertAt`, which allows adding effects at a specified index into the effect stack
 
 ## 1.5.0.0 (2021-03-30)
 

polysemy-plugin/polysemy-plugin.cabal

@@ -80,6 +80,7 @@ test-suite polysemy-plugin-test
       BadSpec
       DoctestSpec
       ExampleSpec
+      InsertSpec
       LegitimateTypeErrorSpec
       MultipleVarsSpec
       PluginSpec

polysemy-plugin/test/InsertSpec.hs

@@ -0,0 +1,22 @@
+module InsertSpec where
+
+import Polysemy.State (State)
+import Polysemy.Reader (Reader)
+import Polysemy.Internal (insertAt)
+import Polysemy
+import Test.Hspec
+
+insertAtWithIndex :: Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e1 : e2 : Reader i : e3 : e4 : r) a
+insertAtWithIndex = insertAt @2
+
+insertAtAndRaiseUnder :: Sem (e1 : r) a -> Sem (e1 : e2 : State s : e3 : Reader i : e4 : r) a
+insertAtAndRaiseUnder = raise2Under . insertAt @2 . raiseUnder
+
+insertAtEmpty :: Sem (e1 : e2 : r) a -> Sem (e1 : e2 : r) a
+insertAtEmpty = insertAt @2
+
+spec :: Spec
+spec = parallel $ do
+  describe "insert" $ do
+    it "insert" $ do
+      1 `shouldBe` 1

polysemy-plugin/test/TypeErrors.hs

@@ -9,6 +9,7 @@ module TypeErrors where
 -- >>> :set -fplugin=Polysemy.Plugin
 -- >>> :m +Polysemy
 -- >>> :m +Polysemy.State
+-- >>> :m +Polysemy.Reader
 -- >>> :m +Data.Maybe
 
 
@@ -26,3 +27,50 @@ module TypeErrors where
 -- ...
 missingFmap = ()
 
+--------------------------------------------------------------------------------
+-- |
+-- >>> :{
+-- insertSome :: ∀ e1 e2 s r a . Sem (e1 ': e2 ': r) a -> Sem (e1 ': e2 ': State s ': r) a
+-- insertSome = insertAt
+-- :}
+-- ...
+-- ... insertAt: You must provide the index ...
+-- ...
+insertAtUnprovidedIndex = ()
+
+--------------------------------------------------------------------------------
+-- |
+-- >>> :{
+-- insertSome :: Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e1 : e2 : Reader i : e3 : e4 : r) a
+-- insertSome = insertAt @1
+-- :}
+-- ...
+-- ...insertAt: Failed to insert effects at index 1
+-- ...
+-- ... before ...
+-- ...'[e1]
+-- ... after ...
+-- ...e2 : e3 : e4 : r
+-- ...Actual ...
+-- ...e1 : e2 : Reader i : e3 : e4 : r
+-- ...
+insertAtWrongIndex = ()
+
+--------------------------------------------------------------------------------
+-- |
+-- Note: The /Actual/ row doesn't match the return type because of the 'raiseUnder'.
+-- >>> :{
+-- insertSome :: Sem (e1 : r) a -> Sem (e1 : e2 : State s : e3 : Reader i : e4 : r) a
+-- insertSome = raiseUnder . insertAt @2 . raise2Under
+-- :}
+-- ...
+-- ...insertAt: Failed to insert effects at index 2
+-- ...
+-- ... before ...
+-- ...'[e1, State s]
+-- ... after ...
+-- ...e30 : r0
+-- ...Actual ...
+-- ...e1 : State s : e3 : Reader i : e4 : r
+-- ...
+insertAtAndRaiseWrongIndex = ()

polysemy.cabal

@@ -62,8 +62,10 @@ library
       Polysemy.Internal.CustomErrors.Redefined
       Polysemy.Internal.Fixpoint
       Polysemy.Internal.Forklift
+      Polysemy.Internal.Index
       Polysemy.Internal.Kind
       Polysemy.Internal.NonDet
+      Polysemy.Internal.Sing
       Polysemy.Internal.Strategy
       Polysemy.Internal.Tactics
       Polysemy.Internal.TH.Common

src/Polysemy.hs

@@ -35,6 +35,7 @@ module Polysemy
   , raise3Under
   , raise_
   , subsume_
+  , insertAt
 
     -- * Trivial Interpretation
   , subsume

src/Polysemy/Bundle.hs

@@ -9,13 +9,13 @@ module Polysemy.Bundle
   , runBundle
   , subsumeBundle
     -- * Miscellaneous
-  , KnownList
   ) where
 
 import Polysemy
 import Polysemy.Internal
-import Polysemy.Internal.Bundle
 import Polysemy.Internal.Union
+import Polysemy.Internal.Bundle (subsumeMembership)
+import Polysemy.Internal.Sing (KnownList (singList))
 
 ------------------------------------------------------------------------------
 -- | An effect for collecting multiple effects into one effect.
@@ -58,8 +58,8 @@ runBundle
   -> 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
+    Union (extendMembershipRight @r' @r pr) $ Weaving e s wv ex ins
+  Left g -> weakenList @r' @r (singList @r') g
 {-# INLINE runBundle #-}
 
 ------------------------------------------------------------------------------

src/Polysemy/Internal.hs

@@ -30,6 +30,7 @@ module Polysemy.Internal
   , Subsume (..)
   , subsume
   , subsumeUsing
+  , insertAt
   , Embed (..)
   , usingSem
   , liftSem
@@ -44,6 +45,8 @@ module Polysemy.Internal
 import Control.Applicative
 import Control.Monad
 #if __GLASGOW_HASKELL__ < 808
+
+
 import Control.Monad.Fail
 #endif
 import Control.Monad.Fix
@@ -53,10 +56,13 @@ import Data.Kind
 import Polysemy.Embed.Type
 import Polysemy.Fail.Type
 import Polysemy.Internal.Fixpoint
+import Polysemy.Internal.Index (InsertAtUnprovidedIndex, InsertAtIndex(insertAtIndex))
 import Polysemy.Internal.Kind
 import Polysemy.Internal.NonDet
 import Polysemy.Internal.PluginLookup
 import Polysemy.Internal.Union
+import Type.Errors (WhenStuck)
+import Polysemy.Internal.Sing (ListOfLength (listOfLength))
 
 
 -- $setup
@@ -540,6 +546,32 @@ subsumeUsing pr =
     go
 {-# INLINE subsumeUsing #-}
 
+------------------------------------------------------------------------------
+-- | Introduce a set of effects into 'Sem' at the index @i@, before the effect
+-- that previously occupied that position. This is intended to be used with a
+-- type application:
+--
+-- @
+-- let
+--   sem1 :: Sem [e1, e2, e3, e4, e5] a
+--   sem1 = insertAt @2 (sem0 :: Sem [e1, e2, e5] a)
+-- @
+--
+-- @since 1.6.0.0
+insertAt
+  :: forall index inserted head oldTail tail old full a
+   . ( ListOfLength index head
+     , WhenStuck index InsertAtUnprovidedIndex
+     , old ~ Append head oldTail
+     , tail ~ Append inserted oldTail
+     , full ~ Append head tail
+     , InsertAtIndex index head tail oldTail full inserted)
+  => Sem old a
+  -> Sem full a
+insertAt = hoistSem $ \u -> hoist (insertAt @index @inserted @head @oldTail) $
+  weakenMid @oldTail (listOfLength @index @head) (insertAtIndex @Effect @index @head @tail @oldTail @full @inserted) u
+{-# INLINE insertAt #-}
+
 
 ------------------------------------------------------------------------------
 -- | Embed an effect into a 'Sem'. This is used primarily via
@@ -588,11 +620,6 @@ runM (Sem m) = m $ \z ->
 {-# INLINE runM #-}
 
 
-type family Append l r where
-  Append (a ': l) r = a ': (Append l r)
-  Append '[] r = r
-
-
 ------------------------------------------------------------------------------
 -- | Type synonym for interpreters that consume an effect without changing the
 -- return value. Offered for user convenience.

src/Polysemy/Internal/Bundle.hs

@@ -2,15 +2,11 @@
 
 {-# OPTIONS_HADDOCK not-home #-}
 
-module Polysemy.Internal.Bundle (
-  module Polysemy.Internal.Bundle,
-  Append,
-) where
+module Polysemy.Internal.Bundle where
 
-import Data.Proxy
-import Polysemy
-import Polysemy.Internal (Append)
-import Polysemy.Internal.Union
+import Polysemy (Members)
+import Polysemy.Internal.Union (ElemOf(..), membership)
+import Polysemy.Internal.Kind (Append)
 
 extendMembership :: forall r r' e. ElemOf e r -> ElemOf e (Append r r')
 extendMembership Here = Here
@@ -21,35 +17,3 @@ 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 #-}
-

src/Polysemy/Internal/Index.hs

@@ -0,0 +1,55 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+{-# OPTIONS_HADDOCK not-home #-}
+
+module Polysemy.Internal.Index where
+
+import GHC.TypeLits (Nat)
+import Type.Errors (TypeError, ErrorMessage(ShowType))
+import Type.Errors.Pretty (type (<>), type (%))
+
+import Polysemy.Internal.Sing (SList (SEnd, SCons))
+
+------------------------------------------------------------------------------
+-- | Infer a partition of the result type @full@ so that for the fixed segments
+-- @head@ and @tail@, the new segment @inserted@ contains the missing effects
+-- between them.
+class InsertAtIndex (index :: Nat) (head :: [k]) (tail :: [k]) (oldTail :: [k]) (full :: [k]) (inserted :: [k]) where
+  insertAtIndex :: SList inserted
+
+instance inserted ~ '[] => InsertAtIndex index head oldTail oldTail full inserted where
+  insertAtIndex = SEnd
+  {-# INLINE insertAtIndex #-}
+
+instance {-# INCOHERENT #-} (
+    InsertAtIndex index head tail oldTail full insertedTail,
+    inserted ~ (e ': insertedTail)
+  ) => InsertAtIndex index head (e ': tail) oldTail full inserted where
+    insertAtIndex = SCons (insertAtIndex @_ @index @head @tail @oldTail @full)
+    {-# INLINE insertAtIndex #-}
+
+instance {-# INCOHERENT #-} TypeError (InsertAtFailure index oldTail head full)
+       => InsertAtIndex index head tail oldTail full inserted where
+  insertAtIndex = error "unreachable"
+
+type family InsertAtUnprovidedIndex where
+  InsertAtUnprovidedIndex = TypeError (
+    "insertAt: You must provide the index at which the effects should be inserted as a type application."
+    % "Example: insertAt @5"
+    )
+
+type InsertAtFailure index soughtTail head full =
+  "insertAt: Failed to insert effects at index " <> 'ShowType index
+  % "There is a mismatch between what's been determined as the head and tail between the newly inserted effects,"
+  <> " and the actual desired return type."
+  % "Determined head before inserted effects:"
+  % "\t" <> 'ShowType head
+  % "Determined tail after the inserted effects:"
+  % "\t" <> 'ShowType soughtTail
+  % "Actual desired return type:"
+  % "\t" <> 'ShowType full
+  % "Make sure that the index provided to insertAt is correct, and that the desired return type simply requires"
+  <> " inserting effects."

src/Polysemy/Internal/Kind.hs

@@ -1,6 +1,8 @@
+{-# OPTIONS_HADDOCK not-home #-}
+
 module Polysemy.Internal.Kind where
 
-import Data.Kind
+import Data.Kind (Type)
 
 ------------------------------------------------------------------------------
 -- | The kind of effects.
@@ -14,3 +16,7 @@ type Effect    = (Type -> Type) -> Type -> Type
 -- @since 0.5.0.0
 type EffectRow = [Effect]
 
+
+type family Append l r where
+  Append (a ': l) r = a ': (Append l r)
+  Append '[] r = r

src/Polysemy/Internal/Sing.hs

@@ -0,0 +1,37 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+{-# OPTIONS_HADDOCK not-home #-}
+
+module Polysemy.Internal.Sing where
+
+import GHC.TypeLits (type (-), Nat)
+import Polysemy.Internal.Kind (Effect)
+
+data SList l where
+  SEnd  :: SList '[]
+  SCons :: SList xs -> SList (x ': xs)
+
+class KnownList l where
+  singList :: SList l
+
+instance KnownList '[] where
+  singList = SEnd
+  {-# INLINE singList #-}
+
+instance KnownList xs => KnownList (x ': xs) where
+  singList = SCons singList
+  {-# INLINE singList #-}
+
+class ListOfLength (n :: Nat) (l :: [Effect]) where
+  listOfLength :: SList l
+
+instance {-# OVERLAPPING #-} (l ~ '[]) => ListOfLength 0 l where
+  listOfLength = SEnd
+  {-# INLINE listOfLength #-}
+
+instance (ListOfLength (n - 1) xs, l ~ (x ': xs)) => ListOfLength n l where
+  listOfLength = SCons (listOfLength @(n - 1))
+  {-# INLINE listOfLength #-}

src/Polysemy/Internal/Union.hs

@@ -39,7 +39,11 @@ module Polysemy.Internal.Union
   -- * Checking membership
   , KnownRow
   , tryMembership
-  ) where
+  , extendMembershipLeft
+  , extendMembershipRight
+  , injectMembership
+  , weakenList
+  , weakenMid) where
 
 import Control.Monad
 import Data.Functor.Compose
@@ -48,6 +52,7 @@ import Data.Kind
 import Data.Typeable
 import Polysemy.Internal.Kind
 import {-# SOURCE #-} Polysemy.Internal
+import Polysemy.Internal.Sing (SList (SEnd, SCons))
 
 #ifndef NO_ERROR_MESSAGES
 import Polysemy.Internal.CustomErrors
@@ -251,6 +256,41 @@ tryMembership :: forall e r. (Typeable e, KnownRow r) => Maybe (ElemOf e r)
 tryMembership = tryMembership' @r @e
 {-# INLINE tryMembership #-}
 
+
+------------------------------------------------------------------------------
+-- | Extends a proof that @e@ is an element of @r@ to a proof that @e@ is an
+-- element of the concatenation of the lists @l@ and @r@.
+-- @l@ must be specified as a singleton list proof.
+extendMembershipLeft :: forall l r e. SList l -> ElemOf e r -> ElemOf e (Append l r)
+extendMembershipLeft SEnd pr = pr
+extendMembershipLeft (SCons l) pr = There (extendMembershipLeft l pr)
+{-# INLINE extendMembershipLeft #-}
+
+
+------------------------------------------------------------------------------
+-- | Extends a proof that @e@ is an element of @l@ to a proof that @e@ is an
+-- element of the concatenation of the lists @l@ and @r@.
+extendMembershipRight :: forall l r e. ElemOf e l -> ElemOf e (Append l r)
+extendMembershipRight Here = Here
+extendMembershipRight (There e) = There (extendMembershipRight @_ @r e)
+{-# INLINE extendMembershipRight #-}
+
+
+------------------------------------------------------------------------------
+-- | Extends a proof that @e@ is an element of @left <> right@ to a proof that
+-- @e@ is an element of @left <> mid <> right@.
+-- Both @left@ and @right@ must be specified as singleton list proofs.
+injectMembership :: forall right e left mid
+                  . SList left
+                 -> SList mid
+                 -> ElemOf e (Append left right)
+                 -> ElemOf e (Append left (Append mid right))
+injectMembership SEnd sm pr = extendMembershipLeft sm pr
+injectMembership (SCons _) _ Here = Here
+injectMembership (SCons sl) sm (There pr) = There (injectMembership @right sl sm pr)
+{-# INLINE injectMembership #-}
+
+
 ------------------------------------------------------------------------------
 -- | Decompose a 'Union'. Either this union contains an effect @e@---the head
 -- of the @r@ list---or it doesn't.
@@ -282,12 +322,32 @@ absurdU = \case {}
 
 
 ------------------------------------------------------------------------------
--- | Weaken a 'Union' so it is capable of storing a new sort of effect.
+-- | Weaken a 'Union' so it is capable of storing a new sort of effect at the
+-- head.
 weaken :: forall e r m a. Union r m a -> Union (e ': r) m a
 weaken (Union pr a) = Union (There pr) a
 {-# INLINE weaken #-}
 
 
+------------------------------------------------------------------------------
+-- | Weaken a 'Union' so it is capable of storing a number of new effects at
+-- the head, specified as a singleton list proof.
+weakenList :: SList l -> Union r m a -> Union (Append l r) m a
+weakenList sl (Union pr e) = Union (extendMembershipLeft sl pr) e
+{-# INLINE weakenList #-}
+
+
+------------------------------------------------------------------------------
+-- | Weaken a 'Union' so it is capable of storing a number of new effects
+-- somewhere within the previous effect list.
+-- Both the prefix and the new effects are specified as singleton list proofs.
+weakenMid :: forall right m a left mid
+           . SList left -> SList mid
+          -> Union (Append left right) m a
+          -> Union (Append left (Append mid right)) m a
+weakenMid sl sm (Union pr e) = Union (injectMembership @right sl sm pr) e
+{-# INLINE weakenMid #-}
+
 
 ------------------------------------------------------------------------------
 -- | Lift an effect @e@ into a 'Union' capable of holding it.