Является ли это свойство функтора сильнее монады?

Размышляя о том, как обобщать монады, я придумал следующее свойство функтора F:

inject :: (a -> F b) -> F(a -> b) 

- что должно быть естественным преобразованием как в а и б.

В отсутствие лучшего имени я называю функтор F связываемым, если существует естественное преобразование inject показано выше.

Основной вопрос заключается в том, известно ли это свойство и имеет ли оно имя, и как оно связано с другими известными свойствами функторов (такими как аппликативный, монадический, остроконечный, проходимый и т. Д.).

Мотивация имени "связываемый" исходит из следующего соображения: предположим, что М - это монада, а F - "связываемый" функтор. Тогда каждый имеет следующий естественный морфизм:

fbind :: M a -> (a -> F(M b)) -> F(M b)

Это похоже на монадическое "связывание",

bind :: M a -> (a -> M b) -> M b

кроме результата украшен функтор Ф.

Идея позади fbind было то, что обобщенная монадическая операция может дать не только один результат M b, но и "функторную" F таких результатов. Я хочу выразить ситуацию, когда монадическая операция дает несколько "цепочек вычислений", а не одну; каждая "цепь вычислений" снова является монадическим вычислением.

Обратите внимание, что каждый функтор F имеет морфизм

eject :: F(a -> b) -> a -> F b

который обратен к "впрыскивать". Но не каждый функтор F имеет "инъекцию".

Примеры функторов, которые имеют "инъекцию": F t = (t,t,t) или же F t = c -> (t,t) где с - постоянный тип. ФУНКТОРЫ F t = c (постоянный функтор) или F t = (c,t) не являются "связываемыми" (т.е. не имеют "впрыскивать"). Функтор продолжения F t = (t -> r) -> r также, похоже, не inject,

Существование "впрыскивать" можно сформулировать по-другому. Рассмотрим функтор "читатель" R t = c -> t где с - постоянный тип. (Этот функтор является аппликативным и монадическим, но это не относится к делу.) Тогда свойство "впрыскивать" означает R (F t) -> F (R t)иными словами, что R коммутирует с F. Обратите внимание, что это не то же самое, что требование прохождения F; это было бы F (R t) -> R (F t), что всегда выполняется для любого функтора F относительно R.

До сих пор мне удалось показать, что "вводить" подразумевает "fbind" для любой монады М.

Кроме того, я показал, что каждый функтор F, который имеет "инъекцию", также будет иметь следующие дополнительные свойства:

  • это указано

point :: t -> F t

  • если F "связываемый" и аппликативный, то F также является монадой

  • если F и G являются "связываемыми", то и функтор пар F * G (но не F + G)

  • если F является "связываемым", а A является любым профунктором, тогда (про) функтор G t = A t -> F t привязываемый

  • функтор идентичности является связываемым.

Открытые вопросы:

  • Является ли свойство быть "связываемым" эквивалентным некоторым другим хорошо известным свойствам, или это новое свойство функтора, которое обычно не рассматривается?

  • Существуют ли какие-либо другие свойства функтора "F", вытекающие из существования "инъекции"?

  • нужны ли какие-то законы для "инъекции", это было бы полезно? Например, мы могли бы потребовать, чтобы R (F t) была изоморфна F (R t) в одном или обоих направлениях.

1 ответ

Решение

Чтобы немного улучшить терминологию, я предлагаю называть эти функторы "жесткими", а не "связываемыми". Мотивация для высказывания "жесткая" будет объяснена ниже.

Функтор f называется жестким, если он имеет inject метод, как показано. Обратите внимание, что каждый функтор имеет eject метод.

class (Functor f) => Rigid f where
  inject :: (a -> f b) -> f(a -> b)

  eject :: f(a -> b) -> a -> f b
  eject fab x = fmap (\ab -> ab x) fab

Закон "невырожденности" должен содержать:

eject . inject = id

Жесткий функтор всегда указан:

instance (Rigid f) => Pointed f where
  point :: t -> f t
  point x = fmap (const x) (inject id)

Если жесткий функтор аппликативный, то он автоматически монадический:

instance (Rigid f, Applicative f) => Monad f where
  bind :: f a -> (a -> f b) -> f b
  bind fa afb = (inject afb) <*> fa

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

Основными контрпримерами монадических функторов, которые не являются жесткими, являются Maybe а также List, Это функторы, которые имеют более одного конструктора: как правило, такие функторы не являются жесткими.

