?

Log in

No account? Create an account
Previous Entry Share Next Entry
MonadSum
eye
voidex
Подумалось мне про трансформеры монад, что если у нас есть натуральные преобразования из монад m и n в некую монаду l, то l — это их сумма, если добавить ещё и обратную функцию. Т.е. при наличии натурального преобразования m => t и n => t можем получить и m+n => t.

Попробовал я это представить прямо в таком виде:
data MonadSum m n a = MonadSum {
  monadSum :: forall t. (Monad t) => (forall b. m b -> t b) -> (forall c. n c -> t c) -> t a }


И вот, что получилось:
maybeIO :: Maybe a -> StateT s IO a
maybeIO Nothing = error "Nothing"
maybeIO (Just v) = return v

eitherIO :: Either String a -> StateT s IO a
eitherIO (Left e) = error e
eitherIO (Right v) = return v

stateIO :: State s a -> StateT s IO a
stateIO act = StateT $ return . runState act

bla :: MonadSum Maybe (MonadSum (Either String) (State Int)) String
bla = do
  n <- liftR $ liftR get
  case n of
    0 -> liftL Nothing
    1 -> liftR $ liftL $ Left "Error"
    2 -> liftR $ liftL $ Right "Ok!"
    _ -> do
      liftR $ liftR $ put (n `div` 2)
      s <- bla
      return $ show n ++ s

testBla :: Int -> IO String
testBla = evalStateT $ unlift maybeIO (unlift eitherIO stateIO) bla

Запуск:
*MonadSum> testBla 0
*** Exception: Nothing
*MonadSum> testBla 1
*** Exception: Error
*MonadSum> testBla 2
"Ok!"
*MonadSum> testBla 3
*** Exception: Error
*MonadSum> testBla 4
"4Ok!"
*MonadSum> testBla 8
"84Ok!"
*MonadSum> testBla 7
*** Exception: Error


Полный код тут.

  • 1
Что-то ваше instance Monad (MonadSum m n) жутко похоже на instance Monad (ReaderT r m). Сравните здесь.

Ну да, похоже на ReaderT от forall t. (forall a. m a -> t a, forall a. n a -> t a).

Ваши функции типов forall b. m b -> t b, forall c. n c -> t c — это морфизмы монад или что?

Да, морфизм монад:
lift : m => t -- натуральное преобразование

при этом, как я понимаю, должны выполняться:
return = lift . return
join . lift . map lift = lift . join


Ко мне можно на ты

Edited at 2012-10-07 06:29 pm (UTC)

Пока что я не вижу, какое отношение MonadSum m n имеет к сумме в категории монад и морфизмов монад. И не уверен, что сумма всегда существует.

У нас есть морфизмы n => MonadSum n m и m => MonadSum n m, и при наличии n => t и m => t можем построить MonadSum n m => t

Точно так же можно представить Either:
data Either a b = Either {
  either :: forall c. (a -> c) -> (b -> c) -> c }


Или я несу чушь?

Чтобы доказать, что, например, liftL является морфизмом монад, надо иметь доказательство, что содержимое MonadSum m n a принимает только морфизмы монад, и взять его неоткуда. А без доказательств это просто кусок кода, который непонятно зачем нужен.

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

Ну в Haskell и instance Monad тоже не монада.
Что такое ССС?

Ну в Haskell и instance Monad тоже не монада.
Чего? Haskell, конечно, не требует доказательств, но люди обычно доказывают. А тех, кто не доказывает, осаживают.

Что такое ССС?
Cartesian closed category

> Чего? Haskell, конечно, не требует доказательств, но люди обычно доказывают. А тех, кто не доказывает, осаживают.
Ну т.е. это на совести людей, тут также. Хотя в Агде я могу потребовать именно морфизмов монад со всеми доказательствами.


Так как понимать «в Haskell instance Monad не монада»?

Monad m не гарантирует, что m - монада, в той же степени, что и (Monad m, Monad n) не гарантирует, что (forall a. m a -> n a) - морфизм монад.

> натуральные преобразования

Это ты зря. На русском так никто не говорит.
Правильно — "естественные преобразования".

  • 1