Поднятие функции высшего порядка в Хаскеле

Question

Я пытаюсь построить функцию типа:

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

Я возился с некоторыми волшебными библиотеками Хаскелла, но безрезультатно. Как я правильно понял, или, может быть, где-то есть готовое решение, которого я не нашел?

Answer 1

Это не может быть сделано в общем за все MonadIO случаи из-за IO введите отрицательную позицию. Есть некоторые библиотеки по взлому, которые делают это для определенных случаев ( monad-control, monad-peel), но были некоторые споры о том, являются ли они семантически правильными, особенно в отношении того, как они обрабатывают исключения и подобные странные IOу вещей.

Изменить: Некоторые люди, кажется, заинтересованы в различии положительной / отрицательной позиции. На самом деле, сказать особо нечего (и вы, наверное, уже слышали это, но под другим именем). Терминология происходит от мира подтипов.

Интуиция подтипов заключается в том, что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 конструкторы в положительных позициях и превращают их в ms. Но это все: у нас нет возможности стать отрицательным IO конструкторы в ms - нам нужен более интересный класс для этого.