Проблема с реализацией inject за Maybe в том, что inject должен преобразовать функцию типа a -> Maybe b в Maybe(a -> b) в то время как Maybe имеет два конструктора. Функция типа a -> Maybe b может вернуть разные конструкторы для разных значений a, Тем не менее, мы должны построить значение типа Maybe(a -> b), Если для некоторых a данная функция производит Nothingу нас нет b поэтому мы не можем произвести полную функцию a->b, Таким образом, мы не можем вернуться Just(a->b); мы вынуждены вернуться Nothing до тех пор, пока данная функция производит Nothing даже для одного значения a, Но мы не можем проверить, что данная функция типа a -> Maybe b производит Just(...) для всех значений a, Поэтому мы вынуждены вернуться Nothing во всех случаях. Это не удовлетворит закон невырожденности.

Итак, мы можем реализовать inject если f t это контейнер "фиксированной формы" (имеющий только один конструктор). Отсюда и название "жесткий".

Другое объяснение того, почему жесткость является более строгим, чем монадичность, заключается в рассмотрении естественно определенного выражения

(inject id) :: f(f a -> a) 

где id :: f a -> f a, Это показывает, что мы можем иметь F-алгебру f a -> a для любого типа aДо тех пор, пока он внутри f, Это неправда, что любая монада имеет алгебру; например, различные "будущие" монады, а также IO Монада описать вычисления типа f a которые не позволяют нам извлекать значения типа a - у нас не должно быть метода типа f a -> a даже если завернутый в f-контейнер. Это показывает, что "будущие" монады и IO Монада не жесткая.

Свойство, которое строго сильнее жесткости, это дистрибутивность одного из пакетов Э. Кметта. Функтор f является распределительным, если мы можем поменять порядок как в p (f t) -> f (p t) для любого функтора p, Жесткость - это то же самое, что возможность менять порядок только по отношению к функтору "читатель". r t = a -> t, Итак, все дистрибутивные функторы жесткие.

Все дистрибутивные функторы обязательно представимы, что означает, что они эквивалентны функтору "читателя" c -> t с некоторым фиксированным типом c, Однако не все жесткие функторы представимы. Примером является функтор g определяется

type g t = (t -> r) -> t

Функтор g не эквивалентны c -> t с фиксированным типом c,

Другие примеры жестких функторов, которые не представимы (т.е. не являются "дистрибутивными"), являются функторами вида a t -> f t где a любой контрафактор и f жесткий функтор. Кроме того, декартово произведение и композиция двух жестких функторов снова жестки. Таким образом, мы можем привести множество примеров жестких функторов в классе экспоненциально-полиномиальных функторов.

Мой ответ на вопрос " Каков общий случай функции продвижения QuickCheck?" также перечислены конструкции жестких функторов.

Наконец, я нашел два варианта использования жестких функторов.

Первый вариант использования был исходной мотивацией для рассмотрения жестких функторов: мы хотели бы вернуть несколько монадических результатов одновременно. Если m это монада, и мы хотим иметь fbind как показано в вопросе, нам нужно f быть жестким. Тогда мы можем реализовать fbind как

fbind :: m a -> (a -> f (m b)) -> f (m b)
fbind ma afmb = fmap (bind ma) (inject afmb)

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

Второй вариант использования вытекает из следующего рассмотрения. Предположим, у нас есть программа p :: a который внутренне использует функцию f :: b -> c, Теперь мы заметили, что функция f очень медленно, и мы хотели бы реорганизовать программу, заменив f с монадическим "будущим" или "заданием", или вообще со стрелой Клейсли f' :: b -> m c для какой-то монады m, Мы, конечно, ожидаем, что программа p также станет монадическим: p' :: m a, Наша задача - рефакторинг p в p',

Рефакторинг происходит в два этапа: во-первых, мы проводим рефакторинг программы p так что функция f явно аргумент p, Предположим, что это было сделано, так что теперь у нас есть p = q f где

q :: (b -> c) -> a

Во-вторых, мы заменим f от f', Теперь мы предполагаем, что q а также f' дано. Мы хотели бы построить новую программу q' типа

q' :: (b -> m c) -> m a

чтобы p' = q' f', Вопрос в том, можем ли мы определить общий комбинатор, который будет рефакторинг q в q',

refactor :: ((b -> c) -> a) -> (b -> m c) -> m a

