¿Qué pasa con el sistema de restricciones actual de GHC Haskell?

Question

He oído que hay algunos problemas con el sistema de restricción "roto" de Haskell, a partir de GHC 7.6 y siguientes. ¿Qué está "mal" con eso? ¿Existe un sistema comparable comparable que supere esos defectos?

Por ejemplo, tanto edwardk como tekmo han tenido problemas (por ejemplo, this comment from tekmo).

Answer 1

Ok, tuve varias discusiones con otras personas antes de publicar aquí porque quería hacerlo bien. Todos me mostraron que todos los problemas que describí se reducen a la falta de restricciones polimórficas.

El ejemplo más simple de este problema es la clase MonadPlus, definida como:

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

... con las siguientes leyes:

mzero `mplus` m = m 

m `mplus` mzero = m 

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

en cuenta que estos son los Monoid leyes, donde el Monoid clase está dada por:

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) 

Entonces, ¿por qué tenemos la clase MonadPlus? La razón es porque Haskell nos prohíbe las restricciones de escritura de la forma:

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

programadores Así Haskell deben evitar esta falla del sistema de tipo definiendo una clase separada para manejar este caso polimórfica particular.

Sin embargo, esto no siempre es una solución viable. Por ejemplo, en mi propio trabajo en la biblioteca pipes, que se encuentra con frecuencia la necesidad de plantear restricciones de la forma:

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

A diferencia de la solución MonadPlus, no puede permitirse el lujo de cambiar la clase Monad tipo a una clase de tipo diferente para evitar el problema de restricción polimórfica porque los usuarios de mi biblioteca perderían la notación do, que es un alto precio a pagar.

Esto también aparece al componer transformadores, tanto los transformadores de mónada como los transformadores de proxy que incluyo en mi biblioteca. Nos gustaría escribir algo como:

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 

Este primer intento no funciona porque lift no limita su resultado ser un Monad. Realmente necesitaríamos:

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

... pero el sistema de restricciones de Haskell no lo permite.

Este problema se volverá cada vez más pronunciado a medida que los usuarios de Haskell pasen a escribir constructores de tipos superiores. Por lo general, tendrá una clase de tipo de la forma:

class SomeClass someHigherKindedTypeConstructor where 
    ... 

...pero se desea limitar algunos constructor de tipo derivado kinded inferior:

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

Sin embargo, sin limitaciones polimórficas, esa limitación no es legal. La última vez que me quejé de este problema fue porque mi biblioteca pipes usa tipos de tipos muy altos, por lo que me encuentro con este problema constantemente.

Existen soluciones provisionales que usan tipos de datos que varias personas me han propuesto, pero aún no he tenido el tiempo de evaluarlas para comprender qué extensiones requieren o cuál soluciona mi problema correctamente. Alguien más familiarizado con este problema podría quizás proporcionar una respuesta por separado detallando la solución a esto y por qué funciona.

Answer 2

[un seguimiento de la respuesta de Gabriel González]

La notación adecuada para las limitaciones y las cuantificaciones en Haskell es la siguiente:

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

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

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

... 

clases pueden ser omitidos, así como forall s Ranking-1 tipos:

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

por ejemplo:

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

o sin Rank2Types (ya que sólo tienen tipos de rango-1 aquí), y el uso 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 

El "problema" es que no podemos escribir

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

o

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

Es decir, forall m a. (Monad m, Monoid (m a)) se puede usar como una restricción independiente, pero no se puede crear un alias con una nueva clase de tipo paramétrica para los tipos *->*.

Esto es porque el mecanismo de clase de tipos Defintion funciona así:

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

es decir, los rhs lado introducen variables de tipo, no los LHS o forall en los LHS.

En su lugar, tenemos que escribir clase de tipos 2-paramétricos:

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

Contras: tenemos que especificar segundo parámetro cada vez que utilizamos MonadPlus.

Pregunta: ¿cómo

instance Monoid a => MonadPlus Maybe a 

se puede escribir si MonadPlus es uno paramétrico clase de tipos?MonadPlus Maybe de base:

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

no funciona como 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] 

---

Análogamente, forall m a b n c d e. (Foo (m a b), Bar (n c d) e) da lugar a (7 - 2 * 2) clase de tipos -PARAMETRIC si queremos * tipos, (7 - 2 * 1) -param clase de tipo etric para tipos * -> * y (7 - 2 * 0) para tipos * -> * -> *.