Что случилось с системой ограничения текущих ограничений GHC Haskell?

Ответ 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)) => ...

Итак, программисты Haskell должны обойти этот недостаток системы типов, определив отдельный класс для обработки этого конкретного полиморфного случая.

Однако это не всегда жизнеспособное решение. Например, в моей работе над библиотекой pipes я часто сталкивался с необходимостью создавать ограничения формы:

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

В отличие от решения MonadPlus я не могу позволить переключить класс типа Monad на другой тип класса, чтобы обойти проблему полиморфного ограничения, потому что тогда пользователи моей библиотеки потеряли бы обозначение do, что является высоким цена для оплаты.

Это также возникает при создании трансформаторов, как монадных трансформаторов, так и прокси-трансформаторов, которые я включаю в свою библиотеку. Мы хотели бы написать что-то вроде:

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 не ограничивает ее результат a 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
    ...

... но вы захотите ограничить некоторый конструктор производного типа нижнего рода:

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

Однако, без полиморфных ограничений, это ограничение не является законным. Я недавно жаловался на эту проблему, потому что моя библиотека pipes использует типы очень высоких видов, поэтому я постоянно сталкиваюсь с этой проблемой.

Существуют временные решения, использующие типы данных, которые несколько человек предложили мне, но у меня пока нет времени, чтобы оценить их, чтобы понять, какие расширения они требуют или который правильно решает мою проблему. Кто-нибудь, более знакомый с этим вопросом, может, возможно, предоставить отдельный ответ, в котором подробно описывается решение этого и почему оно работает.

Ответ 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)) может использоваться как автономное ограничение, но не может быть псевдонимом с новым однопараметрическим классом типа *->*.

Это связано с тем, что механизм детекции typeclass работает следующим образом:

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

то есть. сторона rhs вводит переменные типа, а не lhs или forall в lhs.

Вместо этого нам нужно написать 2-параметрическое 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

Минусы: нам нужно указывать второй параметр каждый раз, когда мы используем MonadPlus.

Вопрос: как

instance Monoid a => MonadPlus Maybe a

может быть записано, если MonadPlus является однопараметрическим typeclass? MonadPlus Maybe from 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) для типов * -> * -> *.