gpt4 book ai didi

haskell - 实例电感作为约束

转载 作者:行者123 更新时间:2023-12-04 18:11:18 25 4
gpt4 key购买 nike

我试图表达一个给定的想法

instance (MonadTrans t, MonadX m) => MonadX (t m)
应该遵循任何 t1 (t2 ... (tn m))也是 MonadX只要所有 txMonadTrans实例。但是,当我尝试将其写下来时,它不起作用:
{-# 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
有什么办法让它工作吗?

最佳答案

使用稍微简单的 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'~tMonadTrans 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是一个固定的单子(monad),而不是我们可以专门针对我们的新选择 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 实例用于类型级应用程序。

关于haskell - 实例电感作为约束,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/70853208/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com