|
|
|
|
|
| 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 | |
|
|
|
| | Methods | | | | sap' :: (x :∈: dom) -> (y :∈: dom) -> ((x -> y) :∈: dom) -> f (x -> y) -> f x -> f y | Source |
|
| | | Instances | |
|
|
|
| | Methods | | sbind' :: (x :∈: dom) -> (y :∈: dom) -> m x -> (x -> m y) -> m y | Source |
|
| | | Instances | |
|
|
| Variants using auto for the domain-membership proofs
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Derived combinators
|
|
|
|
|
|
| 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'
|
|
|
|
|
|
|
|
|
|
| Produced by Haddock version 2.4.2 |
