haskell - GHC Haskell 当前的约束系统有什么问题？

Question

我听说 Haskell 的“损坏”约束系统存在一些问题，从 GHC 7.6 及以下版本开始。它出什么问题了？是否有一个可比的现有系统可以克服这些缺陷？

例如，edwardk 和 tekmo 都遇到了麻烦(例如 this comment from tekmo )。

Answer 1

好吧，在发帖之前我和其他人进行了几次讨论，因为我想把这个问题做好。他们都向我表明，我所描述的所有问题都可以归结为缺乏多态约束。

这个问题最简单的例子是 MonadPlus 类，定义为:

class MonadPlus m where
    mzero :: m a
    mplus :: m a -> m a -> m a

...遵循以下法律:

mzero `mplus` m = m

m `mplus` mzero = m

(m1 `mplus` m2) `mplus` m3 = m1 `mplus` (m2 `mplus` m3)

请注意，这些是 Monoid 法则，其中 Monoid 类由以下公式给出:

class Monoid a where
    mempty :: a
    mappend :: a -> a -> a

mempty `mplus` a = a

a `mplus` mempty = a

(a1 `mplus` a2) `mplus` a3 = a1 `mplus` (a2 `mplus` a3)

那么为什么我们还要有 MonadPlus 类呢？原因是因为 Haskell 禁止我们编写以下形式的约束:

(forall a . Monoid (m a)) => ...

因此，Haskell 程序员必须通过定义一个单独的类来处理这种特定的多态情况来解决类型系统的这一缺陷。

但是，这并不总是可行的解决方案。例如，在我自己的 pipes 库工作中，我经常遇到需要提出以下形式的约束:

(forall a' a b' b . Monad (p a a' b' b m)) => ...

与 MonadPlus 解决方案不同，我无法将 Monad 类型类切换到不同的类型类来解决多态约束问题，因为这样我的库的用户就会失去 do 表示法，这是一个高昂的代价。

在编写变压器(包括 monad 变压器和我库中包含的代理变压器)时也会出现这种情况。我们想写这样的内容:

data Compose t1 t2 m r = C (t1 (t2 m) r)

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

第一次尝试不起作用，因为 lift 并未将其结果限制为 Monad。我们实际上需要:

class (forall m . Monad m => Monad (t m)) => MonadTrans t where
    lift :: (Monad m) => m r -> t m r

...但 Haskell 的约束系统不允许这样做。

随着 Haskell 用户转向更高类型的类型构造函数，这个问题将变得越来越明显。您通常会拥有以下形式的类型类:

class SomeClass someHigherKindedTypeConstructor where
    ...

...但是您需要约束一些较低种类的派生类型构造函数:

class (SomeConstraint (someHigherKindedTypeConstructor a b c))
    => SomeClass someHigherKindedTypeConstructor where
    ...

但是，如果没有多态约束，该约束是不合法的。我是最近提示这个问题的人，因为我的 pipes 库使用非常高级的类型，所以我不断遇到这个问题。

有几个人向我建议的使用数据类型的解决方法，但我(还)没有时间评估它们以了解它们需要哪些扩展或哪个扩展可以正确解决我的问题。更熟悉这个问题的人也许可以提供一个单独的答案，详细说明该问题的解决方案及其工作原理。