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

Question

我听说Haskell的"破坏"约束系统存在一些问题,如GHC 7.6及以下版本.它出什么问题了？是否有可比的现有系统克服了这些缺陷？

例如,edwardk和tekmo都遇到了麻烦(例如来自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不会将其结果限制为a 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库使用的类型非常多,所以我经常遇到这个问题.

有一些使用数据类型的解决方法,有些人向我提出过​​,但我还没有时间对它们进行评估,以了解它们需要哪些扩展或哪一个正确地解决了我的问题.更熟悉这个问题的人可能会提供一个单独的答案,详细说明解决方案及其工作原理.

Answer 2

[Gabriel Gonzalez回答的后续行动]

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>
                    | ...

...

可以省略种类,以及forall排名1类型的s:

<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或foralllhs.

相反,我们需要编写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*1) - 参数类型* -> *类型和(7 - 2*0)* -> * -> *类型,则产生(7 - 2*2)- 参数类型类.