Оказывается, что refactor может быть построен только если m жесткий функтор. В попытке реализовать refactorмы находим по существу ту же проблему, что и при попытке реализовать inject за Maybe: нам дана функция f' :: b -> m c которые могут возвращать различные монадические эффекты m c для разных b, но мы обязаны построить m a, который должен представлять один и тот же монадический эффект для всех b, Это не может работать, например, если m это монада с более чем одним конструктором.

Если m жесткая (и нам не нужно требовать, чтобы m быть монадой), мы можем реализовать refactor:

refactor bca bmc = fmap bca (inject bmc)

Если m не является жестким, мы не можем рефакторинг произвольных программ. До сих пор мы видели, что монада продолжения жесткая, но "будущие" монады и IO Монада не жесткая. Это еще раз показывает, что жесткость, в некотором смысле, более сильное свойство, чем монадичность.

В последнее время я проводил некоторые эксперименты, чтобы лучше понять Distributive, К счастью, мои результаты кажутся тесно связанными с вашими жесткими функторами, что разъясняет их обоих.

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

flap :: Functor f => f (a -> b) -> a -> f b
flap u a = ($ a) <$> u 

class Functor g => Rigid g where
    fflip :: (a -> g b) -> g (a -> b)
    fflip f = (. f) <$> extractors

    extractors :: g (g a -> a)
    extractors = fflip id

-- "Left inverse"/non-degeneracy law: flap . fflip = id

instance Rigid ((->) r) where
    fflip = flip

Несколько замечаний по поводу моей формулировки:

  • Я изменил имена inject а также eject в fflip а также flap В основном потому, что, на мой взгляд, flap больше похоже на инъекцию, из-за таких вещей:

    sweep :: Functor f => f a -> b -> f (a, b)
    sweep u b = flap ((,) <$> u) b
    
  • Я взял flap имя из протолуды. Это игра на flip, что подходит, потому что это один из двух симметричных способов его обобщения. (Мы можем вытащить функцию за пределы произвольного Functor, как в flap или потяните Rigid функтор вне функции, как в fflip.)

  • Я впервые понял значение extractors во время игры с Distributive, но мне не пришло в голову, что это может иметь смысл как часть другого класса. extractors а также fflip являются взаимозаменяемыми, что позволяет, например, написать этот довольно аккуратный экземпляр для монады поиска / выбора:

    newtype Sel r a = Sel { runSel :: (a -> r) -> a }
        deriving (Functor, Applicative, Monad) via SelectT r Identity
    
    instance Rigid (Sel r) where
        -- Sel r (Sel r a -> a) ~ ((Sel r a -> a) -> r) -> Sel r a -> a
        extractors = Sel $ \k m -> m `runSel` \a -> k (const a)
    

Каждый дистрибутивный функтор жесток:

fflipDistrib :: Distributive g => (a -> g b) -> g (a -> b)
fflipDistrib = distribute @_ @((->) _)
-- From this point on, I will pretend Rigid is a superclass of Distributive.
-- There would be some tough questions about interface ergonomics if we were
-- writing this into a library. We don't have to worry about that right now,
-- though.

С другой стороны, мы можем написать функцию, которая имитирует подпись distribute с помощью Rigid:

infuse :: (Rigid g, Functor f) => f (g a) -> g (f a)
infuse u = (<$> u) <$> extractors

infuse однако не distribute, Как вы заметили, существуют жесткие функторы, которые не являются дистрибутивными, такие как Sel, Поэтому мы должны сделать вывод, что infuse В общем случае не следует распределительным законам.

(В сторону: что infuse не законно distribute на случай, если Sel может быть установлено аргументом кардинальности. Если infuse следуя распределительным законам, мы бы infuse . infuse = id для любых двух жестких функторов. Однако что-то вроде infuse @((->) Bool) @(Sel r) приводит к типу результата с меньшим количеством жителей, чем тип аргумента; следовательно, нет никакого способа, которым у этого может быть левый обратный.)

Место в созвездии

На этом этапе было бы уместно уточнить нашу картину того, что именно отличает Distributive из Rigid, Учитывая, что ваш жесткий закон flap . fflip = id Интуиция подсказывает другую половину изоморфизма, fflip . flap = id, может иметь место в случае Distributive, Проверка этой гипотезы требует обхода Distributive,

Существует альтернативное представление Distributive (а также Rigid) в котором distribute (или же fflip) учитывается через функцию-функтор. Более конкретно, любое функторное значение типа g a может быть преобразован в подвеску CPS, которая занимает forall x. g x -> x экстрактор:

