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

Question

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Примеры функторов, которые «вводят»: F t = (t,t,t) или F t = c -> (t,t) где c - постоянный тип. Функторы F t = c (постоянный функтор) или F t = (c,t) не являются «связанными» (т. Е. Не имеют «инъекции»). Продолжающий функтор F t = (t -> r) -> r также, похоже, не имеет inject.

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

До сих пор я мог показать, что «инъекция» подразумевает «fbind» для любой монады M.

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

• он наведен

point :: t -> F t

• если F является «связующим» и применимым, тогда F также является монадой

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

• если Р «Привязываемый» и А любой profunctor то (про) функтор G t = A t -> F t является связываемый

• Идентификационный функтор связывается.

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

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

• Есть ли другие свойства функтора «F», которые следуют из существования «инъекции»?

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

Answer 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 не являются жесткими.

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

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

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

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

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

В ответе на What is the general case of QuickCheck's promote function? также перечислены конструкции жестких функторов.

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

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

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

Мы можем использовать fbind иметь монадических операции, которые возвращают более одного результата одноместную (или, в более общем плане, жесткий функтор-FUL монадических результатов), для любой монады 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 не являются жесткими. Это снова показывает, что жесткость в некотором смысле более сильная, чем монадичность.