interface Applicative f => Alternative f where
empty : f a
(<|>) : f a -> Lazy (f a) -> f aAn Applicative with a notion of failure (empty) and choice ((<|>)). empty is the computation that always fails; p <|> q tries p, and falls back to q if p fails. Together they make (<|>)/empty a monoid on computations — which is exactly what backtracking parsers and "first match wins" lookups are built from.
empty here is distinct from Monoid's mempty: this one has type f a (an empty computation), resolved by its result type. The second argument is Lazy (as in Idris 2): like ||, the choice may not need it, and a grammar can cite itself there, expr = atom <|> (… expr …).