-- The existential wrapper is needed to prevent undue specialisation by GHC.
-- With pen and paper, we can leave it implicit.
data Ev g a where
    Ev :: ((g x -> x) -> a) -> Ev g a

-- Existential aside, this is ultimately just a function type.
deriving instance Functor (Ev g)

-- Morally, evert = flip id
evert :: g a -> Ev g a
evert u = Ev $ \e -> e u

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

-- Morally, revert = flip fmap extractors
revert :: Rigid g => Ev g a -> g a
revert (Ev s) = s <$> extractors

Ev g сам по себе Distributive независимо от того, что g это - в конце концов, это просто функция:

-- We need unsafeCoerce (yikes!) because GHC can't be persuaded that we aren't
-- doing anything untoward with the existential.
-- Note that flip = fflip @((->) _)
instance Rigid (Ev g) where
    fflip = Ev . flip . fmap (\(Ev s) -> unsafeCoerce s)

-- Analogously, flap = distribute @((->) _)
instance Distributive (Ev g) where
    distribute = Ev . flap . fmap (\(Ev s) -> unsafeCoerce s) 

В дальнейшем, fflip а также distribute для произвольной Rigid / Distributive функторы могут быть направлены через evert а также revert:

-- fflip @(Ev g) ~ flip = distribute @((->) _) @((->) _)
fflipEv :: Rigid g => (a -> g b) -> g (a -> b)
fflipEv = revert . fflip . fmap evert

-- distribute @(Ev g) ~ flap = distribute @((->) _) _
distributeEv :: (Rigid g, Functor f) => f (g a) -> g (f a) 
distributeEv = revert . distribute . fmap evert

revert, на самом деле, было бы достаточно для реализации Distributive, В таких условиях распределительные законы требуют evert а также revert существо обратное:

revert . evert = id  -- "home" roundtrip, right inverse law
evert . revert = id  -- "away" roundtrip, left inverse law

Два обхода соответствуют, соответственно, двум несвободным законам распределения:

fmap runIdentity . distribute = runIdentity                               -- identity
fmap getCompose . distribute = distribute . fmap distribute . getCompose  -- composition

(The distribute . distribute = id Требование указано в Data.Distributive документы в конечном итоге составляют эти два закона плюс естественность.)

Ранее я размышлял об изоморфизме, включающем fflip:

flap . fflip = id  -- "home" roundtrip, left inverse Rigid law  
fflip . flap = id  -- "away" roundtrip, would-be right inverse law

Можно непосредственно проверить, что жесткий закон, flap . fflip = id, эквивалентно другому "домашнему" туда и обратно, revert . evert = id, Другое направление сложнее. Предполагаемые изоморфизмы могут быть связаны следующим образом:

                        g (a -> b)        
    {fflip => <= flap}              {evert => <= revert}
a -> g b                                                   Ev g (a -> b)
    {fmap evert => <= fmap revert} {distribute => <= distribute}
                             a -> Ev g b

Давайте предположим, что строгий закон выполняется. Мы хотим доказать это fflip . flap = id если и только если evert . revert = id, поэтому мы должны обрабатывать оба направления:

  • Во-первых, давайте предположим, evert . revert = id, Способ обхода квадрата против часовой стрелки a -> g b в g (a -> b) составляет fflip (см. определение fflipEv выше). Поскольку путь против часовой стрелки состоит из трех изоморфизмов, отсюда следует, что fflip имеет обратную поскольку flap его левый обратный (по жесткому закону), он также должен быть обратным. Следовательно fflip . flap = id,

  • Во-вторых, давайте предположим, fflip . flap = id, Опять против часовой стрелки от a -> g b в g (a -> b) является fflip, но теперь мы знаем, что у него есть обратное, а именно flap, Отсюда следует, что каждая из функций, составленных для составления пути против часовой стрелки, должна иметь обратную. В частности, revert должен иметь обратную поскольку evert его обратное справа (по жесткому закону), оно также должно быть обратным. Следовательно, evert . revert = id,

Приведенные выше результаты позволяют нам точно определить, где Rigid стоит по отношению к Distributive, Жесткий функтор является потенциальным дистрибутивом, за исключением того, что он следует только тождественному закону дистрибутива, а не составному. Изготовление fflip изоморфизм, с flap как обратное, равносильно обновлению Rigid в Distributive,

