Contents Variants using auto for the domain-membership proofs Derived combinators
Description

Example application of sets

This is quite similar to what the rmonad package does, but we use preexisting sets rather than an associated datatype

• The apostrophed variants take proof objects as arguments
• The plain variants use auto; that is, they assume that membership has been proved by an instance of Fact
Synopsis
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
spure :: (SApplicative dom f, Fact (x :∈: dom)) => x -> f x
sap :: (SApplicative dom f, Fact (x :∈: dom), Fact (y :∈: dom), Fact ((x -> y) :∈: dom)) => f (x -> y) -> f x -> f y
sreturn' :: SMonad dom f => (x :∈: dom) -> x -> f x
sreturn :: (SMonad dom f, Fact (x :∈: dom)) => x -> f x
sbind :: (Fact (x :∈: dom), Fact (y :∈: dom), SMonad dom m) => m x -> (x -> m y) -> m y
sjoin' :: SMonad dom m => (m y :∈: dom) -> (y :∈: dom) -> m (m y) -> m y
sjoin :: (Fact (m y :∈: dom), Fact (y :∈: dom), SMonad dom m) => m (m y) -> m y
sfmap'Default :: SMonad dom m => (x :∈: dom) -> (y :∈: dom) -> (x -> y) -> m x -> m y
sap'Default :: SMonad dom m => (x :∈: dom) -> (y :∈: dom) -> ((x -> y) :∈: dom) -> m (x -> y) -> m x -> m y
sliftA2' :: SApplicative dom f => (x :∈: dom) -> (y :∈: dom) -> (z :∈: dom) -> ((y -> z) :∈: dom) -> (x -> y -> z) -> f x -> f y -> f z
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
ssequence' :: SApplicative dom f => (a :∈: dom) -> ([a] :∈: dom) -> (([a] -> [a]) :∈: dom) -> [f a] -> f [a]
ssequence :: (Fact (a :∈: dom), Fact ([a] :∈: dom), Fact (([a] -> [a]) :∈: dom), SApplicative dom f) => [f a] -> f [a]
Documentation
 class SFunctor dom f | f -> dom where Source
Methods
 sfmap' :: (x :∈: dom) -> (y :∈: dom) -> (x -> y) -> f x -> f y Source
Instances
 SFunctor OrdType Set SFunctor OrdType Set
 class SFunctor dom f => SApplicative dom f | f -> dom where Source
Methods
 spure' :: (x :∈: dom) -> x -> f x Source
 sap' :: (x :∈: dom) -> (y :∈: dom) -> ((x -> y) :∈: dom) -> f (x -> y) -> f x -> f y Source
Instances
 SApplicative OrdType Set SApplicative OrdType Set
 class SApplicative dom m => SMonad dom m | m -> dom where Source
Methods
 sbind' :: (x :∈: dom) -> (y :∈: dom) -> m x -> (x -> m y) -> m y Source
Instances
Variants using auto for the domain-membership proofs
 sfmap :: (SFunctor dom f, Fact (x :∈: dom), Fact (y :∈: dom)) => (x -> y) -> f x -> f y Source
 spure :: (SApplicative dom f, Fact (x :∈: dom)) => x -> f x Source
 sap :: (SApplicative dom f, Fact (x :∈: dom), Fact (y :∈: dom), Fact ((x -> y) :∈: dom)) => f (x -> y) -> f x -> f y Source
 sreturn' :: SMonad dom f => (x :∈: dom) -> x -> f x Source
 sreturn :: (SMonad dom f, Fact (x :∈: dom)) => x -> f x Source
 sbind :: (Fact (x :∈: dom), Fact (y :∈: dom), SMonad dom m) => m x -> (x -> m y) -> m y Source
Derived combinators
 sjoin' :: SMonad dom m => (m y :∈: dom) -> (y :∈: dom) -> m (m y) -> m y Source
 sjoin :: (Fact (m y :∈: dom), Fact (y :∈: dom), SMonad dom m) => m (m y) -> m y Source
 sfmap'Default :: SMonad dom m => (x :∈: dom) -> (y :∈: dom) -> (x -> y) -> m x -> m y Source
sfmap' in terms of spure' and sbind'
 sap'Default :: SMonad dom m => (x :∈: dom) -> (y :∈: dom) -> ((x -> y) :∈: dom) -> m (x -> y) -> m x -> m y Source
sap' in terms of spure' and sbind'
 sliftA2' :: SApplicative dom f => (x :∈: dom) -> (y :∈: dom) -> (z :∈: dom) -> ((y -> z) :∈: dom) -> (x -> y -> z) -> f x -> f y -> f z Source
 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 Source
 ssequence' :: SApplicative dom f => (a :∈: dom) -> ([a] :∈: dom) -> (([a] -> [a]) :∈: dom) -> [f a] -> f [a] Source
 ssequence :: (Fact (a :∈: dom), Fact ([a] :∈: dom), Fact (([a] -> [a]) :∈: dom), SApplicative dom f) => [f a] -> f [a] Source
Produced by Haddock version 2.4.2