GHC Haskell目前的约束系统有什么问题？ [英] What's wrong with GHC Haskell's current constraint system?
问题描述
例如，edwardk和tekmo都遇到了麻烦（例如来自tekmo的评论）。 解决方案
好的，在发布之前我与其他人进行了几次讨论，因为我希望得到这个结果。他们都告诉我，我所描述的所有问题归结为缺乏多态限制。
这个问题最简单的例子是 MonadPlus class，定义为：
class MonadPlus m其中
mzero :: ma
mplus :: ma - > m a - > ma
...符合以下法律：
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禁止我们写出形式的约束：
pre $ （forall a。Monoid（m a））=> ...
因此，Haskell程序员必须通过定义一个单独的类来解决类型系统的这个缺陷处理这个特殊的多态情况。
然而，这并不总是一个可行的解决方案。例如，在我自己对 pipes 库的工作中，我经常遇到需要对表单进行约束：
（a'a b'b。Monad（pa a'b'bm））=> ...
与 MonadPlus 解决方案不同，我不能将 Monad 类型类切换到不同的类型类以解决多态约束问题，因为那样我的库的用户将会失去 do 符号，这是一个很高的支付价格。
这也出现在编写变形金刚时，包括monad变形金刚和代理变形金刚图书馆。我们希望写下如下内容：
data构成t1 t2 mr = C（t1（t2 m）r）
实例（MonadTrans t1，MonadTrans t2）=> MonadTrans（撰写t1 t2）其中
lift = C。电梯 。提升
第一次尝试不起作用，因为 lift 不会将其结果限制为 Monad 。我们实际上需要：
pre> class（forall m。Monad m => Monad（t m））=> MonadTrans t其中
lift ::（Monad m）=> m r - > tmr
...但Haskell的约束系统不允许。
随着Haskell用户继续输入更高类型的构造函数，这个问题会变得越来越明显。您通常会拥有以下形式的类型：
class SomeClass someHigherKindedTypeConstructor其中
...
...但是您会想限制一些较低派生的派生类型构造函数：
class（SomeConstraint（someHigherKindedTypeConstructor abc））
=> SomeClass someHigherKindedTypeConstructor其中
...
但是，没有多态约束，该约束是不合法的。最近我一直抱怨这个问题，因为我的 pipes 库使用了很高类型的类型，所以我经常遇到这个问题。
使用几种人提出的数据类型有一些解决方法，但我还没有时间来评估它们以了解它们需要哪些扩展或哪些解决了我的问题正确。有人更熟悉这个问题可能会提供一个单独的答案，详细解释这个问题的解决方案，以及它为什么有效。
I've heard that there are some problems with Haskell's "broken" constraint system, as of GHC 7.6 and below. What's "wrong" with it? Is there a comparable existing system that overcomes those flaws?
For example, both edwardk and tekmo have run into trouble (e.g. this comment from tekmo).
Ok, I had several discussions with other people before posting here because I wanted to get this right. They all showed me that all the problems I described boil down to the lack of polymorphic constraints.
The simplest example of this problem is the MonadPlus class, defined as:
class MonadPlus m where
mzero :: m a
mplus :: m a -> m a -> m a
... with the following laws:
mzero `mplus` m = m
m `mplus` mzero = m
(m1 `mplus` m2) `mplus` m3 = m1 `mplus` (m2 `mplus` m3)
Notice that these are the Monoid laws, where the Monoid class is given by:
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)
So why do we even have the MonadPlus class? The reason is because Haskell forbids us from writing constraints of the form:
(forall a . Monoid (m a)) => ...
So Haskell programmers must work around this flaw of the type system by defining a separate class to handle this particular polymorphic case.
However, this isn't always a viable solution. For example, in my own work on the pipes library, I frequently encountered the need to pose constraints of the form:
(forall a' a b' b . Monad (p a a' b' b m)) => ...
Unlike the MonadPlus solution, I cannot afford to switch the Monad type class to a different type class to get around the polymorphic constraint problem because then users of my library would lose do notation, which is a high price to pay.
This also comes up when composing transformers, both monad transformers and the proxy transformers I include in my library. We'd like to write something like:
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
This first attempt doesn't work because lift does not constrain its result to be a Monad. We'd actually need:
class (forall m . Monad m => Monad (t m)) => MonadTrans t where
lift :: (Monad m) => m r -> t m r
... but Haskell's constraint system does not permit that.
This problem will grow more and more pronounced as Haskell users move on to type constructors of higher kinds. You will typically have a type class of the form:
class SomeClass someHigherKindedTypeConstructor where
...
... but you will want to constrain some lower-kinded derived type constructor:
class (SomeConstraint (someHigherKindedTypeConstructor a b c))
=> SomeClass someHigherKindedTypeConstructor where
...
However, without polymorphic constraints, that constraint is not legal. I've been the one complaining about this problem the most recently because my pipes library uses types of very high kinds, so I run into this problem constantly.
There are workarounds using data types that several people have proposed to me, but I haven't (yet) had the time to evaluate them to understand which extensions they require or which one solves my problem correctly. Somebody more familiar with this issue could perhaps provide a separate answer detailing the solution to this and why it works.
这篇关于GHC Haskell目前的约束系统有什么问题？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
