main.idr

module Main

import Prelude.Functor

total ap : Applicative f => f (a -> b) -> f a -> f b
ap = (<*>)

total maybeAdd1 : Num a => Maybe a -> Maybe a -> Maybe a
maybeAdd1 x y = do x' <- x
                   y' <- y
                   pure (x' + y')

total maybeAdd2 : Num a => Maybe a -> Maybe a -> Maybe a
maybeAdd2 x y = x >>= \x' => y >>= \y' => pure (x' + y')

total maybeAdd3 : Num a => Maybe a -> Maybe a -> Maybe a
maybeAdd3 x y = pure (!x + !y)

total maybeAdd4 : Num a => Maybe a -> Maybe a -> Maybe a
maybeAdd4 x y = [| x + y |]

total maybeAdd5 : Num a => Maybe a -> Maybe a -> Maybe a
maybeAdd5 x y = (+) <$> x <*> y

total maybeAdd6 : Num a => Maybe a -> Maybe a -> Maybe a
maybeAdd6 = liftA2 (+)

total maybeAdd7 : Num a => Maybe a -> Maybe a -> Maybe a
maybeAdd7 = ap . map (+)

total maybeAdd8 : Num a => Maybe a -> Maybe a -> Maybe a
maybeAdd8 = ap . ap (pure (+))

main : IO ()
main = do
  printLn $ maybeAdd1 (Just 1) (Just 2)
  printLn $ maybeAdd2 (Just 1) (Just 2)
  printLn $ maybeAdd3 (Just 1) (Just 2)
  printLn $ maybeAdd4 (Just 1) (Just 2)
  printLn $ maybeAdd5 (Just 1) (Just 2)
  printLn $ maybeAdd6 (Just 1) (Just 2)
  printLn $ maybeAdd7 (Just 1) (Just 2)
  printLn $ maybeAdd8 (Just 1) (Just 2)