mirror of
https://github.com/polysemy-research/polysemy.git
synced 2024-09-17 13:37:21 +03:00
reinterpret3 and hide Member
This commit is contained in:
parent
9044832884
commit
1d9e35d122
@ -17,11 +17,13 @@ module Polysemy
|
||||
, intercept
|
||||
, reinterpret
|
||||
, reinterpret2
|
||||
, reinterpret3
|
||||
-- * Higher order
|
||||
, interpretH
|
||||
, interceptH
|
||||
, reinterpretH
|
||||
, reinterpret2H
|
||||
, reinterpret3H
|
||||
-- * Statefulness
|
||||
, stateful
|
||||
, lazilyStateful
|
||||
|
@ -7,11 +7,13 @@ module Polysemy.Internal.Combinators
|
||||
, intercept
|
||||
, reinterpret
|
||||
, reinterpret2
|
||||
, reinterpret3
|
||||
-- * Higher order
|
||||
, interpretH
|
||||
, interceptH
|
||||
, reinterpretH
|
||||
, reinterpret2H
|
||||
, reinterpret3H
|
||||
-- * Statefulness
|
||||
, stateful
|
||||
, lazilyStateful
|
||||
@ -167,6 +169,26 @@ reinterpret2
|
||||
reinterpret2 f = reinterpret2H $ \(e :: e m x) -> liftT @m $ f e
|
||||
{-# INLINE[3] reinterpret2 #-}
|
||||
|
||||
reinterpret3H
|
||||
:: (∀ m x. e1 m x -> Tactical e1 m (e2 ': e3 ': e4 ': r) x)
|
||||
-> Semantic (e1 ': r) a
|
||||
-> Semantic (e2 ': e3 ': e4 ': r) a
|
||||
reinterpret3H f (Semantic m) = Semantic $ \k -> m $ \u ->
|
||||
case decompCoerce u of
|
||||
Left x -> k . weaken . weaken . hoist (reinterpret3H_b f) $ x
|
||||
Right (Yo e s d y) -> do
|
||||
a <- usingSemantic k $ runTactics s (raise . reinterpret3H_b f . d) $ f e
|
||||
pure $ y a
|
||||
{-# INLINE[3] reinterpret3H #-}
|
||||
|
||||
reinterpret3
|
||||
:: FirstOrder e1 "reinterpret2"
|
||||
=> (∀ m x. e1 m x -> Semantic (e2 ': e3 ': e4 ': r) x)
|
||||
-> Semantic (e1 ': r) a
|
||||
-> Semantic (e2 ': e3 ': e4 ': r) a
|
||||
reinterpret3 f = reinterpret3H $ \(e :: e m x) -> liftT @m $ f e
|
||||
{-# INLINE[3] reinterpret3 #-}
|
||||
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | Like 'interpret', but instead of handling the effect, allows responding to
|
||||
@ -235,3 +257,10 @@ reinterpret2H_b
|
||||
reinterpret2H_b = reinterpret2H
|
||||
{-# NOINLINE reinterpret2H_b #-}
|
||||
|
||||
reinterpret3H_b
|
||||
:: (∀ m x. e1 m x -> Tactical e1 m (e2 ': e3 ': e4 ': r) x)
|
||||
-> Semantic (e1 ': r) a
|
||||
-> Semantic (e2 ': e3 ': e4 ': r) a
|
||||
reinterpret3H_b = reinterpret3H
|
||||
{-# NOINLINE reinterpret3H_b #-}
|
||||
|
||||
|
@ -1,12 +1,13 @@
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE QuantifiedConstraints #-}
|
||||
{-# LANGUAGE StrictData #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE QuantifiedConstraints #-}
|
||||
{-# LANGUAGE StrictData #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
{-# LANGUAGE UndecidableSuperClasses #-}
|
||||
|
||||
module Polysemy.Internal.Union
|
||||
( Union (..)
|
||||
@ -93,16 +94,28 @@ instance Effect (Union r) where
|
||||
{-# INLINE hoist #-}
|
||||
|
||||
|
||||
|
||||
-- TODO(sandy): This type error gets in the way of real type errors, eg if you
|
||||
-- put a $ in the wrong place
|
||||
type Member e r =
|
||||
------------------------------------------------------------------------------
|
||||
-- | Hide the actual implementation of 'Member' from the haddock.
|
||||
class
|
||||
( Find r e
|
||||
, e ~ IndexOf r (Found r e)
|
||||
#ifdef ERROR_MESSAGES
|
||||
, Break (AmbiguousSend r e) (IndexOf r (Found r e))
|
||||
#endif
|
||||
)
|
||||
) => Member' e r
|
||||
|
||||
instance
|
||||
( Find r e
|
||||
, e ~ IndexOf r (Found r e)
|
||||
#ifdef ERROR_MESSAGES
|
||||
, Break (AmbiguousSend r e) (IndexOf r (Found r e))
|
||||
#endif
|
||||
) => Member' e r
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
-- | A @Member e r@ constraint is a proof that the effect @e@ is available in
|
||||
-- the list of effects @r@.
|
||||
type Member = Member'
|
||||
|
||||
|
||||
data Dict c where Dict :: c => Dict c
|
||||
|
Loading…
Reference in New Issue
Block a user