Precomposing монада трансформаторов

Question

Предположим, что у меня есть два монада трансформаторов

T1 :: (* -> *) -> * -> * 
T2 :: (* -> *) -> * -> * 

с экземплярами

instance MonadTrans T1 
instance MonadTrans T2 

и некоторые

X :: (((* -> *) -> * -> *) -> ((* -> *) -> * -> *) -> * -> *) 

, такие как

newtype X t1 t2 a b = X { x :: t1 (t2 a) b } 

, для которых я хотел бы определить что-то вдоль линий

instance (MonadTrans t1, MonadTrans t2) => MonadTrans (X t1 t2) where 
    lift = X . lift . lift 

так что я могу использовать lift поднять m a в X T1 T2 m a?

Проблема здесь заключается в том, что lift s действуют на какую-нибудь монаду Monad m => m a, которую я не могу гарантировать, что вы будете производить промежуточные шаги. Но это меня сбивает с толку. Я предоставляю реализацию lift, поэтому могу предположить, что у меня есть Monad m => m a, поэтому я применяю крайний правый lift и получаю T1 m a, о котором я ничего не знаю, но не следует ли подразумевать, что T1 m - это Monad? Если нет, то почему я не могу просто добавить это к ограничению моего экземпляра

instance (MonadTrans t1 
     , MonadTrans t2 
     , Monad (t2 m)) => MonadTrans (X t1 t2) where ... 

Это также не работает. У меня есть интуиция, что вышеизложенным я говорю «должен ли быть t1, t2, m такой, что ...», который слишком слаб, чтобы доказать, что X t1 t2 является трансформатором (работает для любых/всех Monad m). Но для меня это все еще не имеет большого значения, может ли действующий трансформатор монады создать не монаду при применении к монаде? Если нет, я должен уйти с экземпляром MonadTrans (X t1 t2).

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

бы импликация соответствует ничего, кроме

instance (MonadTrans t, Monad m) => Monad (t m) where 
    return = lift . return 
    a >>= b = ... # no sensible generic implementation 

которая перекрывает другие экземпляры/не может предоставить конкретную привязку? Не может ли это работать с некоторой косвенностью? Изготовление returnT :: Monad m => a -> t m a и bindT :: Monad m => t m a -> (a -> t m b) -> t m b части MonadTrans, чтобы можно было потом написать

instance MonadTrans (StateT s) where 
    lift = ... 
    returnT = ... 
    bindT = ... 

... 

instance (MonadTrans t, Monad m) => Monad (t m) where 
    return = returnT 
    a >>= b = a `bindT` b 

Такого рода случаи в настоящее время не действует из-за перекрывание, что они тем не менее быть целесообразными, полезными?

Answer 1

[C] действительный трансформатор монады производит немонад при применении к монаде?

№. Модифицированный трансформатор - это конструктор типа t :: (* -> *) -> (* -> *), который берет монаду как аргумент и производит новую монаду.

В то время как я хотел бы видеть его более явно, the transformers documentation действительно говорит, «Монада трансформатор делает новую монаду из существующей монады», и это подразумевается the MonadTrans laws:

lift . return = return 
lift (m >>= f) = lift m >>= (lift . f) 

Очевидно эти законы только имеет смысл, если lift m действительно является монадическим вычислением. Как вы отметили в комментариях, все ставки отключены, если у нас есть неправомерные инстанции, с которыми можно бороться. Это Хаскелл, а не Идрис, поэтому мы привыкли вежливо просить законы удовлетворять, используя документацию, вместо того, чтобы требовать их силой, используя типы.

Более «современный» MonadTrans может потребовать явного доказательства того, что t m является монадой, когда m есть. Здесь я использую the "entailment" operator :- от Kmett's constraints library сказать, что Monad m подразумевает Monad (t m): (. Это более или менее та же идея, что @MigMit разработал в своем ответе, но с использованием внедорожных готовых компонентов)

class MonadTrans t where 
    transform :: Monad m :- Monad (t m) 
    lift :: Monad m => m a -> t m a 

Почему нет MonadTrans в transformers, есть элемент transform? Когда было написано, GHC не поддержал оператора :- (расширение ConstraintKinds не было изобретено). В мире много и много кода, который зависит от MonadTrans без transform, поэтому мы не можем вернуться назад и добавить его без a really good reason, и на практике метод transform на самом деле не покупает вас.

Answer 2

Прежде всего: вы хотите невозможно. Вы правильно определили проблему: даже если m является монадой, а t - трансформатор, никто не гарантирует, что t m будет монадой.

С другой стороны, это обычно есть. Но, по крайней мере, теоретически - не всегда, так что вам придется как-то отмечать случаи, когда это так. Это означает, что он маркирует его экземпляром другого типа, который вам нужно будет определить самостоятельно. Давайте посмотрим, как это работает.

Начнем с названия для нашего нового класса:

class MonadTrans t => MonadTransComposeable t where 

Теперь where что? Мы хотим создать экземпляр Monad (t m). К сожалению, это не то, что мы можем сделать. Экземпляры класса, будучи просто данными, не считаются такими же данными, как и все остальное; мы не можем создать функцию, которая их генерирует. Итак, мы должны как-то обойти это. Но если у нас есть такая вещь, то класс довольно просто

