Quel est le problème avec GHC Haskell actuelle du système de contraintes?

Question

J'ai entendu dire qu'il y a quelques problèmes avec Haskell "cassé" système de contraintes, comme de GHC 7.6 et ci-dessous. Ce qui est "mal" avec elle? Est-il comparable au système existant qui permet de surmonter ces défauts?

Par exemple, les deux edwardk et tekmo ont en difficulté (par exemple, ce commentaire de tekmo).

Answer 1

Ok, j'ai eu plusieurs discussions avec d'autres personnes avant de poster ici parce que je voulais obtenir ce droit. Ils ont tous m'ont montré que tous les problèmes que j'ai décrit se résument au manque de polymorphe contraintes.

L'exemple le plus simple de ce problème est l' MonadPlus classe, définie comme suit:

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

... avec les lois suivantes:

mzero `mplus` m = m

m `mplus` mzero = m

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

A noter que ce sont les Monoid lois, où l' Monoid classe est donnée par:

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)

Alors, pourquoi avons-nous même l' MonadPlus classe? La raison en est que Haskell nous interdit de contraintes d'écriture de la forme:

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

Donc, Haskell programmeurs doivent travailler autour de cette faille dans le système de type par la définition d'une catégorie distincte pour gérer ce polymorphes cas.

Cependant, ce n'est pas toujours une solution viable. Par exemple, dans mon propre travail sur l' pipes bibliothèque, j'ai souvent rencontré le besoin de poser des contraintes de la forme:

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

Contrairement à l' MonadPlus solution, je ne peut pas se permettre de basculer l' Monad classe de type vers un autre type de classe pour obtenir autour de la polymorphes contrainte de problème parce que les utilisateurs de ma bibliothèque perdrait do de la notation, qui est un prix élevé à payer.

Cela vient aussi en place lors de la composition de transformateurs, les deux monade transformateurs et le proxy transformateurs-je inclure dans ma bibliothèque. Nous aimerions écrire quelque chose comme:

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

Cette première tentative ne fonctionne pas parce qu' lift ne pas nuire à son résultat à un Monad. Nous avions besoin de:

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

... mais Haskell contrainte du système ne le permet pas.

Ce problème va devenir de plus en plus prononcé comme Haskell les utilisateurs se déplacent sur le type des constructeurs de la hausse des genres. Vous aurez généralement un type de classe de la forme:

class SomeClass someHigherKindedTypeConstructor where
    ...

... mais vous souhaitez limiter certains bas-kinded dérivés de type constructeur:

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

Cependant, sans polymorphes contraintes, cette contrainte n'est pas légal. J'ai été le seul à se plaindre à propos de ce problème, le plus récemment parce que mes pipes bibliothèque utilise les types de très haute sortes, de sorte que je rencontre ce problème en permanence.

Il existe des solutions de contournement à l'aide de types de données que plusieurs personnes se sont proposées pour moi, mais je n'ai pas (encore) eu le temps de les évaluer à comprendre ce qui les extensions dont elle a besoin ou dont on résout mon problème correctement. Quelqu'un de plus familier avec ce problème pourrait peut-être fournir une réponse distincte détaillant la solution à ce problème et pourquoi il fonctionne.

Answer 2

[suivi de Gabriel Gonzalez répondre]

Le droit de notation pour les contraintes et les quantifications en Haskell est la suivante:

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

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

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

...

Les genres peuvent être omis, ainsi que foralls pour le rang-1 types:

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

Par exemple:

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

ou sans Rank2Types (puisque nous n'avons que de rang 1 types ici), et à l'aide de 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

Le "problème" est que nous ne pouvons pas écrire

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

ou

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

C'est, forall m a. (Monad m, Monoid (m a)) peut être utilisé comme une application autonome contrainte, mais ne peut pas être lissés avec un nouveau-paramétrique typeclass pour *->* types.

C'est parce que le typeclass définition mécanisme fonctionne comme ceci:

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

c'est à dire le membre de droite côté d'introduire des variables de type, pas de gauche ou forall à gauche.

Au lieu de cela, nous avons besoin d'écrire 2-paramétrique typeclass:

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

Inconvénients: nous avons besoin de spécifier deuxième paramètre à chaque fois que nous utilisons MonadPlus.

Question: comment

instance Monoid a => MonadPlus Maybe a

peut être écrit si MonadPlus est un paramétriques typeclass? MonadPlus Maybe de base:

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

fonctionne pas comme 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]

---

Analogiquement, forall m a b n c d e. (Foo (m a b), Bar (n c d) e) donne lieu, pour (7 - 2 * 2)-paramétrique typeclass si nous voulons * types, (7 - 2 * 1)-paramétrique typeclass pour * -> * types, et (7 - 2 * 0) pour * -> * -> * types.