Heim (1983) monadically

Heim.hs

import           Control.Applicative
import           Control.Monad
import           Data.List

data Atom = P | Q | R | Top
  deriving (Show, Eq, Enum)

type W = [Atom]
type C = [W]
type Upd m = m C -> m C

c0 :: Monad m => m C
c0 = return $ subsequences (init [P ..])

-- Update Heim
--
atomD :: Monad m => Atom -> Upd m
atomD Top = id
atomD at  = (filter (at `elem`) <$>)

conjD :: Monad m => Upd m -> Upd m -> Upd m
conjD l r = r . l

negD :: Monad m => Upd m -> Upd m
negD p mc = (\\) <$> mc <*> p mc

partD :: (Monad m, Eq (m C), Alternative m) => Upd m -> Upd m
partD p mc = guard (p mc == mc) >> mc

-- Test cases
--
test1 = conjD (partD (atomD P)) (atomD P) $ c0 :: Maybe C
test2 = conjD (atomD P) (partD (atomD P)) $ c0 :: Maybe C
test3 = partD (atomD Top) $ c0 :: Maybe C

-- "Static" Heim
--
type Trival m = ReaderT W m T

atomS :: Monad m => Atom -> Trival m
atomS Top = ReaderT $ const (return True)
atomS at  = ReaderT $ return . (at `elem`)

conjS :: Monad m => Trival m -> (T -> Trival m) -> Trival m
conjS = (>>=)

negS :: Monad m => Trival m -> Trival m
negS = (not <$>)

partS :: (Monad m, Alternative m) => Trival Maybe -> Trival m
partS m = ReaderT $ \w ->
  guard (runReaderT m w == Just True) >> return True

filtS :: Monad m => Trival m -> T -> Trival m
filtS m bool = if bool then m else return False

toUpd :: (Monad m, Alternative m) => Trival Maybe -> Upd m
toUpd (ReaderT f) mc = do
  c <- mc
  if all (\w -> f w /= Nothing) c
  then return [w | w <- c, f w == Just True]
  else empty

-- Test cases
--
test5 = toUpd (conjS (partS (atomS P)) (filtS (atomS P))) c0 :: Maybe C
test6 = toUpd (conjS (atomS P) (filtS (partS (atomS P)))) c0 :: Maybe C