Разные замечания

  • Смотря на fflip а также flap с монадической точки зрения можно сказать, что жесткие монады снабжены инъективным преобразованием стрел Клейсли в статические стрелы. С помощью дистрибутивных монад преобразование преобразуется в изоморфизм, который является обобщением того, как Applicative а также Monad эквивалентны для Reader,

  • extractors конденсирует многое из того, что Distributive около. Для любого дистрибутивного функтора g, Существует g (g a -> a) значение, в котором каждая позиция заполнена соответствующим g a -> a функция экстрактора. Кажется точным сказать, что когда мы переходим от Distributive в Rigid мы теряем эту гарантию того, что положение и экстрактор будут совпадать, а вместе с ним и способность восстанавливать адекватную функторную форму из ничего. В этом контексте стоит еще раз взглянуть на extractors реализация для Sel рано в этом ответе. Любые a -> r функция соответствует Sel r a -> a экстрактор, что означает, что обычно будет множество экстракторов, которые мы не можем перечислить, поэтому мы должны довольствоваться неизоморфными fflip а также infuse (задним числом, const что проявляется в реализации extractors уже раздает игру). Это немного похоже на отсутствие Traversable экземпляр для функций. (В этом случае, однако, есть способ обмануть, если тип домена функции перечислим, Data.Universe стиль. Я не уверен, существует ли такой обходной путь, каким бы непрактичным он ни был, Sel.)

  • Я получил результаты о revert изоморфизм для Distributive в значительной степени за счет отражения, как разложение формы и содержания Traversable Дуальный класс, работает. (Очень читаемая статья, которая исследует тему формы и содержания, - " Понимание идиоматических обходов назад и вперед", автор Bird et. Al.). Хотя более подробное описание этого вопроса, вероятно, лучше оставить для отдельного поста, здесь стоит задать хотя бы один вопрос: соответствует ли понятие, аналогичное Rigid иметь смысл для Traversable? Я верю, что это так, хотя я чувствую, что это звучит менее полезно, чем Rigid возможно. Одним из примеров "жесткой" псевдопереходности может быть структура данных, снабженная обходом, который дублирует эффекты, но затем отбрасывает соответствующие дубликаты элементов при перестройке структуры под аппликативным уровнем, так что следует закону идентичности - но не композиционный.

  • Говоря о revert, Ev Конструкция сама по себе довольно значима: это кодировка свободного дистрибутивного функтора. В частности, evert а также revert сопоставимы с liftF а также retract для свободных монад, а также для аналогичных функций для других свободных конструкций. (В таком контексте revert быть полной противоположностью evert намеки на то, как сильно Distributive является. В некоторых случаях для опровержения более обычным является отказ от информации, как это происходит в общем случае Rigid.)

  • Наконец, но не в последнюю очередь, есть еще один способ понять смысл Ev: это означает, что полиморфный тип экстрактора представляет собой распределительный функтор, в Representable смысл, с evert соответствует index, а также revert, чтобы tabulate, К сожалению, количественное определение делает очень неловким, чтобы выразить это в Хаскеле с фактическим Representable интерфейс. (Это симптоматично, что я должен был достичь unsafeCoerce дать Ev это естественно Rigid а также Distributive случаи.) Если это служит утешением, это не будет ужасно практичным представлением в любом случае: если у меня уже есть полиморфный экстрактор в руках, мне на самом деле не нужно index для извлечения значений.

Все мы знакомы с Traversable typeclass, который можно свести к следующему:

class Functor t => Traversable t
  where
  sequenceA :: Applicative f => t (f a) -> f (t a)

Это использует концепцию Applicativeфунктор. Есть только закономерное усиление категориального понятия, лежащего в основеApplicative это выглядит так:

-- Laxities of a lax monoidal endofunctor on Hask under (,)
zip :: Applicative f => (f a, f b) -> f (a, b)
zip = uncurry $ liftA2 (,)

husk :: Applicative f => () -> f ()
husk = pure

-- Oplaxities of an oplax monoidal endofunctor on ... (this is trivial for all endofunctors on Hask)
unzip :: Functor f => f (a, b) -> (f a, f b)
unzip fab = (fst <$> fab, snd <$> fab)

unhusk :: f () -> ()
unhusk = const ()

-- The class
class Applicative f => StrongApplicative f

