Я хотел бы предложить более систематический подход к ответу на этот вопрос, а также показать примеры, в которых не используются какие-либо специальные приемы, такие как «нижние» значения или бесконечные типы данных или что-либо подобное.
Когда конструкторы типов не могут иметь экземпляры класса типов?
В общем, есть две причины, по которым конструктору типов может не иметь экземпляр определенного класса типов:
- Невозможно реализовать сигнатуры типов требуемых методов из класса типов.
- Может реализовывать сигнатуры типов, но не может соответствовать требуемым законам.
Примеры первого типа проще, чем тевторого типа, потому что для первого типа нам просто нужно проверить, можно ли реализовать функцию с заданной сигнатурой типа, в то время как для второго типа мы должны доказать, что никакая реализация не может удовлетворить законы.
Конкретные примеры
Это контраунктор, а не функтор, поскольку он использует параметр типа a в контравариантномпозиция.Невозможно реализовать функцию с сигнатурой типа (a -> b) -> F a -> F b.
Конструктор типа, который не является законным функтором , даже если сигнатура типа fmapможет быть реализовано:
data Q a = Q(a -> Int, a)
fmap :: (a -> b) -> Q a -> Q b
fmap f (Q(g, x)) = Q(\_ -> g x, f x) -- this fails the functor laws!
Любопытным аспектом этого примера является то, что мы можем реализовать fmap правильного типа, хотя F не может быть возможнобыть функтором, потому что он использует a в контравариантной позиции.Таким образом, эта реализация fmap, показанная выше, вводит в заблуждение - даже если она имеет правильную сигнатуру типа (я считаю, что это единственно возможная реализация этой сигнатуры типа), законы функтора не выполняются (для этого требуются некоторые простые вычисления).
На самом деле, F является только профунктором, - он не является ни функтором, ни контрафунктором.
Законный функтор, который не является аппликативным, поскольку подпись типа pure не может быть реализована: возьмите монаду Writer (a, w) и удалите ограничение, согласно которому w должно быть моноидом.Тогда невозможно построить значение типа (a, w) из a.
Функтор, который не является аппликативным , поскольку сигнатура типа <*> не может быть реализовано: data F a = Either (Int -> a) (String -> a).
Функтор, который не является законно аппликативным , даже если методы класса типов могут быть реализованы:
data P a = P ((a -> Int) -> Maybe a)
Конструктор типа P является функтором, поскольку он использует a только в ковариантных позициях.
instance Functor P where
fmap :: (a -> b) -> P a -> P b
fmap fab (P pa) = P (\q -> fmap fab $ pa (q . fab))
Единственно возможная реализация сигнатуры типа <*>это функция, которая всегда возвращает Nothing:
(<*>) :: P (a -> b) -> P a -> P b
(P pfab) <*> (P pa) = \_ -> Nothing -- fails the laws!
Но эта реализация не удовлетворяет закону идентичности для аппликативных функторов.
- Функтор
Applicative но не Monad, поскольку подпись типа bind не может быть реализована.
Я не знаю таких примеров!
- Функтор
Applicative, но не Monad, потому что законы не могут быть выполнены, даже еслисигнатура типа bind может быть реализована.
Этот пример вызвал немало дискуссий, поэтому можно с уверенностью сказать, что доказать правильность этого примера нелегко.Но несколько человек подтвердили это независимо разными способами.См. Является ли `PoE данных a = пустым |Соедините монаду? для дальнейшего обсуждения.
data B a = Maybe (a, a)
deriving Functor
instance Applicative B where
pure x = Just (x, x)
b1 <*> b2 = case (b1, b2) of
(Just (x1, y1), Just (x2, y2)) -> Just((x1, x2), (y1, y2))
_ -> Nothing
Несколько громоздко доказать, что законного Monad экземпляра не существует.Причина немонадного поведения заключается в том, что не существует естественного способа реализации bind, когда функция f :: a -> B b может вернуть Nothing или Just для различных значений a.
Возможно, яснее рассмотреть Maybe (a, a, a), который также не является монадой, и попытаться реализовать для этого join. Можно обнаружить, что не существует интуитивно разумного способа реализации join.
join :: Maybe (Maybe (a, a, a), Maybe (a, a, a), Maybe (a, a, a)) -> Maybe (a, a, a)
join Nothing = Nothing
join Just (Nothing, Just (x1,x2,x3), Just (y1,y2,y3)) = ???
join Just (Just (x1,x2,x3), Nothing, Just (y1,y2,y3)) = ???
-- etc.
В случаях, указанных ???, очевидно, что мы не можем получить Just (z1, z2, z3) любым разумным и симметричным способом из шести различных значений типа a. Конечно, мы могли бы выбрать какое-то произвольное подмножество из этих шести значений, например, всегда брать первое непустое Maybe, но это не удовлетворяло бы законам монады. Возвращение Nothing также не будет удовлетворять законам.
- Древовидная структура данных, которая не является монадой , хотя она имеет ассоциативность для
bind - но не соответствует законам идентичности.
Обычная древовидная монада (или «дерево с ветвями в форме функтора») определяется как
data Tr f a = Leaf a | Branch (f (Tr f a))
Это бесплатная монада над функтором f. Форма данных представляет собой дерево, где каждая точка ветвления является «функторной» из поддеревьев. Стандартное двоичное дерево будет получено с type f a = (a, a).
Если мы изменим эту структуру данных, сделав также листья в форме функтора f, мы получим то, что я называю «полумонадой» - оно имеет bind, которое удовлетворяет законам естественности и ассоциативности, но его pure метод не соответствует одному из законов идентичности. «Полумонады - это полугруппы в категории эндофункторов, в чем проблема?» Это тип класса Bind.
Для простоты я определяю метод join вместо bind:
data Trs f a = Leaf (f a) | Branch (f (Trs f a))
join :: Trs f (Trs f a) -> Trs f a
join (Leaf ftrs) = Branch ftrs
join (Branch ftrstrs) = Branch (fmap @f join ftrstrs)
Прививка веток стандартная, но прививка листьев нестандартная и дает Branch. Это не проблема для закона ассоциативности, но нарушает один из законов идентичности.
Когда полиномиальные типы имеют экземпляры монад?
Ни одному из функторов Maybe (a, a) и Maybe (a, a, a) нельзя дать законный Monad экземпляр, хотя они, очевидно, Applicative.
У этих функторов нет никаких хитростей - нигде Void или bottom, ни хитрости, ни лени / строгости, ни бесконечных структур, ни ограничений на классы типов. Экземпляр Applicative является полностью стандартным. Функции return и bind могут быть реализованы для этих функторов, но не будут удовлетворять законам монады. Другими словами, эти функторы не являются монадами, потому что отсутствует определенная структура (но непросто понять, чего именно не хватает). Например, небольшое изменение в функторе может превратить его в монаду: data Maybe a = Nothing | Just a - это монада. Другой подобный функтор data P12 a = Either a (a, a) также является монадой.
Конструкции для полиномиальных монад
В общем, вот некоторые конструкции, которые производят законные Monad из полиномиальных типов. Во всех этих конструкциях M является монадой:
type M a = Either c (w, a) где w - любой моноид type M a = m (Either c (w, a)), где m - любая монада, а w - любой моноид type M a = (m1 a, m2 a) где m1 и m2 - любые монады type M a = Either a (m a), где m - любая монада
Первая конструкция WriterT w (Either c), вторая конструкция WriterT w (EitherT c m). Третья конструкция является компонентным произведением монад: pure @M определяется как компонентное произведение pure @m1 и pure @m2, а join @M определяется путем пропуска данных перекрестного произведения (например, m1 (m1 a, m2 a) отображается на m1 (m1 a), пропуская вторую часть кортежа):
join :: (m1 (m1 a, m2 a), m2 (m1 a, m2 a)) -> (m1 a, m2 a)
join (m1x, m2x) = (join @m1 (fmap fst m1x), join @m2 (fmap snd m2x))
Четвертая конструкция определяется как
data M m a = Either a (m a)
instance Monad m => Monad M m where
pure x = Left x
join :: Either (M m a) (m (M m a)) -> M m a
join (Left mma) = mma
join (Right me) = Right $ join @m $ fmap @m squash me where
squash :: M m a -> m a
squash (Left x) = pure @m x
squash (Right ma) = ma
Я проверил, что все четыре конструкции производят законные монады.
I гипотеза о том, что нет других конструкций для полиномиальных монад. Например, функтор Maybe (Either (a, a) (a, a, a, a)) не получается ни через одну из этих конструкций и поэтому не является монадическим. Однако Either (a, a) (a, a, a) является монадическим, поскольку он изоморфен произведению трех монад a, a и Maybe a. Кроме того, Either (a,a) (a,a,a,a) является монадическим, потому что оно изоморфно произведению a и Either a (a, a, a).
Четыре конструкции, показанные выше, позволят нам получить любую сумму любого количества продуктов любого числа a, например, Either (Either (a, a) (a, a, a, a)) (a, a, a, a, a)) и так далее.Все такие конструкторы типов будут иметь (по крайней мере один) экземпляр Monad.
Конечно, еще неизвестно, какие варианты использования могут существовать для таких монад.Другая проблема заключается в том, что экземпляры Monad, полученные с помощью конструкций 1-4, как правило, не являются уникальными.Например, конструктору типа type F a = Either a (a, a) может быть дан экземпляр Monad двумя способами: конструкцией 4 с использованием монады (a, a) и конструкцией 3 с использованием изоморфизма типов Either a (a, a) = (a, Maybe a).Опять же, поиск вариантов использования для этих реализаций не сразу очевиден.
Остается вопрос - учитывая произвольный тип данных полинома, как распознать, имеет ли он экземпляр Monad.Я не знаю, как доказать, что нет других конструкций для полиномиальных монад.Я не думаю, что до сих пор существует какая-либо теория для ответа на этот вопрос.