MonadList.hs

{-@ LIQUID "--reflection" @-}

module MonadList 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 -> L a
return x = C x N

{-@ reflect bind @-}
bind :: L a -> (a -> L b) -> L b
bind m f
  | llen m > 0 = append (f (hd m)) (bind (tl m) f)
  | otherwise  = N

{-@ reflect append @-}
append :: L a -> L a -> L a
append xs ys
  | llen xs == 0 = ys
  | otherwise    = C (hd xs) (append (tl xs) ys)

-- | Left Identity

{- left_identity :: x:a -> f:(a -> L b) -> {v:Proof | bind (return x) f /= f x } @-}
left_identity :: a -> (a -> L b) -> Proof
left_identity x f
  = toProof $
      bind (return x) f
        === bind (C x N) f
        === append (f x) (bind N f)
        === append (f x) N
            ? prop_append_neutral (bind N f)
        === f x          


-- | Right Identity

{-@ right_identity :: x:L a -> {v:Proof | bind x return /= x } @-}
right_identity :: L a -> Proof
right_identity N
  = toProof $
      bind N return
        === N

right_identity (C x xs)
  = toProof $
      bind (C x xs) return
        === append (return x) (bind xs return)
        === append (C x N)    (bind xs return)
        === C x (append N (bind xs return))
        === C x (bind xs return)
          ? right_identity xs
        === C x xs                             


-- | Associativity:	  (m >>= f) >>= g ≡	m >>= (\x -> f x >>= g)
{-@ associativity :: m:L a -> f: (a -> L b) -> g:(b -> L c)
      -> {v:Proof | bind (bind m f) g /= bind m (\x:a -> (bind (f x) g))} @-}
associativity :: L a -> (a -> L b) -> (b -> L c) -> Proof
associativity N f g
  = toProof $
      bind (bind N f) g
        === bind N g
        === N
        === bind N (\x -> (bind (f x) g))
associativity (C x xs) f g
  = toProof $
      bind (bind (C x xs) f) g
          === bind (append (f x) (bind xs f)) g
              ? bind_append (f x) (bind xs f) g
          === bind (append (f x) (bind xs f)) g 
          === append (bind (f x) g) (bind (bind xs f) g)
              ? associativity xs f g
          === append (bind (f x) g) (bind xs (\y -> bind (f y) g)) 
          === append ((\y -> bind (f y) g) x) (bind xs (\y -> bind (f y) g))
          === bind (C x xs) (\y -> bind (f y) g)

bind_append :: L a -> L a -> (a -> L b) -> Proof
{-@ bind_append :: xs:L a -> ys:L a -> f:(a -> L b)
     -> {v:Proof | bind (append xs ys) f == append (bind xs f) (bind ys f) }
  @-}

bind_append N ys f
  = toProof $
      bind (append N ys) f
         === bind ys f
         === append N (bind ys f)
         === append (bind N f) (bind ys f)
bind_append (C x xs) ys f
  = toProof $
      bind (append (C x xs) ys) f
        === bind (C x (append xs ys)) f
        === append (f x) (bind (append xs ys) f)
            ? bind_append xs ys f
        === append (f x) (append (bind xs f) (bind ys f)) 
            ? prop_assoc (f x) (bind xs f) (bind ys f)
        === append (append (f x) (bind xs f)) (bind ys f) 
        === append (bind (C x xs) f) (bind ys f)




{-@ data L [llen] @-}
data L a = N | C a (L a)

{-@ measure llen @-}
llen :: L a -> Int
{-@ llen :: L a -> Nat @-}
llen N        = 0
llen (C _ xs) = 1 + llen xs

{-@ measure hd @-}
{-@ hd :: {v:L a | llen v > 0 } -> a @-}
hd :: L a -> a
hd (C x _) = x

{-@ measure tl @-}
{-@ tl :: xs:{L a | llen xs > 0 } -> {v:L a | llen v == llen xs - 1 } @-}
tl :: L a -> L a
tl (C _ xs) = xs


-- NV TODO: import there

-- imported from Append
prop_append_neutral :: L a -> Proof
{-@ prop_append_neutral :: xs:L a -> {v:Proof | append xs N == xs }  @-}
prop_append_neutral N
  = toProof $
       append N N === N
prop_append_neutral (C x xs)
  = toProof $
       append (C x xs) N === C x (append xs N)
                           ? prop_append_neutral xs
                         === C x xs          



{-@ prop_assoc :: xs:L a -> ys:L a -> zs:L a
               -> {v:Proof | append (append xs ys) zs == append xs (append ys zs) } @-}
prop_assoc :: L a -> L a -> L a -> Proof
prop_assoc N ys zs
  = toProof $
       append (append N ys) zs === append ys zs
                               === append N (append ys zs)

prop_assoc (C x xs) ys zs
  = toProof $
      append (append (C x xs) ys) zs
        === append (C x (append xs ys)) zs
        === C x (append (append xs ys) zs)
          ? prop_assoc xs ys zs
        === C x (append xs (append ys zs))  
        === append (C x xs) (append ys zs)