>>65095623You generally want a nice toolbox of compbinators. Some examples include:

getOr : (Maybe<A>, A) -> A

getOrDelayed : (Maybe<A>, () -> A) -> A

getOrExn : (Maybe<A>) -> A // throws exception on null

map : (Maybe<A>, A -> B) -> Maybe<B> // "functor"

both : (Maybe<A>, Maybe<B>) -> Maybe<Pair<A,B>> // "applicative"

then : (Maybe<A>, A -> Maybe<B>) -> Maybe<B> // "monad"

all : (List<Maybe<A>>) -> Maybe<List<A>>

>>65095631Why does everyone keep listening to the Idris shills, its literally a worse Agda