Does idris support a way to collapse symmetrical statements into one?

Question

I'm new to functional programming, so working through 'Type Driven Development with Idris'. Give a function maxMaybe that can compute the max between two Maybe Doubles, defines as below

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
maxMaybe x Nothing = x
maxMaybe Nothing Nothing = Nothing
maxMaybe (Just x) (Just y) = Just (max x y)

Is there a way to collapse the following cases into just one, since the positions don't matter?

maxMaybe Nothing y = y
maxMaybe x Nothing = x

I would also be curious to know if this kind of thing is handled generally in other purely functional programming languages like Haskell or OCaml

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
-- maxMaybe x Nothing = x
maxMaybe Nothing Nothing = Nothing
maxMaybe (Just x) (Just y) = Just (max x y)

maxMaybe (Just 5) (Nothing) maxMaybe (Just 5) Nothing : Maybe Integer

Answer 1

You can write

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe mx my = [| max mx my |] <|> mx <|> my

but it will probably be more expensive at runtime as you'll redo a lot of the case analysis unless enough compiler optimisations kick in to give you something essentially equivalent to your original solution.

Answer 2

In Haskell an idea might be to work with the Min semigroup and wrap use this:

import Data.Function (on)
import Data.Semigroup (Max (Max, getMax))

maxMaybe :: Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe = on ((fmap getMax .) . (<>)) (fmap Max)

you can easily generalize this to any Semigroup like structure:

semiFunc :: (Functor f, Semigroup (f b)) => (a -> b) -> (b -> c) -> f a -> f a -> f c
semiFunc f g = on ((fmap g .) . (<>)) (fmap f)

then maxMaybe is a special case of semiFunc with maxMaybe = semiFunc Max getMax.

Answer 3

You have asked both answers in Haskell and in OCaml, and so far only answer in Haskell have been provided. Therefore, I will give the OCaml equivalent, and not repeat the Haskell code.

Since the question is specifically about merging together symmetrical branches of a match statement, here is how your version could have been written in OCaml:

let max_option x y = match x, y with
  | None, y -> y
  | x, None -> x
  | None, None -> None
  | Some x, Some y -> Some (max x y)

And here is how the folded version would be

let max_option x y = match x, y with
  | None, v | v, None -> v (* two branches are merged *)
  | Some x, Some y -> Some (max x y)
  (* the `None, None` branch has been deleted as it was redundant *)

But, for this specific case, since 'a option (Maybe a in Haskell) is a monad, it would be more idiomatic to use monadic let bindings:

let max_option x y =
  let (let>) = Option.bind in
  let> x = x in
  let> y = y in
  Some (max x y)

Since the example is a bit contrived, you get some weird let> x = x statements. You could probably use more higher-kind functions, but I don't think it would result in much more idiomatic OCaml code, contrary to Haskell.