A filter implementation on objective

filter.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}


module
    Main
where

import Prelude hiding (filter)  
import Control.Object
import Control.Monad.Trans.State.Strict
import Control.Monad.IO.Class
import Control.Monad (liftM)
import Control.Monad.Fix
import Control.Monad.Trans
import Control.Monad.Operational




--
-- 基礎
--
sequential :: Monad m => Object t m -> Object (Program t) m
sequential r = Object $ liftM (fmap sequential) . inv r
  where
    inv :: Monad m => Object t m -> Program t t1 -> m (t1, Object t m)
    inv obj (Program (Pure x)) = return (x, obj)
    inv obj (Program (Free (CoYoneda f x))) 
      = runObject obj x >>= \(a, obj') -> inv obj' (Program . f $ a)


data Sum f g a = InL (f a) | InR (g a)


--
-- filterの定義
--
data Fails f a
  where
    Fails :: f x -> Fails f (Maybe x)
type Failable f = Program (Fails f)

maybeFail :: f a -> Failable f (Maybe a)
maybeFail = singleton . Fails



filter ::
    (forall x. f x -> Bool) ->
    Object (Failable f) (Program f)
filter cond = liftO $ interpret $ \(Fails fx) ->
    if cond fx
      then do
        x <- singleton fx
        return $ Just x
      else
        return $ Nothing
    

--
-- 実装例
--
data
    Command a
  where
    Str :: String -> Command ()
    I :: Int -> Command ()


writer ::
    MonadIO m =>
    Object Command m

writer = Object $ \case
    Str s ->
      do
        liftIO $ putStrLn s
        return ((), writer)
    I i ->
      do
        liftIO $ putStrLn $ "Integer " ++ show i
        return ((), writer)


isEven :: Command a -> Bool
isEven (I i) = (i `mod` 2) == 0
isEven _ = True


isStr :: Command a -> Bool
isStr (Str _) = True
isStr _ = False


main =
  do
    putStrLn "Plain writer ---"
    w1 <- new $ writer
    w1.-Str "aaa"
    w1.-I 3
    w1.-I 4

    putStrLn "isEven ---"
    w2 <- new $ filter isEven @>>@ sequential writer
    w2.-maybeFail (Str "aaa")
    w2.-maybeFail (I 3)
    w2.-maybeFail (I 4)

    putStrLn "Not isStr ---"
    w3 <- new $ filter (not . isStr) @>>@ sequential writer
    w3.-maybeFail (Str "bbb")
    w3.-maybeFail (I 3)
    w3.-maybeFail (I 4)