module Data.Maybe
export  { isNothing; isJust; fromMaybe }
import Class.Functor
import Class.Applicative
import Class.Monad
import Data.Numeric.Bool
where


-- | A `Maybe` may contain a value, or not.
data Maybe (a: Data) where
        Nothing : Maybe a
        Just    : a -> Maybe a


-- Functor --------------------------------------------------------------------
functor_maybe
 = Functor 
        maybe_fmap
 where 
        maybe_fmap : [a b: Data]. (a -> b) -> Maybe a -> Maybe b
        maybe_fmap f xx 
         = case xx of
               Nothing -> Nothing
               Just x  -> Just (f x)


-- Applicative ----------------------------------------------------------------
applicative_maybe
 = Applicative 
        functor_maybe 
        maybe_pure
        maybe_ap
 where
        maybe_pure : [a: Data]. a -> Maybe a
        maybe_pure x
         = Just x

        maybe_ap   : [a b: Data]. Maybe (a -> b) -> Maybe a -> Maybe b
        maybe_ap mf ma
         | Just xf      <- mf
         , Just xa      <- ma
         = Just (xf xa)

         | otherwise
         = Nothing


-- Monad ----------------------------------------------------------------------
monad_maybe
 = Monad
        applicative_maybe
        maybe_return
        maybe_bind
 where  
        maybe_return : [a: Data]. a -> Maybe a
        maybe_return x
         = Just x

        maybe_bind   : [a b: Data]. Maybe a -> (a -> Maybe b) -> Maybe b
        maybe_bind ma f         
         = case ma of
                Nothing -> Nothing
                Just xa -> f xa


-- Predicates -----------------------------------------------------------------
-- | Check if the given value is a `Nothing`.
isNothing (m: Maybe a): Bool
 = case m of
        Nothing -> True
        Just x  -> False


-- | Check if the given value is a `Just`.
isJust (m: Maybe a): Bool
 = case m of
        Nothing -> False
        Just x  -> True


-- Destructors ----------------------------------------------------------------
-- | Take the value from a `Just`, or return a default value.
fromMaybe (def: a) (m: Maybe a): a
 = case m of
        Nothing -> def
        Just x  -> x


-- | Apply a function to the value in a `Just`, or return a default value.
maybe (def: b) (f: a -> b) (m: Maybe a): b
 = case m of
        Nothing -> def
        Just x  -> f x