def Control.Applicative.optional {f : Type u_1 → Type u_2} {α : Type u_1} [Alternative f] (fa : f α) : f (Option α)

Try an action, returning some on success or none on failure.

$$\text{optional}\;fa = (\text{some} \mathbin{<\$>} fa) \mathbin{<|>} \text{pure}\;\text{none}$$

Equations

• Control.Applicative.optional fa = (some <$> fa <|> pure none)

def Control.Applicative.asum {f : Type u_1 → Type u_2} {α : Type u_1} [Alternative f] : List (f α) → f α

Fold a list of alternatives with <|>, starting from failure.

$$\text{asum}\;[a_1, \ldots, a_n] = a_1 \mathbin{<|>} \cdots \mathbin{<|>} a_n \mathbin{<|>} \text{failure}$$

Equations

• Control.Applicative.asum [] = failure
• Control.Applicative.asum (x_1 :: xs) = (x_1 <|> Control.Applicative.asum xs)

def Control.Applicative.guard {f : Type → Type u_1} [Alternative f] (b : Bool) : f Unit

Conditional failure: succeeds with () if the boolean is true, fails otherwise.

$$\text{guard}\;b = \begin{cases} \text{pure}\;() & \text{if } b \\ \text{failure} & \text{otherwise} \end{cases}$$

Equations

• Control.Applicative.guard b = if b = true then pure () else failure