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

Question

Итак, монада-писатель позволяет вам записывать материал в [обычно] какой-то контейнер и возвращать этот контейнер в конце. В большинстве реализаций "контейнер" может быть любым моноидом.

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

Чтобы действительно написать монаду, двойственную к обычной монаде писателя, нам понадобится какая-то структура, двойственная моноиду.

1. Кто-нибудь знает, что это за двойная структура?
2. Кто-нибудь написал эту монаду? Есть ли известное имя для этого?

Answer 1

Я не совсем уверен в том, каким должен быть дуал моноида, но думаю о дуале (возможно, неправильно) как о чем-то противоположном (просто на том основании, что Comonad является дуалом монады и выполняет все те же операции. но наоборот наоборот). Вместо того, чтобы основывать это на 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]

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

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

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

Answer 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 = ()

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

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

РЕДАКТИРОВАТЬ: Читатель с 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,

Answer 3

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

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

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

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

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 На запас уникальных этикеток стоит настоящая монада.