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

所以哈斯克爾程序員必須解決這一缺陷的類型的系統通過定義一個單獨的類來處理這種特殊的情況下，多態。

但是，這並不總是一個可行的解決方案。例如，在我自己的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 
    ... 

...但你會希望限制一些kinded下派生類型構造函數：

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

然而，如果沒有多態的限制，該限制是不合法的。最近我一直抱怨這個問題，因爲我的pipes庫使用的類型非常多，所以我經常遇到這個問題。

有幾種人使用的數據類型的解決方法，但我還沒有時間來評估它們，以瞭解它們需要哪些擴展或哪些擴展正確解決了我的問題。更熟悉這個問題的人可能會提供一個單獨的答案，詳細解釋這個問題以及它爲什麼起作用。

Answer 2

[一個後續加布裏埃爾岡薩雷斯答案]

用於在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的類型：

<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（因爲我們只有在這裏排名-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或forall在LHS。

相反，我們需要寫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）-parametric類型類如果我們想要*類型，（7 - 2 * 1） - 參數etric typeclass爲* -> *類型，（7 - 2 * 0）爲* -> * -> *類型。