class MonadTrans t => MonadTransComposeable t where 
    transformedInstance :: Monad m => MonadInstance (t m) 

Давайте определим MonadInstance Теперь. Мы хотим убедиться, что если есть MonadInstance n, то n является монадой. GADT s прийти на помощь:

data MonadInstance n where MonadInstance :: Monad n => MonadInstance n 

Обратите внимание, что MonadInstance конструктор имеет контекст, который гарантирует, что мы не можем сделать MonadInstance n без n будучи Monad.

Мы можем определить экземпляры MonadTransComposeable Сейчас:

instance MonadTransComposeable (StateT s) where 
    transformedInstance = MonadInstance 

Она будет работать, так как она уже установлена ​​в transformers пакете, что всякий раз, когда m монада, StateT m является монада тоже. Поэтому конструктор MonadInstance имеет смысл.

Теперь мы можем составить MonadTrans и MonadTransComposeable. Использование вашего собственного определения

newtype X t1 (t2 :: (* -> *) -> (* -> *)) m a = X { x :: t1 (t2 m) a } 

мы можем определить экземпляр. Теперь мы можем доказать, что t2 m является монадой; это не автоматический, и мы должны сказать, Haskell, которые transformedInstance использовать, но это не трудно:

instance (MonadTrans t1, MonadTransComposeable t2) => MonadTrans (X t1 t2) where 
    lift :: forall m a. (Monad m) => m a -> X t1 t2 m a 
    lift ma = 
    case transformedInstance :: MonadInstance (t2 m) of 
     MonadInstance -> X (lift (lift ma)) 

---

Теперь, давайте делать что-то весело. Давайте расскажем Haskell, что когда t1 и t2 являются «хорошими» (составными) монадными трансформаторами, X t1 t2 тоже.

Как и раньше, это довольно легко:

instance (MonadTransComposeable t1, MonadTransComposeable t2) => MonadTransComposeable (X t1 t2) where 
    transformedInstance = MonadInstance 

То же самое с StateT. Уловка заключается в том, что теперь Хаскелл будет жаловаться, что он не может знать, действительно ли X t1 t2 m является монадой. Что справедливо - мы не определили экземпляр. Давайте сделаем это.

Мы будем использовать тот факт, что t1 (t2 m) является монадой. Таким образом, мы делаем это явно:

transformedInstance2 :: forall t1 t2 m. (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => MonadInstance (t1 (t2 m)) 
transformedInstance2 = 
    case transformedInstance :: MonadInstance (t2 m) of 
    MonadInstance -> transformedInstance 

Теперь мы определим Monad (X t1 t2 m) экземпляр.Из-за глупого решения сделать Monad подкласс Applicative, мы не можем сделать это в одном заявлении, но должны пройти через Functor и Applicative, но это не трудно:

instance (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => Functor (X t1 t2 m) where 
    fmap h (X ttm) = 
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of 
     MonadInstance -> X (fmap h ttm) 

instance (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => Applicative (X t1 t2 m) where 
    pure a = 
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of 
     MonadInstance -> X (pure a) 
    (X ttf) <*> (X tta) = 
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of 
     MonadInstance -> X (ttf <*> tta) 

и, наконец,

instance (MonadTransComposeable t1, MonadTransComposeable t2, Monad m) => Monad (X t1 t2 m) where 
    X tta >>= f = 
    case transformedInstance2 :: MonadInstance (t1 (t2 m)) of 
     MonadInstance -> X (tta >>= \a -> case f a of X ttb -> ttb) 

Answer 3

Существует хорошо известная теория, в которой говорится, что монады обычно не являются композиционными. То есть, учитывая любые две произвольных монады, t и u нет никакой гарантии, что tu ○ монады, где (t ○ u) a = t (u a). Это, по-видимому, является конечной причиной того, что эта прекомпозиция недоступна.

Рациональное простое. Во-первых, обратите внимание, что любая монада может быть записана как преобразование тождественной монады. Затем любые две монады могут быть переведены в форму X. Это соответствует их составу, что обычно не допускается, поэтому мы знаем, что X обычно не допускается.

Id Пусть тождественный монада,

newtype Id a = Id a 

и пусть состав будет дано:

newtype t ○ u a = Comp (t (u a)) 

пусть Кроме того, для любой монады t, композиция с Id равно t.

t ○ Id ~ t ~ Id ○ t 

Затем мы исследуем случай X t u m a, где tu представляют собой композиции с Id. Тип и конструкция определяются

X (t ○) (Id ○ (u ○)) (Id ○ m) a 
    = X ((t ○) (Id ○ (u ○ (Id ○ m)) a) 

И конструктор РИТ эквивалентно

~ X ((t ○) (u ○ m) a) 

который имеет тип

X (t ○) (u ○) m a 

И поэтому частичное применение X (t ○) (u ○) соответствует составу любые две монады, которые не допускаются.

Все это не означает, что мы не можем сочинять монады, а скорее объяснять, почему нам нужны такие методы, как transform или MonadTransComposable от Бенджамина Ходжсона и МигМит соответственно.

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