LMonadEquality.hs

module LMonadEquality where

import LFunctor -- Liquid Haskell Functor data class

--------------------------------------------------------------------------------
-- Monad
--------------------------------------------------------------------------------

-- Data Class.
{-@
data LMonad m = LMonad
  { iFunctor :: LFunctor m
  , lift :: forall a . a -> m a
  , bind :: forall a b . m a -> (a -> m b) -> m b
  , bind_correct :: forall a b . m:m a -> f:(a -> b) ->
      {bind m (vcomp lift f) = vmapF iFunctor f m}
  , bind_identity :: forall a . m:m a ->
      {bind m lift = m}
  , bind_lift :: forall a b . k:(a -> m b) -> x:a ->
      {bind (lift x) k = k x}
  , bind_associative :: forall a b c . m:m a -> k1:(a -> m b) -> k2:(b -> m c) ->
      {bind (bind m k1) k2 = bind m (raw_kleisli bind k1 k2)}
  }
@-}
data LMonad m = LMonad
  { iFunctor :: LFunctor m,
    lift :: forall a. a -> m a,
    bind :: forall a b. m a -> (a -> m b) -> m b,
    bind_correct :: forall a b. m a -> (a -> b) -> Proof,
    bind_identity :: forall a. m a -> Proof,
    bind_lift :: forall a b. (a -> m b) -> a -> Proof,
    bind_associative :: forall a b c. m a -> (a -> m b) -> (b -> m c) -> Proof
  }

-- Function.
{-@ reflect raw_kleisli @-}
raw_kleisli ::
  forall m a b c.
  (m b -> (b -> m c) -> m c) -> -- bind
  (a -> m b) ->
  (b -> m c) ->
  (a -> m c)
raw_kleisli (>>=) f g x = f x >>= g

-- Function.
{-@ reflect kleisli @-}
kleisli :: forall m a b c. LMonad m -> (a -> m b) -> (b -> m c) -> (a -> m c)
kleisli iMonad = raw_kleisli (>>=)
  where
    (>>=) = bind iMonad

--------------------------------------------------------------------------------
-- Equality
--------------------------------------------------------------------------------

{-@ measure meq :: LMonad m -> m a -> m a -> Bool @-}

{-@ type MEq m a iMonad m1 m2 = {_:MBEq m a | meq iMonad m1 m2} @-}

{-@
data MBEq :: (* -> *) -> * -> * where
    MBEq_lift :: forall m a. iMonad:LMonad m ->
      x:a -> y:a -> {pf:Proof | x = y} ->
      MEq m a iMonad (lift iMonad x) (lift iMonad y)
  | MBEq_bind :: forall m a b. iMonad:LMonad m ->
      m1:m a -> m2: m a -> MEq m a iMonad m1 m2 ->
      k1:(a -> m b) -> k2:(a -> m b) -> (x:a -> MEq m b iMonad (k1 x) (k2 x)) ->
      MEq m b iMonad (bind m1 k1) (bind m2 k2)
@-}
data MBEq :: (* -> *) -> * -> * where
  MBEq_lift ::
    forall m a.
    LMonad m ->
    a -> -- x
    a -> -- y
    Proof -> -- x = y
    -----------------------------------
    MBEq m a -- lift x = lift y
  MBEq_bind ::
    forall m a b.
    LMonad m ->
    m a -> -- m1
    m a -> -- m2
    MBEq m a -> -- m1 = m2
    (a -> m b) -> -- k1
    (a -> m b) -> -- k2
    (a -> MBEq m b) -> -- forall x, k1 x = k2 x
    MBEq m b -- m1 >>= k1 = m2 >>= k2