В какой степени экземпляры Applicative/Monad однозначно определены?

Ответ 1

Во-первых, поскольку Monoid не являются уникальными, то они не являются Writer Monad или Applicative s. Рассмотрим

data M a = M Int a

то вы можете дать ему экземпляры Applicative и Monad, изоморфные любому из:

Writer (Sum Int)
Writer (Product Int)

Учитывая экземпляр Monoid для типа s, другая изоморфная пара с разными экземплярами Applicative/Monad:

ReaderT s (Writer s)
State s

Что касается того, что один экземпляр Applicative распространяется на два разных Monad s, я не могу вспомнить ни одного примера. Однако, когда я попытался полностью убедить себя в том, что ZipList действительно невозможно сделать Monad, я нашел следующее довольно сильное ограничение, которое выполняется для любого Monad:

join (fmap (\x -> fmap (\y -> f x y) ys) xs) = f <$> xs <*> ys

Это не дает join для всех значений: в случае списков ограниченные значения - это те, где все элементы имеют одинаковую длину, то есть списки списков с "прямоугольной" формой.

(Для Reader monads, где "форма" монадических значений не меняется, на самом деле это все значения m (m x), поэтому они имеют уникальное расширение EDIT: подумайте об этом, Either, Maybe и Writer также имеют только "прямоугольные" значения m (m x), поэтому их расширение от Applicative до Monad также уникально.)

Я не удивлюсь, если существует Applicative с двумя Monad.

Для Alternative/MonadPlus, Я не могу вспомнить какой-либо закон для экземпляров, использующих закон левого распределения вместо Left Catch, я не вижу ничего, что мешало бы вам просто заменять (<|>) на flip (<|>). Я не знаю, есть ли менее тривиальная вариация.

ADDENDUM: Я вдруг вспомнил, что нашел пример Applicative с двумя Monad s. А именно, конечные списки. Там обычный экземпляр Monad [], но вы можете заменить его join на следующую функцию (по существу, сделать пустые списки "заразными" ):

ljoin xs
  | any null xs = []
  | otherwise   = concat xs

(Увы, списки должны быть конечными, потому что в противном случае проверка null никогда не закончится, и это разрушит закон монады join . fmap return == id.)

Это имеет то же значение, что и join/concat в прямоугольных списках списков, поэтому даст тот же Applicative. Насколько я помню, оказывается, что первые два монад-закона являются автоматическими, и вам просто нужно проверить ljoin . ljoin == ljoin . fmap ljoin.

Ответ 2

Учитывая, что каждый Applicative имеет аналог Backwards,

newtype Backwards f x = Backwards {backwards :: f x}
instance Applicative f => Applicative (Backwards f) where
  pure x = Backwards (pure x)
  Backwards ff <*> Backwards fs = Backwards (flip ($) <$> fs <*> ff)

необычно для Applicative быть однозначно определенным, так же как (и это очень далеко от несвязанного) многие множества распространяются на моноиды несколькими способами.

В этом ответе я поставил задачу найти по крайней мере четыре различных достоверных экземпляра Applicative для непустых списков: я не буду его испортить, но я даст большой намек на то, как охотиться.

Между тем, в какой-то замечательной недавней работе (которую я видел в летней школе несколько месяцев назад), Тармо Уусталу показал довольно аккуратный способ справиться с этой проблемой, по крайней мере, когда базовый функтор представляет собой контейнер, в смысл Абботта, Альтенкирха и Гани.

Предупреждение: зависимые типы впереди!

Что такое контейнер? Если у вас есть зависимые типы, вы можете представить контейнер-подобные функторы F равномерно, как определено двумя компонентами

• набор фигур, S: Установить
• S-индексный набор позиций, P: S → Set

До изоморфизма структуры данных контейнера в F X задаются зависимой парой некоторой формы s: S и некоторой функцией e: P s → X, которая сообщает вам элемент, расположенный в каждой позиции. То есть мы определяем расширение контейнера

(S <| P) X = (s : S) * (P s -> X)

(который, кстати, очень похож на обобщенный степенной ряд, если вы читаете -> как обратное экспонирование). Предполагается, что треугольник напоминает вам о дереве node сбоку, с элементом s: S, обозначающим вершину, и базовой линией, представляющей позицию P s. Мы говорим, что некоторый функтор является контейнером, если он изоморфен некоторому S <| P.

В Haskell вы можете легко взять S = F (), но построение P может занять довольно много хакеров типа. Но это то, что вы можете попробовать дома. Вы обнаружите, что контейнеры закрыты при всех обычных процессах формирования полиномиального типа, а также в идентификаторе,

