Я пытаюсь построить функцию типа:
liftSumthing :: ((a -> m b) -> m b) -> (a -> t m b) -> t m b
где t является монадным трансформатором. В частности, я заинтересован в этом:
liftSumthingIO :: MonadIO m => ((a -> IO b) -> IO b) -> (a -> m b) -> m b
Я возился с некоторыми Haskell wizardry libs, но безрезультатно. Как это получить? или, может быть, есть готовое решение где-то, чего я не нашел?
Это невозможно сделать в общем случае во всех экземплярах MonadIO из-за типа IO в отрицательной позиции. Есть несколько библиотек хака, которые делают это для конкретных экземпляров (monad-control, monad-peel), но были некоторые споры о том, являются ли они семантически обоснованными, особенно в отношении того, как они обрабатывают исключения и подобные странные вещи IO y.
Изменить: Некоторые люди, похоже, заинтересованы в различии позитивной/отрицательной позиции. На самом деле, нечего сказать (и вы, наверное, уже слышали это, но под другим именем). Терминология исходит из мира подтипов.
Интуиция, лежащая в основе подтипирования, заключается в том, что "a является подтипом b (который я напишу a <= b), когда a можно использовать везде, где вместо этого ожидался b". Решающий подтипирование во многих случаях прост; для продуктов (a1, a2) <= (b1, b2), когда a1 <= b1 и a2 <= b2, например, это очень простое правило. Но есть несколько сложных случаев; например, когда мы должны решить, что a1 -> a2 <= b1 -> b2?
Ну, мы имеем функцию f :: a1 -> a2 и контекст, ожидающий функцию типа b1 -> b2. Таким образом, контекст будет использовать возвращаемое значение f, как если бы оно было b2, поэтому мы должны потребовать, чтобы a2 <= b2. Трудность в том, что контекст будет поставлять f с помощью b1, хотя f будет использовать его, как если бы он был a1. Следовательно, мы должны требовать, чтобы b1 <= a1 - который оглядывается назад от того, что вы можете догадаться! Мы говорим, что a2 и b2 являются "ковариантными" или встречаются в "положительном положении", а a1 и b1 являются "контравариантными" или встречаются в "отрицательном положении".
(Быстро в сторону: почему "положительный" и "отрицательный"? Он мотивирован умножением. Рассмотрим эти два типа:
f1 :: ((a1 -> b1) -> c1) -> (d1 -> e1)
f2 :: ((a2 -> b2) -> c2) -> (d2 -> e2)
Когда тип f1 должен быть подтипом типа f2? Я излагаю эти факты (упражнение: проверьте это, используя правило выше):
e1 <= e2.d2 <= d1.c2 <= c1.b1 <= b2.a2 <= a1. e1 находится в положительном положении в d1 -> e1, который, в свою очередь, находится в положительном положении в типе f1; кроме того, e1 находится в положительном положении в типе f1 в целом (так как оно ковариантно, по приведенному выше факту). Его положение во всем члене является произведением его положения в каждом подтерм: положительное * положительное = положительное. Аналогично, d1 находится в отрицательном положении в d1 -> e1, который находится в положительном положении во всем типе. отрицательный * положительный = отрицательный, а переменные d действительно контравариантны. b1 находится в положительном положении в типе a1 -> b1, который находится в отрицательном положении в (a1 -> b1) -> c1, который находится в отрицательном положении во всем типе. положительный * отрицательный * отрицательный = положительный, и он ковариант. Вы получаете идею.)
Теперь рассмотрим класс MonadIO:
class Monad m => MonadIO m where
liftIO :: IO a -> m a
Мы можем рассматривать это как явное объявление подтипирования: мы даем способ сделать IO a подтипом m a для некоторого конкретного m. Сразу же мы знаем, что мы можем взять любое значение с конструкторами IO в положительных позициях и превратить их в m s. Но все: мы не можем превратить отрицательные конструкторы IO в m - для этого нам нужен более интересный класс.