{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Control.Monad.Dep.Advice
(
Advice,
makeAdvice,
makeArgsAdvice,
makeExecutionAdvice,
advise,
Ensure,
Top2,
And2,
MonadConstraint,
EnvConstraint,
MustBe,
MustBe2,
restrictArgs,
restrictEnv,
restrictResult,
runFinalDepT,
runFromEnv,
Top,
And,
All,
NP (..),
I (..),
cfoldMap_NP,
type (:-) (..),
Dict (..),
)
where
import Control.Monad.Dep
import Data.Constraint
import Data.Kind
import Data.SOP
import Data.SOP.Dict qualified as SOP
import Data.SOP.NP
type Advice ::
(Type -> Constraint) ->
(((Type -> Type) -> Type) -> (Type -> Type) -> Constraint) ->
(Type -> Constraint) ->
Type
data Advice ca cem cr where
Advice ::
forall u ca cem cr.
Proxy u ->
( forall as e m.
(All ca as, cem e m, Monad m) =>
NP I as ->
DepT e m (u, NP I as)
) ->
( forall e m r.
(cem e m, Monad m, cr r) =>
u ->
DepT e m r ->
DepT e m r
) ->
Advice ca cem cr
instance Semigroup (Advice ca cem cr) where
Advice Proxy u
outer forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgsOuter forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecutionOuter <> :: Advice ca cem cr -> Advice ca cem cr -> Advice ca cem cr
<> Advice Proxy u
inner forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgsInner forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecutionInner =
let captureExistentials ::
forall ca cem cr outer inner.
Proxy outer ->
( forall as e m.
(All ca as, cem e m, Monad m) =>
NP I as ->
DepT e m (outer, NP I as)
) ->
( forall e m r.
(cem e m, Monad m, cr r) =>
outer ->
DepT e m r ->
DepT e m r
) ->
Proxy inner ->
( forall as e m.
(All ca as, cem e m, Monad m) =>
NP I as ->
DepT e m (inner, NP I as)
) ->
( forall e m r.
(cem e m, Monad m, cr r) =>
inner ->
DepT e m r ->
DepT e m r
) ->
Advice ca cem cr
captureExistentials :: Proxy outer
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (outer, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
outer -> DepT e m r -> DepT e m r)
-> Proxy inner
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (inner, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
inner -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
captureExistentials Proxy outer
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (outer, NP I as)
tweakArgsOuter' forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
outer -> DepT e m r -> DepT e m r
tweakExecutionOuter' Proxy inner
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (inner, NP I as)
tweakArgsInner' forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
inner -> DepT e m r -> DepT e m r
tweakExecutionInner' =
Proxy (Pair outer inner)
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (Pair outer inner, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
Pair outer inner -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall u (ca :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice
(Proxy (Pair outer inner)
forall k (t :: k). Proxy t
Proxy @(Pair outer inner))
( let tweakArgs ::
forall as e m.
(All ca as, cem e m, Monad m) =>
NP I as ->
DepT e m (Pair outer inner, NP I as)
tweakArgs :: NP I as -> DepT e m (Pair outer inner, NP I as)
tweakArgs NP I as
args =
do
(outer
uOuter, NP I as
argsOuter) <- NP I as -> DepT e m (outer, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (outer, NP I as)
tweakArgsOuter' @as @e @m NP I as
args
(inner
uInner, NP I as
argsInner) <- NP I as -> DepT e m (inner, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (inner, NP I as)
tweakArgsInner' @as @e @m NP I as
argsOuter
(Pair outer inner, NP I as) -> DepT e m (Pair outer inner, NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (outer -> inner -> Pair outer inner
forall a b. a -> b -> Pair a b
Pair outer
uOuter inner
uInner, NP I as
argsInner)
in NP I as -> DepT e m (Pair outer inner, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (Pair outer inner, NP I as)
tweakArgs
)
( let tweakExecution ::
forall e m r.
(cem e m, Monad m, cr r) =>
Pair outer inner ->
DepT e m r ->
DepT e m r
tweakExecution :: Pair outer inner -> DepT e m r -> DepT e m r
tweakExecution =
( \(Pair outer
uOuter inner
uInner) DepT e m r
action ->
outer -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
outer -> DepT e m r -> DepT e m r
tweakExecutionOuter' @e @m @r outer
uOuter (inner -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
inner -> DepT e m r -> DepT e m r
tweakExecutionInner' @e @m @r inner
uInner DepT e m r
action)
)
in Pair outer inner -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
Pair outer inner -> DepT e m r -> DepT e m r
tweakExecution
)
in Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall (ca :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint) outer inner.
Proxy outer
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (outer, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
outer -> DepT e m r -> DepT e m r)
-> Proxy inner
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (inner, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
inner -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
captureExistentials @ca @cem @cr Proxy u
outer forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgsOuter forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecutionOuter Proxy u
inner forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgsInner forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecutionInner
instance Monoid (Advice ca cem cr) where
mappend :: Advice ca cem cr -> Advice ca cem cr -> Advice ca cem cr
mappend = Advice ca cem cr -> Advice ca cem cr -> Advice ca cem cr
forall a. Semigroup a => a -> a -> a
(<>)
mempty :: Advice ca cem cr
mempty = Proxy ()
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m ((), NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
() -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall u (ca :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice (Proxy ()
forall k (t :: k). Proxy t
Proxy @()) (\NP I as
args -> ((), NP I as) -> DepT e m ((), NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NP I as -> ((), NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure NP I as
args)) ((DepT e m r -> DepT e m r) -> () -> DepT e m r -> DepT e m r
forall a b. a -> b -> a
const DepT e m r -> DepT e m r
forall a. a -> a
id)
makeAdvice ::
forall u ca cem cr.
( forall as e m.
(All ca as, cem e m, Monad m) =>
NP I as ->
DepT e m (u, NP I as)
) ->
( forall e m r.
(cem e m, Monad m, cr r) =>
u ->
DepT e m r ->
DepT e m r
) ->
Advice ca cem cr
makeAdvice :: (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
makeAdvice = Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall u (ca :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice (Proxy u
forall k (t :: k). Proxy t
Proxy @u)
makeArgsAdvice ::
forall ca cem cr.
( forall as e m.
(All ca as, cem e m, Monad m) =>
NP I as ->
DepT e m (NP I as)
) ->
Advice ca cem cr
makeArgsAdvice :: (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (NP I as))
-> Advice ca cem cr
makeArgsAdvice forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (NP I as)
tweakArgs =
(forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m ((), NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
() -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall u (ca :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint).
(forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
makeAdvice @()
( \NP I as
args -> do
NP I as
args <- NP I as -> DepT e m (NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (NP I as)
tweakArgs NP I as
args
((), NP I as) -> DepT e m ((), NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((), NP I as
args)
)
((DepT e m r -> DepT e m r) -> () -> DepT e m r -> DepT e m r
forall a b. a -> b -> a
const DepT e m r -> DepT e m r
forall a. a -> a
id)
makeExecutionAdvice ::
forall ca cem cr.
( forall e m r.
(cem e m, Monad m, cr r) =>
DepT e m r ->
DepT e m r
) ->
Advice ca cem cr
makeExecutionAdvice :: (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
DepT e m r -> DepT e m r)
-> Advice ca cem cr
makeExecutionAdvice forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
DepT e m r -> DepT e m r
tweakExecution = (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m ((), NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
() -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall u (ca :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint).
(forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
makeAdvice @() (\NP I as
args -> ((), NP I as) -> DepT e m ((), NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NP I as -> ((), NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure NP I as
args)) (\() DepT e m r
action -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
DepT e m r -> DepT e m r
tweakExecution DepT e m r
action)
data Pair a b = Pair !a !b
type Ensure :: (Type -> (Type -> Type) -> Constraint) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
class c (e (DepT e m)) (DepT e m) => Ensure c e m
instance c (e (DepT e m)) (DepT e m) => Ensure c e m
advise ::
forall ca cem cr as e m r advisee.
(Multicurryable as e m r advisee, All ca as, cem e m, Monad m, cr r) =>
Advice ca cem cr ->
advisee ->
advisee
advise :: Advice ca cem cr -> advisee -> advisee
advise (Advice Proxy u
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution) advisee
advisee = do
let uncurried :: NP I as -> DepT e m r
uncurried = advisee -> NP I as -> DepT e m r
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
curried -> NP I as -> DepT e m r
multiuncurry @as @e @m @r advisee
advisee
uncurried' :: NP I as -> DepT e m r
uncurried' NP I as
args = do
(u
u, NP I as
args') <- NP I as -> DepT e m (u, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs NP I as
args
u -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution u
u (NP I as -> DepT e m r
uncurried NP I as
args')
in (NP I as -> DepT e m r) -> advisee
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
(NP I as -> DepT e m r) -> curried
multicurry @as @e @m @r NP I as -> DepT e m r
uncurried'
type Multicurryable ::
[Type] ->
((Type -> Type) -> Type) ->
(Type -> Type) ->
Type ->
Type ->
Constraint
class Multicurryable as e m r curried | curried -> as e m r where
type BaseMonadAtTheTip as e m r curried :: Type
multiuncurry :: curried -> NP I as -> DepT e m r
multicurry :: (NP I as -> DepT e m r) -> curried
_runFromEnv :: m (e (DepT e m)) -> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
instance Monad m => Multicurryable '[] e m r (DepT e m r) where
type BaseMonadAtTheTip '[] e m r (DepT e m r) = m r
multiuncurry :: DepT e m r -> NP I '[] -> DepT e m r
multiuncurry DepT e m r
action NP I '[]
Nil = DepT e m r
action
multicurry :: (NP I '[] -> DepT e m r) -> DepT e m r
multicurry NP I '[] -> DepT e m r
f = NP I '[] -> DepT e m r
f NP I '[]
forall k (a :: k -> *). NP a '[]
Nil
_runFromEnv :: m (e (DepT e m))
-> (e (DepT e m) -> DepT e m r)
-> BaseMonadAtTheTip '[] e m r (DepT e m r)
_runFromEnv m (e (DepT e m))
producer e (DepT e m) -> DepT e m r
extractor = do
e (DepT e m)
e <- m (e (DepT e m))
producer
DepT e m r -> e (DepT e m) -> m r
forall (env :: (* -> *) -> *) (m :: * -> *) r.
DepT env m r -> env (DepT env m) -> m r
runDepT (e (DepT e m) -> DepT e m r
extractor e (DepT e m)
e) e (DepT e m)
e
instance Multicurryable as e m r curried => Multicurryable (a ': as) e m r (a -> curried) where
type BaseMonadAtTheTip (a ': as) e m r (a -> curried) = a -> BaseMonadAtTheTip as e m r curried
multiuncurry :: (a -> curried) -> NP I (a : as) -> DepT e m r
multiuncurry a -> curried
f (I x
a :* NP I xs
as) = curried -> NP I as -> DepT e m r
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
curried -> NP I as -> DepT e m r
multiuncurry @as @e @m @r @curried (a -> curried
f a
x
a) NP I as
NP I xs
as
multicurry :: (NP I (a : as) -> DepT e m r) -> a -> curried
multicurry NP I (a : as) -> DepT e m r
f a
a = (NP I as -> DepT e m r) -> curried
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
(NP I as -> DepT e m r) -> curried
multicurry @as @e @m @r @curried (NP I (a : as) -> DepT e m r
f (NP I (a : as) -> DepT e m r)
-> (NP I as -> NP I (a : as)) -> NP I as -> DepT e m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I a -> NP I as -> NP I (a : as)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
(:*) (a -> I a
forall a. a -> I a
I a
a))
_runFromEnv :: m (e (DepT e m))
-> (e (DepT e m) -> a -> curried)
-> BaseMonadAtTheTip (a : as) e m r (a -> curried)
_runFromEnv m (e (DepT e m))
producer e (DepT e m) -> a -> curried
extractor a
a = m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
_runFromEnv @as @e @m @r @curried m (e (DepT e m))
producer (\e (DepT e m)
f -> e (DepT e m) -> a -> curried
extractor e (DepT e m)
f a
a)
runFinalDepT ::
forall as e m r curried.
Multicurryable as e m r curried =>
m (e (DepT e m)) ->
curried ->
BaseMonadAtTheTip as e m r curried
runFinalDepT :: m (e (DepT e m)) -> curried -> BaseMonadAtTheTip as e m r curried
runFinalDepT m (e (DepT e m))
producer curried
extractor = m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
_runFromEnv m (e (DepT e m))
producer (curried -> e (DepT e m) -> curried
forall a b. a -> b -> a
const curried
extractor)
runFromEnv ::
forall as e m r curried.
(Multicurryable as e m r curried, Monad m) =>
m (e (DepT e m)) ->
(e (DepT e m) -> curried) ->
BaseMonadAtTheTip as e m r curried
runFromEnv :: m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
runFromEnv = m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
_runFromEnv
type Top2 :: ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
class Top2 e m
instance Top2 e m
type And2 ::
(((Type -> Type) -> Type) -> (Type -> Type) -> Constraint) ->
(((Type -> Type) -> Type) -> (Type -> Type) -> Constraint) ->
(((Type -> Type) -> Type) -> (Type -> Type) -> Constraint)
class (f e m, g e m) => (f `And2` g) e m
instance (f e m, g e m) => (f `And2` g) e m
infixl 7 `And2`
type MustBe :: forall k. k -> k -> Constraint
class x ~ y => MustBe x y
instance x ~ y => MustBe x y
type MustBe2 :: ((Type -> Type) -> Type) -> (Type -> Type) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
class (e' ~ e, m' ~ m) => MustBe2 e' m' e m
instance (e' ~ e, m' ~ m) => MustBe2 e' m' e m
type EnvConstraint :: (((Type -> Type) -> Type) -> Constraint) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
class c e => EnvConstraint c e m
instance c e => EnvConstraint c e m
type MonadConstraint :: ((Type -> Type) -> Constraint) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
class c m => MonadConstraint c e m
instance c m => MonadConstraint c e m
restrictArgs ::
forall more less cem cr.
(forall r. more r :- less r) ->
Advice less cem cr ->
Advice more cem cr
restrictArgs :: (forall r. more r :- less r)
-> Advice less cem cr -> Advice more cem cr
restrictArgs forall r. more r :- less r
evidence (Advice Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution) =
let captureExistential ::
forall more less cem cr u.
(forall r. more r :- less r) ->
Proxy u ->
( forall as e m.
(All less as, cem e m, Monad m) =>
NP I as ->
DepT e m (u, NP I as)
) ->
( forall e m r.
(cem e m, Monad m, cr r) =>
u ->
DepT e m r ->
DepT e m r
) ->
Advice more cem cr
captureExistential :: (forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice more cem cr
captureExistential forall r. more r :- less r
evidence' Proxy u
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs' forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution' =
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All more as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice more cem cr
forall u (ca :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice
(Proxy u
forall k (t :: k). Proxy t
Proxy @u)
( let tweakArgs'' :: forall as e m. (All more as, cem e m, Monad m) => NP I as -> DepT e m (u, NP I as)
tweakArgs'' :: NP I as -> DepT e m (u, NP I as)
tweakArgs'' = case (forall a. Dict more a -> Dict less a)
-> Dict (All more) as -> Dict (All less) as
forall k (c :: k -> Constraint) (d :: k -> Constraint) (xs :: [k]).
(forall (a :: k). Dict c a -> Dict d a)
-> Dict (All c) xs -> Dict (All d) xs
SOP.mapAll @more @less ((forall r. more r :- less r) -> Dict more a -> Dict less a
forall k (more :: k -> Constraint) (less :: k -> Constraint)
(a :: k).
(forall (x :: k). more x :- less x) -> Dict more a -> Dict less a
translateEvidence @more @less forall r. more r :- less r
evidence') of
Dict (All more) as -> Dict (All less) as
f -> case Dict (All more) as -> Dict (All less) as
f (All more as => Dict (All more) as
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
SOP.Dict @(All more) @as) of
Dict (All less) as
SOP.Dict -> \NP I as
args -> NP I as -> DepT e m (u, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs' @as @e @m NP I as
args
in NP I as -> DepT e m (u, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All more as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs''
)
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution'
in (forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice more cem cr
forall (more :: * -> Constraint) (less :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint) u.
(forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice more cem cr
captureExistential forall r. more r :- less r
evidence Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution
restrictEnv ::
forall more ca less cr.
(forall e m. more e m :- less e m) ->
Advice ca less cr ->
Advice ca more cr
restrictEnv :: (forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m)
-> Advice ca less cr -> Advice ca more cr
restrictEnv forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m
evidence (Advice Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution) =
let captureExistential ::
forall more ca less cr u.
(forall e m. more e m :- less e m) ->
Proxy u ->
( forall as e m.
(All ca as, less e m, Monad m) =>
NP I as ->
DepT e m (u, NP I as)
) ->
( forall e m r.
(less e m, Monad m, cr r) =>
u ->
DepT e m r ->
DepT e m r
) ->
Advice ca more cr
captureExistential :: (forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca more cr
captureExistential forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m
evidence' Proxy u
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs' forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution' =
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, more e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(more e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca more cr
forall u (ca :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice
(Proxy u
forall k (t :: k). Proxy t
Proxy @u)
( let tweakArgs'' :: forall as e m. (All ca as, more e m, Monad m) => NP I as -> DepT e m (u, NP I as)
tweakArgs'' :: NP I as -> DepT e m (u, NP I as)
tweakArgs'' = case more e m :- less e m
forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m
evidence' @e @m of Sub more e m => Dict (less e m)
Dict -> \NP I as
args -> NP I as -> DepT e m (u, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs' @as @e @m NP I as
args
in NP I as -> DepT e m (u, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, more e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs''
)
( let tweakExecution'' :: forall e m r. (more e m, Monad m, cr r) => u -> DepT e m r -> DepT e m r
tweakExecution'' :: u -> DepT e m r -> DepT e m r
tweakExecution'' = case more e m :- less e m
forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m
evidence' @e @m of Sub more e m => Dict (less e m)
Dict -> \u
u DepT e m r
action -> u -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution' @e @m @r u
u DepT e m r
action
in u -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(more e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution''
)
in (forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca more cr
forall (more :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(ca :: * -> Constraint)
(less :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint) u.
(forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca more cr
captureExistential forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m
evidence Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution
restrictResult ::
forall more ca cem less.
(forall r. more r :- less r) ->
Advice ca cem less ->
Advice ca cem more
restrictResult :: (forall r. more r :- less r)
-> Advice ca cem less -> Advice ca cem more
restrictResult forall r. more r :- less r
evidence (Advice Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r
tweakExecution) =
let captureExistential ::
forall more ca cem less u.
(forall r. more r :- less r) ->
Proxy u ->
( forall as e m.
(All ca as, cem e m, Monad m) =>
NP I as ->
DepT e m (u, NP I as)
) ->
( forall e m r.
(cem e m, Monad m, less r) =>
u ->
DepT e m r ->
DepT e m r
) ->
Advice ca cem more
captureExistential :: (forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem more
captureExistential forall r. more r :- less r
evidence' Proxy u
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs' forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r
tweakExecution' =
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, more r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem more
forall u (ca :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice
(Proxy u
forall k (t :: k). Proxy t
Proxy @u)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs'
( let tweakExecution'' :: forall e m r. (cem e m, Monad m, more r) => u -> DepT e m r -> DepT e m r
tweakExecution'' :: u -> DepT e m r -> DepT e m r
tweakExecution'' = case more r :- less r
forall r. more r :- less r
evidence' @r of Sub more r => Dict (less r)
Dict -> \u
u DepT e m r
action -> u -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r
tweakExecution' @e @m @r u
u DepT e m r
action
in u -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, more r) =>
u -> DepT e m r -> DepT e m r
tweakExecution''
)
in (forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem more
forall (more :: * -> Constraint) (ca :: * -> Constraint)
(cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
(less :: * -> Constraint) u.
(forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r)
-> Advice ca cem more
captureExistential forall r. more r :- less r
evidence Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r
tweakExecution
translateEvidence :: forall more less a. (forall x. more x :- less x) -> SOP.Dict more a -> SOP.Dict less a
translateEvidence :: (forall (x :: k). more x :- less x) -> Dict more a -> Dict less a
translateEvidence forall (x :: k). more x :- less x
evidence Dict more a
SOP.Dict =
case more a :- less a
forall (x :: k). more x :- less x
evidence @a of
Sub more a => Dict (less a)
Dict -> less a => Dict less a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
SOP.Dict @less @a