interface Applicative f => Alternative f where
empty : f a
(<|>) : f a -> Lazy (f a) -> f a
Un Applicative muni d'une notion d'échec (empty) et de choix ((<|>)). empty est le calcul qui échoue toujours ; p <|> q essaie p, et se rabat sur q si p échoue. Ensemble, (<|>)/empty forment un monoïde sur les calculs — précisément ce sur quoi reposent les analyseurs à rebroussement et les recherches « premier succès retenu ».
L'empty d'ici est distinct du mempty de Monoid : celui-ci a le type f a (un calcul vide), résolu par son type de résultat. Le second argument est Lazy (comme en Idris 2) : comme pour ||, le choix peut s'en passer, et une grammaire peut s'y citer, expr = atom <|> (… expr …).