-- The laws
-- zip . unzip = id
-- unzip . zip = id
-- husk . unhusk = id
-- unhusk . husk = id -- this one is trivial

Связанный вопрос и ответы на него содержат более подробную информацию, но суть в том, что StrongApplicatives моделируют понятие "фиксированного размера" для функторов. Этот класс типов имеет интересную связь сRepresentableфункторы. Для справки,Representable является:

class Functor f => Representable x f | f -> x
  where
  rep :: f a -> (x -> a)
  unrep :: (x -> a) -> f a

instance Representable a ((->) a)
  where
  rep = id
  unrep = id

Аргумент от @Daniel Вагнер показывает, чтоStrongApplicative является обобщением Representable, в этом каждый Representable является StrongApplicative. Есть лиStrongApplicatives, которые не Representable пока не ясно.

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

class Functor f => Something f
  where
  unsequence :: StrongApplicative f => f (t a) -> t (f a)

Так уж случилось, что (->) a это StrongApplicative, и на самом деле репрезентативный экземпляр (извините за каламбур) рода Representable StrongApplicativeфункторы. Следовательно, мы можем написать вашinject/promote операция как:

promote :: Something f => (a -> f b) -> f (a -> b)
promote = unsequence

Мы упоминали ранее StrongApplicative является суперклассом семейства Representativeфункторы. Из изучения типаunsequence, очевидно, что чем сильнее ограничение, которое мы накладываем на полиморфный аппликатив, тем легче будет реализовать unsequence (и, следовательно, большее количество экземпляров результирующего класса).

Таким образом, в некотором смысле существует иерархия "разрушаемых" функторов, которая течет в направлении, противоположном иерархии аппликативных эффектов, по отношению к которым вы, возможно, захотите устранить их. Иерархия "внутренних" функторов будет выглядеть так:

Functor f => Applicative f => StrongApplicative f => Representable x f

И соответствующая иерархия detraversable/distributive functors может выглядеть так:

Distributive t <= ADistributive t <= SADistributive t <= RDistributive t

С определениями:

class RDistributive t
  where
  rdistribute :: Representable x f => f (t a) -> t (f a)

  default rdistribute :: (SADistributive t, StrongApplicative f) => f (t a) -> t (f a)
  rdistribute = sadistribute

class RDistributive t => SADistributive t
  where
  sadistribute :: StrongApplicative f => f (t a) -> t (f a)

  default sadistribute :: (ADistributive t, Applicative f) => f (t a) -> t (f a)
  sadistribute = adistribute

class SADistributive t => ADistributive t
  where
  adistribute :: Applicative f => f (t a) -> t (f a)

  default adistribute :: (Distributive t, Functor f) => f (t a) -> t (f a)
  adistribute = distribute

class ADistributive t => Distributive t
  where
  distribute :: Functor f => f (t a) -> t (f a)

Наше определение promote можно обобщить, чтобы зависеть от RDistributive (поскольку (->) a сам по себе действительно является представимым функтором):

promote :: RDistributive f => (a -> f b) -> f (a -> b)
promote = rdistribute

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

data Pair a = Pair { pfst :: a, psnd :: a }
  deriving Functor

instance RDistributive Pair
instance SADistributive Pair
instance ADistributive Pair
instance Distributive Pair
  where
  distribute x = Pair (pfst <$> x) (psnd <$> x)

Конечно, если вы сильно потребуете полиморфный "внутренний функтор", например Representable x f в RDistributiveвозможны такие случаи:

newtype Weird r a = Weird { runWeird :: (a -> r) -> a }
  deriving Functor

instance RDistributive (Weird r)
  where
  rdistribute = fmap unrep . promoteWeird . rep
    where
    promoteWeird :: (x -> Weird r a) -> Weird r (x -> a)
    promoteWeird f = fmap (. f) $ Weird $ \k m -> m `runWeird` \a -> k (const a)

ЗАДАЧА: проверьте, где (если где-либо) в иерархии попадают все другие примеры жестких функторов.

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

Вероятно, стоит подумать о некоторых законах для этих непроходимых классов типов. Напрашивается очевидныйsequence . unsequence = id а также unsequence . sequence = id везде, где функтор поддерживает оба Traversable а также Untraverse.

Также стоит упомянуть, что взаимодействие "закона распределения" функторов с монадами и комонадами достаточно хорошо изучено, так что это может иметь некоторое отношение к обсуждению монад в ваших сообщениях.

Другие вопросы по тегам