我試圖表達一個給定的想法
instance (MonadTrans t, MonadX m) => MonadX (t m)
它應該遵循，只要有實體，任何t1 (t2 ... (tn m))也是。但是，當我嘗試將其寫下來時，它不起作用：MonadXtxMonadTrans
{-# LANGUAGE BasicallyEverything #-}
data Dict c where
Dict :: c => Dict c
class (forall m . Monad m => Monad (t m)) => MonadTrans t where
lift :: Monad m => m a -> t m a
class (c m, Monad m, forall t . (MonadTrans t, Monad (t m)) => c (t m)) => Foo c m
instance (c m, Monad m, forall t . (MonadTrans t, Monad (t m)) => c (t m)) => Foo c m
liftDict :: MonadTrans t => Dict (Foo c m) -> Dict (Foo c (t m))
liftDict Dict = Dict
這會導致以下錯誤：
? Could not deduce: c (t1 (t m)) arising from a use of ‘Dict’
from the context: MonadTrans t
bound by the type signature for:
liftDict :: forall (t :: (* -> *) -> * -> *)
(c :: (* -> *) -> Constraint) (m :: * -> *).
MonadTrans t =>
Dict (Foo c m) -> Dict (Foo c (t m))
at src/Lib.hs:85:1-64
or from: Foo c m
bound by a pattern with constructor:
Dict :: forall (a :: Constraint). a => Dict a,
in an equation for ‘liftDict’
at src/Lib.hs:86:10-13
or from: (MonadTrans t1, Monad (t1 (t m)))
bound by a quantified context at src/Lib.hs:1:1
? In the expression: Dict
In an equation for ‘liftDict’: liftDict Dict = Dict
? Relevant bindings include
liftDict :: Dict (Foo c m) -> Dict (Foo c (t m))
(bound at src/Lib.hs:86:1)
|
86 | liftDict Dict = Dict
有什么辦法讓它作業嗎？
uj5u.com熱心網友回復：
使用這里給出的稍微簡單的定義，您會得到完全相同的錯誤Foo c m：
(c m, Monad m, forall t. MonadTrans t => c (t m))
^^^ don't really need Monad (t m) here
讓我們澄清一些變數名稱，以便在撰寫時清楚哪些變數絕對相等，哪些不相等liftDict。
有：
MonadTrans t
forall m'. Monad m' => Monad (t m')
Foo c m
c m
Monad m
forall t'. MonadTrans t' => c (t' m)
想：
Foo c (t m)
c (t m)
Monad (t m)
forall t''. MonadTrans t'' => c (t'' (t m))
在“想要”類別中，c (t m)很容易——我們申請forall t'. MonadTrans t' => c (t' m)我們的t'~tand MonadTrans t。也很容易Monad (t m)，通過應用和。forall m'. Monad m' => Monad (t m')m'~mMonad m
但是最后一個......很棘手！您希望這些排列：
Have: forall t' . MonadTrans t' => c (t' m )
Want: forall t''. MonadTrans t'' => c (t'' (t m))
但他們并沒有完全排成一行。這里發生的m是一個固定的單子，而不是我們可以專門針對我們的新選擇的論點t m！好吧，讓我們把它作為一個論據。
class (c m, Monad m, forall m' t . (Monad m', MonadTrans t) => c (t m')) => Foo c m
instance (c m, Monad m, forall m' t . (Monad m', MonadTrans t) => c (t m')) => Foo c m
這編譯！但它不再說明我們想要什么，因為我們在這里所說的歸納步驟不需要c約束。幸運的是，我們可以重新添加它而不會導致它停止編譯：
class (c m, Monad m, forall m' t . (c m', Monad m', MonadTrans t) => c (t m')) => Foo c m
instance (c m, Monad m, forall m' t . (c m', Monad m', MonadTrans t) => c (t m')) => Foo c m
我認為您可能會發現將這些約束稍微不同地分組是很直觀的：
class ( (c m, Monad m) -- base case
, forall m' t. (c m', Monad m', MonadTrans t) => c (t m')
-- inductive hypothesis
) => Foo c m
但請注意：這Foo可能比您最初想象的要少。特別是，為了有一個Foo c實體，對于型別級應用程式，只能有一個完全通用的實體。c
轉載請註明出處，本文鏈接：https://www.uj5u.com/qukuanlian/423007.html
標籤：