0 | module Control.Applicative.Restricted
 1 |
 2 | import Data.Functor.Restricted
 3 |
 4 |
 5 | export infixl 4 <*
 6 | export infixl 4 *>
 7 |
 8 |
 9 | -- We provide a restricted version of liftA2 rather than of <*>, since
10 | -- in cases of interest (x -> y) does not satisfy the restriction.
11 | public export
12 | interface RFunctor r f => RApplicative (0 r : Type -> Type) (0 f : Type -> Type) | f where
13 |   rpure : r x => x -> f x
14 |   rliftA2 : (r x, r y, r z) => (x -> y -> z) -> f x -> f y -> f z
15 |
16 | export
17 | (<*) : (RApplicative r f, r x, r y) => f x -> f y -> f x
18 | (<*) = rliftA2 const
19 |
20 | export
21 | (*>) : (RApplicative r f, r x, r y) => f x -> f y -> f y
22 | (*>) = rliftA2 (const id)
23 |
24 | public export
25 | data RApp : (Type -> Type) -> (Type -> Type) -> Type -> Type where
26 |   MkRApp : f x -> RApp r f x
27 |
28 | (RApplicative r f, Monoid m, r m) => Semigroup (RApp r f m) where
29 |   (<+>) (MkRApp x) (MkRApp y) = MkRApp (rliftA2 (<+>) x y)
30 |
31 | (RApplicative r f, Monoid m, r m) => Monoid (RApp r f m) where
32 |   neutral = MkRApp $ rpure neutral
33 |