"Читательская" монада

Ответ 1

Я не совсем уверен в том, что должно быть двойственным моноидом, но думать о двойственном (возможно, некорректно) как о чем-то противоположном (просто на том основании, что Комонад является двойником Монады и имеет все те же операции, но наоборот). Вместо того, чтобы основывать его на mappend и mempty, я бы основывал его на:

fold :: (Foldable f, Monoid m) => f m -> m

Если мы специализируем f на список, мы получаем:

fold :: Monoid m => [m] -> m

Мне кажется, что я должен содержать все моноидные классы, в частности.

mempty == fold []
mappend x y == fold [x, y]

Итак, тогда я предполагаю, что двойственный из этого другого моноидного класса будет:

unfold :: (Comonoid m) => m -> [m]

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

Итак, на этой основе, я думаю, что монада "читателя", которую вы описываете, будет поставлять монаду. Монада поставки - это, фактически, трансформатор состояния списка значений, так что в любой момент мы можем выбрать поставку из списка из списка. В этом случае список будет результатом unold.supply monad

Я должен подчеркнуть, что я не эксперт Хаскелла и не эксперт-теоретик. Но это то, что заставило меня задуматься.

Ответ 2

Дуал моноида является комонидом. Напомним, что моноид определяется как (что-то изоморфное)

 class Monoid m where
    create :: () -> m
    combine :: (m,m) -> m

с этими законами

 combine (create (),x) = x
 combine (x,create ()) = x
 combine (combine (x,y),z) = combine (x,combine (y,z))

таким образом

 class Comonoid m where
    delete :: m -> ()
    split :: m -> (m,m)

необходимы некоторые стандартные операции

 first :: (a -> b) -> (a,c) -> (b,c)
 second :: (c -> d) -> (a,c) -> (a,d)

 idL :: ((),x) -> x
 idR :: (x,()) -> x

 assoc :: ((x,y),z) -> (x,(y,z))

с такими законами, как

idL $ first delete $ (split x) = x
idR $ second delete $ (split x) = x
assoc $ first split (split x) = second split (split x)

Эта модель выглядит странно по какой-то причине. Он имеет экземпляр

instance Comonoid m where
   split x = (x,x)
   delete x = ()

в Haskell, это единственный экземпляр. Мы можем переписать читателя как точный дубль писателя, но поскольку существует только один экземпляр для comonoid, мы получаем что-то изоморфное стандартным типам чтения.

Наличие всех типов комонидов - это то, что делает категорию "декартовой" в "декартовой закрытой категории". "Моноидальные закрытые категории" похожи на CCC, но без этого свойства и связаны с системами подструктурного типа. Частью привлекательности линейной логики является повышенная симметрия, что является примером. Хотя, имея подструктурные типы, вы можете определить comonoids с более интересными свойствами (поддерживая такие вещи, как управление ресурсами). Фактически, это обеспечивает основу для понимания роли конструкторов и деструкторов копирования в С++ (хотя С++ не применяет важные свойства из-за существования указателей).

РЕДАКТОР: Читатель от комонидов

newtype Reader r x = Reader {runReader :: r -> x}
forget :: Comonoid m => (m,a) -> a
forget = idL . first delete

instance Comonoid r => Monad (Reader r) where
   return x = Reader $ \r -> forget (r,x)
   m >>= f = \r -> let (r1,r2) = split r in runReader (f (runReader m r1)) r2

ask :: Comonoid r => Reader r r
ask = Reader id

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

Ответ 3

Предложение основано на состоянии, что делает его субоптимальным для некоторых приложений. Например, мы можем захотеть создать бесконечное дерево заданных значений (например, randoms):

tree :: (Something r) => Supply r (Tree r)
tree = Branch <$> supply <*> sequenceA [tree, tree]

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

Вам нужно что-то расщепляемое (как в @PhillipJF Comonoid). Но есть проблема, если вы попытаетесь сделать это в Monad:

newtype Supply r a = Supply { runSupply :: r -> a }

instance (Splittable r) => Monad (Supply r) where
    return = Supply . const
    Supply m >>= f = Supply $ \r ->
        let (r',r'') = split r in
        runSupply (f (m r')) r''

Поскольку законы монады требуют f >>= return = f, поэтому это означает, что r'' = r в определении (>>=). Но для законов монады также требуется, чтобы return x >>= f = f x, поэтому r' = r. Таким образом, для Supply, чтобы быть монадой, split x = (x,x), и, таким образом, у вас есть обычный старый Reader снова.

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

Если вы разрешаете Supply быть монадой до некоторого отношения эквивалентности, то вы можете получить нетривиальные расщепления. Например. value-supply построит разделимые объекты, которые будут выдавать уникальные ярлыки из списка в неуказанном порядке (используя магию unsafe*) - так что монада поставки питания будет монада до перестановки ярлыков. Это все, что необходимо для многих приложений. И, фактически, существует функция

runSupply :: (forall r. Eq r => Supply r a) -> a

который абстрагируется над этим отношением эквивалентности, чтобы дать четко определенный чистый интерфейс, потому что единственное, что он позволяет вам делать с ярлыками, - это увидеть, являются ли они равными, и это не изменится, если вы перепутаете их. Если это runSupply - единственное наблюдение, которое вы разрешаете на Supply, то Supply при поставке уникальных ярлыков - настоящая монада.