|
|
|
|
|
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 |