MonadMaybe.hs

{-@ LIQUID "--reflection"        @-}
{-@ LIQUID "--ple"               @-}
{- LIQUID "--betaequivalence"   @-}

module MonadMaybe where

import Prelude hiding (return)

import Language.Haskell.Liquid.ProofCombinators

-- | Monad Laws :
-- | Left identity:	  return a >>= f  ≡ f a
-- | Right identity:	m >>= return    ≡ m
-- | Associativity:	  (m >>= f) >>= g ≡	m >>= (\x -> f x >>= g)

{-@ reflect return @-}
return :: a -> Maybe a
return x = Just x

{-@ reflect bind @-}
bind :: Maybe a -> (a -> Maybe b) -> Maybe b
bind m f
  | is_Just m  = f (from_Just m)
  | otherwise  = Nothing

-- | Left Identity

{-@ left_identity :: x:a -> f:(a -> Maybe b) -> {v:Proof | bind (return x) f == f x } @-}
left_identity :: a -> (a -> Maybe b) -> Proof
left_identity x f
  = trivial 



-- | Right Identity

{-@ right_identity :: x:Maybe a -> {v:Proof | bind x return == x } @-}
right_identity :: Maybe a -> Proof
right_identity Nothing
  = trivial 
right_identity (Just x)
  = trivial 


-- | Associativity:	  (m >>= f) >>= g ≡	m >>= (\x -> f x >>= g)
{-@ assume associativity :: m:Maybe a -> f: (a -> Maybe b) -> g:(b -> Maybe c)
      -> {v:Proof | bind (bind m f) g == bind m (\x:a -> (bind (f x) g))} @-}
associativity :: Maybe a -> (a -> Maybe b) -> (b -> Maybe c) -> Proof
associativity Nothing f g
  =   trivial 
associativity (Just x) f g
  =   trivial 

{-@ measure from_Just @-}
from_Just :: Maybe a -> a
{-@ from_Just :: xs:{Maybe a | is_Just xs } -> a @-}
from_Just (Just x) = x


{-@ measure is_Just @-}
is_Just :: Maybe a -> Bool
is_Just (Just _) = True
is_Just _        = False