haskell - GHC Haskellの現在の制約システムの何が問題になっていますか？

Question

GHC 7.6以下の時点で、Haskellの「壊れた」制約システムにいくつかの問題があると聞きました。どうしたの？それらの欠陥を克服する同等の既存のシステムはありますか？

たとえば、edwardkとtekmoの両方で問題が発生しました（たとえば、tekmoからのこのコメント）。

Answer 1

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.

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))、スタンドアロンの制約として使用できますが、型の新しい1パラメトリック*->*型クラスでエイリアス化することはできません。

これは、型クラス定義メカニズムが次のように機能するためです。

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

短所：を使用するたびに2番目のパラメーターを指定する必要がありますMonadPlus。

質問：どのように

instance Monoid a => MonadPlus Maybe a

MonadPlus1パラメトリック型クラスの場合に記述できますか？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）が発生し* -> * -> *ます。