module Control.SMonad where
import Type.Set
import Type.Logic
import Data.Set as Set
class SFunctor dom f | f -> dom where
sfmap' :: x :β: dom ->
y :β: dom ->
(x -> y) -> f x -> f y
class SFunctor dom f => SApplicative dom f | f -> dom where
spure' :: x :β: dom ->
x -> f x
sap' :: x :β: dom ->
y :β: dom ->
(x -> y) :β: dom ->
f (x -> y) -> f x -> f y
class SApplicative dom m => SMonad dom m | m -> dom where
sbind' :: x :β: dom ->
y :β: dom ->
m x -> (x -> m y) -> m y
sfmap :: ( SFunctor dom f
, Fact (x :β: dom)
, Fact (y :β: dom) )
=>
(x -> y) -> f x -> f y
sfmap = sfmap' auto auto
spure :: ( SApplicative dom f
, Fact (x :β: dom) )
=>
x -> f x
spure = spure' auto
sap :: ( SApplicative dom f
, Fact (x :β: dom)
, Fact (y :β: dom)
, Fact ((x -> y) :β: dom) )
=>
f (x->y) -> f x -> f y
sap = sap' auto auto auto
sreturn' :: (SMonad dom f) => (x :β: dom) -> x -> f x
sreturn' = spure'
sreturn :: (SMonad dom f, Fact (x :β: dom)) => x -> f x
sreturn = spure
sbind
:: (Fact (x :β: dom), Fact (y :β: dom), SMonad dom m) =>
m x -> (x -> m y) -> m y
sbind = sbind' auto auto
sjoin'
:: (SMonad dom m) => (m y :β: dom) -> (y :β: dom) -> m (m y) -> m y
sjoin' p1 p2 y = sbind' p1 p2 y id
sjoin
:: (Fact (m y :β: dom), Fact (y :β: dom), SMonad dom m) =>
m (m y) -> m y
sjoin y = sbind y id
sfmap'Default
:: (SMonad dom m) =>
(x :β: dom) -> (y :β: dom) -> (x -> y) -> m x -> m y
sfmap'Default px py f x = sbind' px py x (\x0 -> sreturn' py (f x0))
sap'Default
:: (SMonad dom m) =>
(x :β: dom)
-> (y :β: dom)
-> ((x -> y) :β: dom)
-> m (x -> y)
-> m x
-> m y
sap'Default px py pxy f x = sbind' pxy py f
(\f0 -> sbind' px py x (\x0 -> sreturn' py (f0 x0)))
sliftA2'
:: (SApplicative dom f) =>
(x :β: dom)
-> (y :β: dom)
-> (z :β: dom)
-> ((y -> z) :β: dom)
-> (x -> y -> z)
-> f x
-> f y
-> f z
sliftA2' px py pz pyz f x y =
sap' py pz pyz
(sfmap' px pyz f x)
y
sliftA2
:: (Fact ((x1 -> y) :β: dom),
Fact (y :β: dom),
Fact (x1 :β: dom),
SApplicative dom f,
Fact (x :β: dom)) =>
(x -> x1 -> y) -> f x -> f x1 -> f y
sliftA2 f x y = sfmap f x `sap` y
ssequence'
:: (SApplicative dom f) =>
(a :β: dom)
-> ([a] :β: dom)
-> (([a] -> [a]) :β: dom)
-> [f a]
-> f [a]
ssequence' px pxs pxsxs = go
where
go [] = spure' pxs []
go (x:xs) = sliftA2' px pxs pxs pxsxs (:) x (go xs)
ssequence
:: (Fact (a :β: dom),
Fact ([a] :β: dom),
Fact (([a] -> [a]) :β: dom),
SApplicative dom f) =>
[f a] -> f [a]
ssequence = ssequence' auto auto auto
instance SFunctor OrdType Set where
sfmap' OrdType OrdType = Set.map
instance SApplicative OrdType Set where
spure' OrdType = singleton
sap' = sap'Default
instance SMonad OrdType Set where
sbind' OrdType OrdType xs f = Set.fold (\x r -> Set.union (f x) r) Set.empty xs