{-# LANGUAGE ImpredicativeTypes #-}
module Polysemy.IdempotentLowering
( (.@!)
, nat
, liftNat
, fixedNat
, (.@@!)
, nat'
, liftNat'
, fixedNat'
) where
import Polysemy
import Data.Coerce
newtype Nat m n = Nat (∀ x. m x -> n x)
nat :: Applicative base => (∀ x. m x -> n x) -> base (∀ x. m x -> n x)
nat :: (forall (x :: k). m x -> n x) -> base (forall (x :: k). m x -> n x)
nat forall (x :: k). m x -> n x
f = (forall (x :: k). m x -> n x) -> base (forall (x :: k). m x -> n x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((forall (x :: k). m x -> n x)
-> base (forall (x :: k). m x -> n x))
-> (forall (x :: k). m x -> n x)
-> base (forall (x :: k). m x -> n x)
forall a b. (a -> b) -> a -> b
$ Nat m n -> forall (x :: k). m x -> n x
coerce (Nat m n -> forall (x :: k). m x -> n x)
-> Nat m n -> forall (x :: k). m x -> n x
forall a b. (a -> b) -> a -> b
$ (forall (x :: k). m x -> n x) -> Nat m n
forall k (m :: k -> *) (n :: k -> *).
(forall (x :: k). m x -> n x) -> Nat m n
Nat forall (x :: k). m x -> n x
f
newtype Nat' m n f = Nat' (∀ x. m x -> n (f x))
nat' :: Applicative base => (∀ x. m x -> n (f x)) -> base (∀ x. m x -> n (f x))
nat' :: (forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x))
nat' forall (x :: k). m x -> n (f x)
f = (forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x)))
-> (forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x))
forall a b. (a -> b) -> a -> b
$ Nat' m n f -> forall (x :: k). m x -> n (f x)
coerce (Nat' m n f -> forall (x :: k). m x -> n (f x))
-> Nat' m n f -> forall (x :: k). m x -> n (f x)
forall a b. (a -> b) -> a -> b
$ (forall (x :: k). m x -> n (f x)) -> Nat' m n f
forall k k (m :: k -> *) (n :: k -> *) (f :: k -> k).
(forall (x :: k). m x -> n (f x)) -> Nat' m n f
Nat' forall (x :: k). m x -> n (f x)
f
(.@!)
:: (Monad base, Monad m)
=> base (∀ x. Sem r x -> m x)
-> ( (∀ x. Sem r x -> m x)
-> base ( ∀ y
. Sem (e ': r) y
-> Sem r y
)
)
-> base (∀ z. Sem (e ': r) z -> m z)
base (forall x. Sem r x -> m x)
fi .@! :: base (forall x. Sem r x -> m x)
-> ((forall x. Sem r x -> m x)
-> base (forall y. Sem (e : r) y -> Sem r y))
-> base (forall z. Sem (e : r) z -> m z)
.@! (forall x. Sem r x -> m x)
-> base (forall y. Sem (e : r) y -> Sem r y)
gi = do
forall x. Sem r x -> m x
f <- base (forall x. Sem r x -> m x)
fi
forall y. Sem (e : r) y -> Sem r y
g <- (forall x. Sem r x -> m x)
-> base (forall y. Sem (e : r) y -> Sem r y)
gi (\Sem r x
x -> Sem r x -> m x
forall x. Sem r x -> m x
f Sem r x
x)
(forall z. Sem (e : r) z -> m z)
-> base (forall z. Sem (e : r) z -> m z)
forall k (base :: * -> *) (m :: k -> *) (n :: k -> *).
Applicative base =>
(forall (x :: k). m x -> n x) -> base (forall (x :: k). m x -> n x)
nat ((forall z. Sem (e : r) z -> m z)
-> base (forall z. Sem (e : r) z -> m z))
-> (forall z. Sem (e : r) z -> m z)
-> base (forall z. Sem (e : r) z -> m z)
forall a b. (a -> b) -> a -> b
$ \Sem (e : r) x
z -> Sem r x -> m x
forall x. Sem r x -> m x
f (Sem r x -> m x) -> Sem r x -> m x
forall a b. (a -> b) -> a -> b
$ Sem (e : r) x -> Sem r x
forall y. Sem (e : r) y -> Sem r y
g Sem (e : r) x
z
infixl 8 .@!
(.@@!)
:: (Monad base, Monad m)
=> base (∀ x. Sem r x -> m x)
-> ( (∀ x. Sem r x -> m x)
-> base ( ∀ y
. Sem (e ': r) y
-> Sem r (f y)
)
)
-> base (∀ z. Sem (e ': r) z -> m (f z))
base (forall x. Sem r x -> m x)
fi .@@! :: base (forall x. Sem r x -> m x)
-> ((forall x. Sem r x -> m x)
-> base (forall y. Sem (e : r) y -> Sem r (f y)))
-> base (forall z. Sem (e : r) z -> m (f z))
.@@! (forall x. Sem r x -> m x)
-> base (forall y. Sem (e : r) y -> Sem r (f y))
gi = do
forall x. Sem r x -> m x
f <- base (forall x. Sem r x -> m x)
fi
forall y. Sem (e : r) y -> Sem r (f y)
g <- (forall x. Sem r x -> m x)
-> base (forall y. Sem (e : r) y -> Sem r (f y))
gi (\Sem r x
x -> Sem r x -> m x
forall x. Sem r x -> m x
f Sem r x
x)
(forall z. Sem (e : r) z -> m (f z))
-> base (forall z. Sem (e : r) z -> m (f z))
forall k k (base :: * -> *) (m :: k -> *) (n :: k -> *)
(f :: k -> k).
Applicative base =>
(forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x))
nat' ((forall z. Sem (e : r) z -> m (f z))
-> base (forall z. Sem (e : r) z -> m (f z)))
-> (forall z. Sem (e : r) z -> m (f z))
-> base (forall z. Sem (e : r) z -> m (f z))
forall a b. (a -> b) -> a -> b
$ \Sem (e : r) x
z -> Sem r (f x) -> m (f x)
forall x. Sem r x -> m x
f (Sem r (f x) -> m (f x)) -> Sem r (f x) -> m (f x)
forall a b. (a -> b) -> a -> b
$ Sem (e : r) x -> Sem r (f x)
forall y. Sem (e : r) y -> Sem r (f y)
g Sem (e : r) x
z
infixl 8 .@@!
liftNat
:: Applicative base
=> (forall x. (forall y. f y -> g y) -> m x -> n x)
-> (forall y. f y -> g y) -> base (forall x. m x -> n x)
liftNat :: (forall (x :: k). (forall (y :: k). f y -> g y) -> m x -> n x)
-> (forall (y :: k). f y -> g y)
-> base (forall (x :: k). m x -> n x)
liftNat forall (x :: k). (forall (y :: k). f y -> g y) -> m x -> n x
z forall (y :: k). f y -> g y
a = (forall (x :: k). m x -> n x) -> base (forall (x :: k). m x -> n x)
forall k (base :: * -> *) (m :: k -> *) (n :: k -> *).
Applicative base =>
(forall (x :: k). m x -> n x) -> base (forall (x :: k). m x -> n x)
nat ((forall (x :: k). m x -> n x)
-> base (forall (x :: k). m x -> n x))
-> (forall (x :: k). m x -> n x)
-> base (forall (x :: k). m x -> n x)
forall a b. (a -> b) -> a -> b
$ (forall (y :: k). f y -> g y) -> m x -> n x
forall (x :: k). (forall (y :: k). f y -> g y) -> m x -> n x
z forall (y :: k). f y -> g y
a
liftNat'
:: Applicative base
=> (forall x. (forall y. f y -> g y) -> m x -> n (f x))
-> (forall y. f y -> g y) -> base (forall x. m x -> n (f x))
liftNat' :: (forall (x :: k). (forall (y :: k). f y -> g y) -> m x -> n (f x))
-> (forall (y :: k). f y -> g y)
-> base (forall (x :: k). m x -> n (f x))
liftNat' forall (x :: k). (forall (y :: k). f y -> g y) -> m x -> n (f x)
z forall (y :: k). f y -> g y
a = (forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x))
forall k k (base :: * -> *) (m :: k -> *) (n :: k -> *)
(f :: k -> k).
Applicative base =>
(forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x))
nat' ((forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x)))
-> (forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x))
forall a b. (a -> b) -> a -> b
$ (forall (y :: k). f y -> g y) -> m x -> n (f x)
forall (x :: k). (forall (y :: k). f y -> g y) -> m x -> n (f x)
z forall (y :: k). f y -> g y
a
fixedNat
:: forall m n base
. Applicative base
=> ((forall x. m x -> n x) -> (forall x. m x -> n x))
-> base (forall x. m x -> n x)
fixedNat :: ((forall (x :: k). m x -> n x) -> forall (x :: k). m x -> n x)
-> base (forall (x :: k). m x -> n x)
fixedNat (forall (x :: k). m x -> n x) -> forall (x :: k). m x -> n x
f =
let x :: (forall x. m x -> n x)
x :: m x -> n x
x = (forall (x :: k). m x -> n x) -> forall (x :: k). m x -> n x
f forall (x :: k). m x -> n x
x
in (forall (x :: k). m x -> n x) -> base (forall (x :: k). m x -> n x)
forall k (base :: * -> *) (m :: k -> *) (n :: k -> *).
Applicative base =>
(forall (x :: k). m x -> n x) -> base (forall (x :: k). m x -> n x)
nat forall (x :: k). m x -> n x
x
fixedNat'
:: forall m n f base
. Applicative base
=> ((forall x. m x -> n (f x)) -> (forall x. m x -> n (f x)))
-> base (forall x. m x -> n (f x))
fixedNat' :: ((forall (x :: k). m x -> n (f x))
-> forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x))
fixedNat' (forall (x :: k). m x -> n (f x))
-> forall (x :: k). m x -> n (f x)
f =
let x :: (forall x. m x -> n (f x))
x :: m x -> n (f x)
x = (forall (x :: k). m x -> n (f x))
-> forall (x :: k). m x -> n (f x)
f forall (x :: k). m x -> n (f x)
x
in (forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x))
forall k k (base :: * -> *) (m :: k -> *) (n :: k -> *)
(f :: k -> k).
Applicative base =>
(forall (x :: k). m x -> n (f x))
-> base (forall (x :: k). m x -> n (f x))
nat' forall (x :: k). m x -> n (f x)
x