Id ~= () <| \ _ -> ()

где вся форма выполнена только из одной внешней формы и внутренней формы для каждого внешнего положения,

(S0 <| P0) . (S1 <| P1)  ~=  ((S0 <| P0) S1) <| \ (s0, e0) -> (p0 : P0, P1 (e0 p0))

и некоторые другие вещи, в частности тензор, где есть одна внешняя и одна внутренняя форма (так что "внешний" и "внутренний" взаимозаменяемы)

(S0 <| P0) (X) (S1 <| P1)   =   ((S0, S1) <| \ (s0, s1) -> (P0 s0, P1 s1))

так что F (X) G означает "F -структуры G -структуры-все-одинаковые", например, [] (X) [] означает прямоугольные списки-списки. Но я отвлекаюсь

Полиморфные функции между контейнерами Каждая полиморфная функция

m : forall X. (S0 <| P0) X -> (S1 <| P1) X

может быть реализована морфизмом контейнера, построенным из двух компонентов очень определенным образом.

• функция f : S0 -> S1 отображение форм ввода в выходные формы;
• функция g : (s0 : S0) -> P1 (f s0) -> P0 s0 отображение выходных позиций для ввода позиций.

Наша полиморфная функция тогда

\ (s0, e0) -> (f s0, e0 . g s0)

где форма вывода вычисляется из формы ввода, тогда выходные позиции заполняются путем выбора элементов из входных позиций.

(Если вы Питер Хэнкок, у вас есть еще одна метафора для того, что происходит). Формы - это команды, позиции - это ответы, морфизм контейнера - это драйвер устройства, переводя команды в одну сторону, а затем отвечает другой.)

Каждый морфизм контейнера дает вам полиморфную функцию, но верно и обратное. Учитывая такое m, мы можем взять

(f s, g s) = m (s, id)

То есть, у нас есть теорема о представлении, говорящая, что каждая полиморфная функция между двумя контейнерами дается таким образом F, G -pair.

Что насчет Applicative? Мы немного понемногу потеряли на этом пути, построив всю эту технику. Но это того стоило. Когда базовые функторы для монадов и аппликаций являются контейнерами, полиморфные функции pure и <*>, return и join должны быть представлены соответствующим понятием морфизма контейнера.

Сначала возьмем аппликативы, используя их моноидальное представление. Нам нужно

unit : () -> (S <| P) ()
mult : forall X, Y. ((S <| P) X, (S <| P) Y) -> (S <| P) (X, Y)

Карты слева направо для фигур требуют от нас

unitS : () -> S
multS : (S, S) -> S

похоже, нам понадобится моноид. И когда вы проверяете применимые законы, вы обнаружите, что нам нужен ровно моноид. Приспособление контейнера с аппликативной структурой точно перерабатывает моноидные структуры на его формах с помощью подходящих операций, связанных с положением. Нечего делать для unit (потому что не существует chocie исходной позиции), но для mult нам нужно, чтобы ifenver

multS (s0, s1) = s

имеем

multP (s0, s1) : P s -> (P s0, P s1)

удовлетворяющих соответствующим условиям идентичности и ассоциативности. Если мы перейдем к интерпретации Хэнкока, мы определяем моноиды (skip, semicolon) для команд, где нет способа взглянуть на ответ на первую команду, прежде чем выбирать вторую, например команды - колоду перфокарт. Мы должны уметь отбирать ответы на комбинированные команды в индивидуальные ответы на отдельные команды.

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

Как насчет Monad? Между тем, для monads M с M ~= S <| P. Нам нужно

return : Id -> M
join   : M . M -> M

Сначала взглянув на фигуры, это означает, что нам нужен какой-то однобокий моноид.

return_f : () -> S
join_f   : (S <| P) S -> S  --  (s : S, P s -> S) -> S

Это однобокое, потому что мы получаем пучок фигур справа, а не только один. Если мы перейдем к интерпретации Хэнкока, мы определяем своего рода последовательную композицию для команд, где мы позволяем выбрать вторую команду на основе первого ответа, например, мы взаимодействуем в телетайпе. Более геометрически мы объясняем, как glom два слоя дерева в один. Было бы очень удивительно, если бы такие композиции были уникальными.

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

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

Изменить.. Чтобы выразить честь другому ответу, я должен заметить, что когда везде P s = (), тогда (S <| P) X ~= (S, X) и монад/аппликативные структуры совпадают точно друг с другом и с моноидных структур на S. То есть для монадов-писателей нам нужно только выбрать операции на уровне фигуры, потому что в каждом случае есть ровно одна позиция для значения.