Что не так с нынешней системой ограничений GHC Haskell?

Question

Я слышал, что есть некоторые проблемы с "сломанной" системой ограничений Haskell, начиная с GHC 7.6 и ниже. Что с этим не так? Существует ли сопоставимая существующая система, которая преодолевает эти недостатки?

Например, у edwardk и tekmo возникли проблемы (например, этот комментарий от tekmo).

Answer 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 не ограничивает его результат быть 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 Библиотека использует типы очень высокого класса, поэтому я постоянно сталкиваюсь с этой проблемой.

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

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

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

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

т.е. правая сторона вводит переменные типа, а не 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

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

Вопрос: как

instance Monoid a => MonadPlus Maybe a

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