Was stimmt nicht mit GHC Haskells aktuellem Constraint-System?

Question

Ich habe gehört, dass es einige Probleme mit Haskells "gebrochenem" Constraint-System gibt, ab GHC 7.6 und niedriger. Was stimmt damit nicht? Gibt es ein vergleichbares bestehendes System, das diese Mängel beseitigt?

Zum Beispiel sind sowohl edwardk als auch tekmo in Schwierigkeiten geraten (z. B. this comment from tekmo).

Answer 1

Ok, ich hatte mehrere Gespräche mit anderen Leuten, bevor ich hier gepostet habe, weil ich das richtig machen wollte. Sie alle zeigten mir, dass all die beschriebenen Probleme auf das Fehlen polymorpher Zwänge zurückzuführen sind.

Das einfachste Beispiel für dieses Problem ist die MonadPlus Klasse, wie folgt definiert:

class MonadPlus m where 
    mzero :: m a 
    mplus :: m a -> m a -> m a 

... mit den folgenden Gesetzen:

mzero `mplus` m = m 

m `mplus` mzero = m 

(m1 `mplus` m2) `mplus` m3 = m1 `mplus` (m2 `mplus` m3) 

Beachten Sie, dass diese die Monoid Gesetze, wo die Monoid Klasse ist gegeben durch:

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) 

Warum haben wir also die Klasse MonadPlus? Der Grund ist, weil Haskell uns vom Schreiben Zwängen der Form verbietet:

(forall a . Monoid (m a)) => ... 

So Haskell Programmierer um diese Fehler des Typs Systems arbeiten müssen eine separate Klasse durch die Definition dieses besonderen polymorphen Fall zu behandeln.

Dies ist jedoch nicht immer eine praktikable Lösung. Zum Beispiel in meiner eigenen Arbeit auf der pipes Bibliothek, die ich gestoßen häufig die Notwendigkeit, Einschränkungen der Form darstellen:

(forall a' a b' b . Monad (p a a' b' b m)) => ... 

Im Gegensatz zur MonadPlus Lösung, ich kann nicht leisten, die Monad Typklasse in eine andere Typklasse wechseln um das polymorphe Einschränkungsproblem zu umgehen, weil dann Benutzer meiner Bibliothek do Schreibweise verlieren würden, was einen hohen Preis zu zahlen ist.

Dies kommt auch beim Zusammensetzen von Transformatoren, Monadetransformatoren und den Proxytransformatoren, die ich in meine Bibliothek einbeziehe. Wir möchten etwas schreiben wie:

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 

Dieser erste Versuch nicht funktioniert, weil lift nicht beschränkt nicht das Ergebnis ein Monad zu sein. Wir würden tatsächlich brauchen:

class (forall m . Monad m => Monad (t m)) => MonadTrans t where 
    lift :: (Monad m) => m r -> t m r 

... aber Haskells Beschränkungssystem erlaubt das nicht.

Dieses Problem wird immer ausgeprägter, wenn Haskell-Benutzer zu Typenkonstruktoren höherer Typen wechseln. In der Regel haben Sie eine Typklasse des folgenden Formats:

class SomeClass someHigherKindedTypeConstructor where 
    ... 

...aber Sie werden etwas niedriger kinded abgeleitet Typkonstruktor einschränken wollen:

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

jedoch ohne polymorphe Einschränkungen, dass Zwang nicht legal ist. Ich habe mich zuletzt über dieses Problem beschwert, weil meine pipes Bibliothek Arten sehr hoher Arten verwendet, also laufe ich ständig auf dieses Problem.

Es gibt Problemumgehungen mit Datentypen, die mir mehrere Leute vorgeschlagen haben, aber ich hatte (noch) nicht die Zeit, sie zu bewerten, um zu verstehen, welche Erweiterungen sie benötigen oder welche mein Problem richtig löst. Jemand, der mit diesem Thema vertrauter ist, könnte vielleicht eine separate Antwort geben, die die Lösung dafür und warum es funktioniert.

Answer 2

[ein Follow-up zu Gabriel Gonzalez Antwort]

Die richtige Schreibweise für Zwänge und Quantifizierungen in Haskell ist folgende:

<functions-definition> ::= <functions> :: <quantified-type-expression> 

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

<type-expression> ::= <type-expression> -> <quantified-type-expression> 
        | ... 

... 

Kinds entfallen, sowie forall s werden für Rang-1-Typen:

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

zum Beispiel:

{-# 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 

oder ohne Rank2Types (da wir nur Rang-1-Typen hier haben), und mit 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 

Das "Problem" ist, dass wir nicht

schreiben

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

oder

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

Das heißt, forall m a. (Monad m, Monoid (m a)) kann als eigenständige Integritätsbedingung verwendet werden, kann aber nicht mit einer neuen einparametrigen Typenklasse für *->* Typen aliasiert werden. Diese

ist, weil der Mechanismus wie defintion typeclass dies funktioniert:

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

das heißt die rhs Seitentyp Variablen einführen, nicht auf die linke Skala oder forall an den lhs.

Stattdessen brauchen wir 2-parametrischen typeclass schreiben:

{-# 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 

Nachteile: wir zweite Parameter verwenden, jedes Mal wenn wir MonadPlus angeben müssen.

Frage: wie

instance Monoid a => MonadPlus Maybe a 

wenn MonadPlus geschrieben werden kann, ist ein parametrischer typeclass?MonadPlus Maybe von base:

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

arbeitet Monoid Maybe nicht mag:

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] 

---

analogisch, forall m a b n c d e. (Foo (m a b), Bar (n c d) e) gibt Anlass für (7-2 * 2) -parametric typeclass wenn wir * Typen wollen, (7 - 2 * 1) -Param etric typeclass für * -> * Typen und (7 - 2 * 0) für * -> * -> * Typen.