Почему `hoist` ограничивает параметр типа этой монады?

Question

У меня есть функция, которая сочиняет две монады:

comp :: Monad m => m a -> m b -> m b 

И два экземпляра таких монад, где на есть «внутри» Mfunctor,

ms :: Monad m => m String 
ms = undefined 

tma :: (Monad m, MFunctor t) => t m a 
tma = undefined 

Теперь, если я пытаюсь составить ms с tma :

tmas = hoist (\ma -> comp ma ms) tma 

Я получаю эту ошибку:

Could not deduce (a ~ [Char]) 
    from the context (Monad m, MFunctor t) 
     bound by the inferred type of 
       comp :: (Monad m, MFunctor t) => t m b 
     at Coroutine.hs:607:1-40 
     `a' is a rigid type variable bound by 
      a type expected by the context: m a -> m a at Coroutine.hs:607:8 
    Expected type: m a 
     Actual type: m String 

в котором говорится, что a в ms должен быть произвольного типа: ms :: Monad m => m a.

Почему это и есть способ составить tma с монадами определенных параметров.

Я могу видеть, что подпись тали:

hoist :: (Monad m, MFunctor t) => (forall a. m a -> n a) -> t m b -> t n b 

, но не могу представить, как forall влияет на то, что я пытаюсь сделать, если это имеет какой-либо эффект.

Answer 1

Переключите порядок аргументов comp так:

tmas = hoist (\ma -> comp ms ma) tma 

-- or more simply: 
tmas = hoist (comp ms) tma 

причина в том, что тип comp является:

comp :: (Monad m) => m a -> m b -> m b 

Если вы установили, ms в качестве второго аргумента, то b типа провер как String и вы получите:

(`comp` ms) :: (Monad m) => m a -> m String 

...но если вы установите ms в качестве первого аргумента, то a типа провер как String вы получите:

(ms `comp`) :: (Monad m) => m b -> m b 

Этот последний тип является правильным типом для hoist поскольку b является квантор всеобщности (т.е. «FORALL» под ред) ,

Чтобы ответить на вопрос о правильности, ответ заключается в том, что универсальное квантификация гарантирует, что аргумент hoist изменяет только уровень монады, а не возвращаемое значение монады. Однако, если вы намерены изменить возвращаемое значение, то hoist не то, что вы хотите.

Answer 2

Тип hoist говорит, что он ожидает функцию (forall a. m a -> n a) т. Е. Функцию, которая изменяет тип «контейнер», но сохраняет параметр типа тот же. Здесь forall означает, что предоставленная вами функция не может быть специализирована для каких-либо конкретных a, но должна работать для любого параметра типа.

Функция вы пытаетесь использовать (\ma -> comp ma ms) имеет тип m a -> m String так это в значительной степени противоположно тому, что hoist предпологает, так как он держит контейнер (m) то же, но изменяет параметр типа (от a до String) ,

Я думаю, что вы на самом деле ищут вместо hoist в этом случае функция, которая поднимает одноместную функцию, чтобы работать на трансформированных монады, поэтому вместо MFunctor вы хотите что-то вроде:

import Control.Monad.Trans.Class 

tmas :: (Monad m, Monad (t m), MonadTrans t) => t m String 
tmas = transLift (\ma -> comp ma ms) tma 

transLift :: (Monad m, Monad (t m), MonadTrans t) => (m a -> m b) -> t m a -> t m b 
transLift f tma = tma >>= lift . f . return