Definitions
trait type Applicative (F : Type -> Type)Source#
| mkApplicative@{ {{functor}} : Functor F; pure : {A : Type} -> A -> F A; ap : {A B : Type} -> F (A -> B) -> F A -> F B; } |
open Applicative public
applicativeSeq {F : Type -> Type} {{Applicative F}} {A B : Type} (fa : F A) (fb : F B) : F BSource#
Sequences computations. Note that this function will be renamed to >>> once IO becomses a polymorphic type and can be given an Applicative instance.
liftA2 {F : Type -> Type} {{Applicative F}} {A B C} (fun : A -> B -> C) : F A -> F B -> F CSource#
lifts a binary function to Applicative
mapA_ {t : Type -> Type} {f : Type -> Type} {A B} {{Foldable t}} {{Applicative f}} (fun : A -> f B) (l : t A) : f UnitSource#
replicateA {F : Type -> Type} {A} {{Applicative F}} : Nat -> F A -> F (List A)Source#