Haskell - Смешанные отслеживанием состояния вычисления

Question

Учитывая следующую структуру:

data Computation a = Pure (CState -> (a, CState)) 
        | Action (CState -> IO (a, CState)) 

(Cstate некоторое структура используется для сохранения состояния, но это не представляет большого интереса в настоящее время.)
Теперь я хочу, чтобы сделать его экземпляр Монады, которая в основном является государственной монадой и будет легко реализована с помощью StateT. Единственное, что у меня есть, это то, что я хочу отслеживать, является ли итоговое вычисление Pure on или Action, и я хочу, чтобы проверить, содержит ли Computation Action s, перед выполнением Action (поэтому IO в Action не выполняется).

Следует также отметить, что на самом деле не имеет значения, что Computation имеет два конструктора. Я только начал реализовывать это с помощью этих конструкторов.

Правила определения того a >> b Незапятнанно просто: a >> b является Pure если a и b являются как Pure противном случае это действие.

Теперь я приступил к реализации экземпляра Monad:

instance Monad Computation where 
    return x = Pure $ \s -> (x, s) 
    (Action c) >>= f = Action . runStateT $ 
         (StateT $ unpackAction oldComp) >>= (StateT . unpackAction . f) 
    p@(Pure c) >>= f 
     | givesPure f = Pure . runState $ 
         state oldF >>= (state . unpackPure . f) 
     | otherwise = liftComp p >>= f -- Just lift the first argument and recurse, to make an action 

-- Helper functions used above: 
unpackAction :: Computation a -> (CState -> IO (a, CState)) 
unpackAction (Pure c) = return . c 
unpackAction (Action c) = c 

-- Make an Action out of a Pure 
liftComp :: Computation a -> Computation a 
liftComp (Pure c) = Action $ return . c 
liftComp a@(Action _) = a 

Так что только недостающая часть является givesPure функцией, и я не уверен, если это вообще возможно реализовать его. Я когда-то реализация подобного:

givesPure :: (a -> Computation b) -> Bool 
givesPure f = isPure $ f undefined -- I actually used error with a custom message instead of undefined, but that shouldn't matter 

isPure :: Computation a -> Bool 
isPure (Pure _) = True 
isPure (Action _) = False 

Это работает, но делает предположение о том, что функция, которую я связываясь с, во все дни возвращает вычисления с такой же чистотой, независимо от того, что его вход. Это предположение оказалось достаточно для меня, так как чистота вычислений должны быть четко определены и не зависят от некоторых вычислений, пока я не заметил, что функция в виде dosn't работы с этим предположением:

baz :: Int -> Computation b 
baz x = if x > 5 
     then foo 
     else bar 
-- foo and bar both have the type Computation b 

Так мне кажется, что это невозможно сделать, так как мне нужно текущее состояние, чтобы применить первое вычисление, чтобы получить правильный ввод для функции, чтобы получить второе вычисление и проверить, является ли он чистым.

Кто-нибудь видит решение этого или имеет доказательство того, что это невозможно?

Answer 1

Вы можете попробовать использовать GADT:

data Pure 
data Action 

data Computation t a where 
    Pure :: (CState -> (a, CState))  -> Computation t a 
    Action :: (CState -> IO (a, CState)) -> Computation Action a 

Идея заключается в том, что значение x :: Computation Action a может сделать IO (но может также быть чистым), в то время как значение y :: Computation Pure a не может сделать IO.

Например,

liftComp :: Computation t a -> Computation Action a 
liftComp (Pure c) = Pure c 
liftComp x@(Action c) = x 

Answer 2

Вы столкнулись с тем фактом, что монадические вычисления не подходят для статического анализа, потому что эффекты (в вашем случае, наличие эффектов) зависят от значений, полученных при самом вычислении. Вы не можете предсказать их, не запуская вычисления.

Как вы идете от Applicative к Arrow в Monad, вы получаете в «власть» (вы можете выразить больше вычислений), но теряют в аменабельностью для статического анализа.

Для Applicative s имеется готовый тип данных Lift, который добавляет чистое вычисление к уже существующему приложению. Но у него нет экземпляра Monad.