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對一些monad 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）。但是對我來說，這仍然沒有什麼意義，一個有效的monad變壓器在應用於monad時能產生一個非monad嗎？如果不是，我應該能夠脫離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和MonadTransbindT :: Monad m => t m a -> (a -> t m b) -> t m b一部分，這樣可以再寫入

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]一個有效的monad變換器在應用於monad時產生非monad？

不是。單子變壓器是一種類型構造函數t :: (* -> *) -> (* -> *)，它將monad作爲參數併產生新的monad。

雖然我希望看到更明確地說，the transformers documentation不說「一個單子轉換，使一個新的單子了現有的單子」，而它是由the MonadTrans laws暗示：

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

顯然，這些法律只有在lift m確實是一個單子計算時纔有意義。正如你在評論中指出的那樣，如果我們有非合法的實例需要與之抗衡，那麼所有的投注都將失效。這是哈斯克爾而不是伊德里斯，所以我們習慣於禮貌地要求使用文檔來滿足法律要求，而不是強制要求使用類型。

一個更「現代」的MonadTrans可能需要明確的證據，t m是一個monad只要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是一個monad，並且t - 一個變壓器，沒有人保證t m是monad。

另一方面，它通常是。但是 - 至少在理論上 - 並不總是如此，所以，你必須以某種方式標記出現的時機。這意味着用另一個類型類型的實例來標記它，你必須自己定義它。讓我們看看它是如何工作的。

我們將用一個名字開始爲我們的新類：

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是monad。 GADT也走到救援：

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

注意，MonadInstance構造有一個背景，這保證了我們不能沒有n是一個Monad使MonadInstance n。

我們現在可以定義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是一個monad;它不是自動的，我們要告訴哈斯克爾使用哪個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是「好」（可組合的）monad變換器，X t1 t2也是。

和以前一樣，它很容易：

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

同與StateT。問題在於，現在Haskell會抱怨說它不知道X t1 t2 m是否真的是單子。這是公平的 - 我們沒有定義一個實例。讓我們這樣做。

我們將使用t1 (t2 m)是monad的事實。所以，我們做這個明確的：

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

有一個衆所周知的理論說monad一般不是可組合的。也就是說，給定任意兩個單子，t，和u沒有保證t ○ u是一個單子，其中（t ○ u）a = t (u a)。這似乎是這種預合成不可用的最終原因。

理性很簡單。首先，請注意，任何monad都可以寫成身份monad的變換。然後，任何兩個單子可以翻譯成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) 

給出的RHS的構造等同於

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

其中有

X (t ○) (u ○) m a 

這樣一來，部分應用程序X (t ○) (u ○)對應的組合物的類型任何兩個單子，這是不允許的。

這一切都不是說我們不能構成單子，而是解釋爲什麼我們需要分別來自Benjamin Hodgson和MigMit的方法transform或MonadTransComposable。

我已經使這個社區wiki成爲社區維基，正如我期望的那樣，快速而寬鬆的證明可以被那些真正知道他們在做什麼的人大大提高。