GHC Haskell目前的约束系统有什么问题?



我听说 Haskell 的"破碎"约束系统存在一些问题,从 GHC 7.6 及更低版本开始。它有什么"问题"?是否有一个类似的现有系统可以克服这些缺陷?

例如,edwardk和tekmo都遇到了麻烦(例如tekmo的这条评论)。

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

此问题的最简单示例是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用户转向更高种类的类型构造函数,这个问题将变得越来越明显。 您通常具有以下形式的类型类:

class SomeClass someHigherKindedTypeConstructor where
...

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

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

但是,如果没有多态约束,该约束是不合法的。 我最近一直在抱怨这个问题,因为我的pipes库使用非常高的类型,所以我经常遇到这个问题。

有几个人向我提出了使用数据类型的解决方法,但我(还)没有时间评估它们以了解它们需要哪些扩展或哪个扩展可以正确解决我的问题。 更熟悉这个问题的人也许可以提供单独的答案,详细说明这个问题的解决方案以及它为什么有效。

[加布里埃尔·冈萨雷斯回答的后续]

Haskell中约束和量化的正确表示法如下:

<functions-definition> ::= <functions> :: <quantified-type-expression>
<quantified-type-expression> ::= forall <type-variables-with-kinds> . (<constraints>) => <type-expression>
<type-expression> ::= <type-expression> -> <quantified-type-expression>
| ...
...

可以省略种类,也可以省略等级 1 类型的forall

<simply-quantified-type-expression> ::= (<constraints-that-uses-rank-1-type-variables>) => <type-expression>

例如:

{-# LANGUAGE Rank2Types #-}
msum :: forall m a. Monoid (m a) => [m a] -> m a
msum = mconcat
mfilter :: forall m a. (Monad m, Monoid (m a)) => (a -> Bool) -> m a -> m a
mfilter p ma = do { a <- ma; if p a then return a else mempty }
guard :: forall m. (Monad m, Monoid (m ())) => Bool -> m ()
guard True = return ()
guard False = mempty

或者没有Rank2Types(因为我们这里只有 rank-1 类型),并使用CPP(J4F):

{-# LANGUAGE CPP #-}
#define MonadPlus(m, a) (Monad m, Monoid (m a))
msum :: MonadPlus(m, a) => [m a] -> m a
msum = mconcat
mfilter :: MonadPlus(m, a) => (a -> Bool) -> m a -> m a
mfilter p ma = do { a <- ma; if p a then return a else mempty }
guard :: MonadPlus(m, ()) => Bool -> m ()
guard True = return ()
guard False = mempty

"问题"是我们不能写

class (Monad m, Monoid (m a)) => MonadPlus m where
...

class forall m a. (Monad m, Monoid (m a)) => MonadPlus m where
...

也就是说,forall m a. (Monad m, Monoid (m a))可以用作独立约束,但不能使用*->*类型的新单参数类型类进行别名。

这是因为类型类定义机制的工作方式如下:

class (constraints[a, b, c, d, e, ...]) => ClassName (a b c) (d e) ...

RHS端引入类型变量,而不是 LHS 的 LHS 或forall

相反,我们需要编写 2 参数类型类:

{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
class (Monad m, Monoid (m a)) => MonadPlus m a where
mzero :: m a
mzero = mempty
mplus :: m a -> m a -> m a
mplus = mappend
instance MonadPlus [] a
instance Monoid a => MonadPlus Maybe a
msum :: MonadPlus m a => [m a] -> m a
msum = mconcat
mfilter :: MonadPlus m a => (a -> Bool) -> m a -> m a
mfilter p ma = do { a <- ma; if p a then return a else mzero }
guard :: MonadPlus m () => Bool -> m ()
guard True = return ()
guard False = mzero

缺点:每次使用MonadPlus时都需要指定第二个参数。

问题:如何

instance Monoid a => MonadPlus Maybe a

如果MonadPlus是一个参数类型类,可以写吗?MonadPlus Maybe来自base

instance MonadPlus Maybe where
mzero = Nothing
Nothing `mplus` ys  = ys
xs      `mplus` _ys = xs

作品不像Monoid Maybe

instance Monoid a => Monoid (Maybe a) where
mempty = Nothing
Nothing `mappend` m = m
m `mappend` Nothing = m
Just m1 `mappend` Just m2 = Just (m1 `mappend` m2) -- < here

(Just [1,2] `mplus` Just [3,4]) `mplus` Just [5,6] => Just [1,2]
(Just [1,2] `mappend` Just [3,4]) `mappend` Just [5,6] => Just [1,2,3,4,5,6]
类似地,如果我们想要*类型,forall m a b n c d e. (Foo (m a b), Bar (n c d) e)会产生 (7 - 2 * 2)-参数类型类,* -> *类型会产生 (7 - 2 *

1)-参数类型类,* -> * -> *类型会产生 (7 - 2 * 0)。

最新更新