Я хотел бы предложить более систематический подход к ответу на этот вопрос, а также показать примеры, в которых не используются какие-либо специальные приемы, такие как «нижние» значения или бесконечные типы данных или что-то в этом роде.
Когда конструкторы типов не могут иметь экземпляры классов типов?
В общем, существует две причины, по которым конструктор типа может не иметь экземпляра определенного класса типа:
- Невозможно реализовать сигнатуры типов требуемых методов из класса типа.
- Может реализовывать типовые подписи, но не может соответствовать требуемым законам.
Примеры первого типа проще, чем примеры второго типа, потому что для первого типа нам просто нужно проверить, можно ли реализовать функцию с заданной сигнатурой типа, а для второго типа мы должны доказать, что нет реализации может соответствовать законам.
Конкретные примеры
Это контрафунктор, а не функтор, по отношению к параметру типа a, потому что a находится в контравариантном положении. Невозможно реализовать функцию с сигнатурой типа (a -> b) -> F z a -> F z 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, показанная выше, вводит в заблуждение - даже несмотря на то, что она имеет правильную сигнатуру типа (я считаю, что это единственная возможная реализация этой сигнатуры типа), законы функторов не выполняются. Например, fmap id ≠ id, потому что let (Q(f,_)) = fmap id (Q(read,"123")) in f "456" это 123, а let (Q(f,_)) = id (Q(read,"123")) in f "456" это 456.
Фактически 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 может быть реализована.
Этот пример вызвал немало дискуссий, поэтому можно с уверенностью сказать, что доказать его правильность непросто. Но несколько человек проверили это независимо разными методами. См. Является ли `data PoE a = Empty | Соедините монаду a` 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
Я проверил, что все четыре конструкции производят законные монады.
Я предполагаю, что других конструкций для полиномиальных монад не существует. Например, функтор 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. Я не знаю, как доказать, что других конструкций для полиномиальных монад не существует. Я не думаю, что пока существует какая-либо теория, чтобы ответить на этот вопрос.
person
winitzki
schedule
07.04.2018
* -> *), для которого не существует нет подходящегоfmap? - person Owen schedule 28.08.2011a -> Stringне функтор. - person Rotsor schedule 28.08.2011a -> String- математический функтор, но не HaskellFunctor, для ясности. - person J. Abrahamson schedule 04.09.2014(a -> b) -> f b -> f a- person AJF schedule 23.03.2015