akuklev: (ДР Цертуса 2011)
[personal profile] akuklev
Как выясняется, есть глубокая аналогия между монадическими эффектами и индуктивными типами. А что соответствует с эффектной стороны высшим индуктивным типам? Мне кажется, у меня есть ответ на этот вопрос для важного частного случая.

Давайте начнём с моноида. Для наших рассуждений удобно сказать, что моноид это такая структура (ею могут быть оснащены множества), которая сопоставляет цепочкам элементов этого типа "a ∘ b ∘ c" (включая пустую цепочку) элемент этого типа, притом ассоциативным образом:
@Structure WMonoid[T : *]:
  reduce(l : List[T]) : T
  associativity : /* complicated proposition */


Нейтральный элемент моноида восстанавливается как reduce(nil). Ещё бывает, что моноид содержит нулевой элемент — это такой элемент z, что редукция любой цепочки, содержащей z, равна z. Несложно доказать, что такой элемент может быть только один (z = z ∘ z' = z). Для моноида натуральных (или любых других) чисел по умножению таким элементом как раз является ноль.

Монада это уже не структура на типе, а на параметризованном типе M[T] (то есть, отображении M : * -> *), где можно ассоциативно редуцировать цепочки "f ∘ g" отображений f : X -> M[Y], g : Y -> M[Z] со сходящимися на стыках типами, т.е.
@Structure WMonad[M : * -> *]:
  reduce[X Y : *](l : TypeAlignedList[X, Y]) : X -> M(Y)
  associativity : /* complicated proposition */
  
  @Family TypeAlignedList[X Y : Type]:
    nil[T : *] : TypeAlignedList[T, T]
    succ[X Y Z : *](
      head : Y -> M(Z)
      tail : TypeAlignedList[X, Y]
    ) : TypeAlignedList[X, Z]

Стандартная монадная операция return[T]: T -> M[T] восстанавливается как reduce(nil[T]). Монады тоже бывают снабжены нулевым объектом, точнее семейством нулевых объектов zero[T] : M[T] со всё тем же свойством, что ежели такой попадается где-то в цепочке l : TypeAlignedList[X, Y], то contract(l) = zero[Y].

Две очень важных в программировании монады снабжены таким объектом — монада Partial[T] частичных вычислений возвращающих T или зависающих, и монада MultiPartial[T] вычислений, постепенно перечисляющих (порядок и повторения неважны) какое-то счётное подмножество типа T. И в первом и во втором случае нулевым элементом служит зависающее (т.е. никогда ничего не выдающее) вычисление.

Указанные монады обладают дополнительной крайне интересной особенностью: для них можно задать частично определённую операцию (коммутативную, ассоциативную, идемпотентную и с нулевым элементом в качестве нейтрального) «запуска наперегонки» f + g, будем называть её join. В случае Multipartial[T] эта операция задана для любых двух f и g совпадающего типа, и объединяет выдаваемые ими множества. В случае Partial[T] эта операция определена только для таких f и g, для которых мы наперёд знаем (можем доказать), что если они оба не зависают, то выдают равные результаты. Вот эту самую операцию интересно добавить в структуру монады с нулём. Примем для полученной структуры рабочее название джойнада (как выяснилось, уже занято, но хрен с ним пока).

Итак, джойнада задаётся на конкретном пунктированном спектре M(n : Nat)[T], т.е. семействе типов состоящем из произвольного типа M(0)[T] с выделенной точкой zero и типов M(n)[T] являющихся подтипами n-элементных кортежей элементов M(0)[T], таких что операция удлинения кортежа p : M(n)[T] на единицу путём вставки нуля на k-той позиции отображает в равные внутри M(n + 1)[T] независимо от k, и равные кортежу из нулей в M(n + 1), если исходный кортеж был из нулей. Таким образом эти операции задают структурные отображения Σ(M(n)) -> M(n + 1), оправдывающие использование названия “спектр”. Идейный смысл типов M(n)[T] в том, что это joinable пары, тройки и т.д. элементов M(0)[T]. Для монады Multipartial[T] joinable любые пары, тройки и т.д. элементов. Для монады Partial[T] — только пары вида (f, 0), (0, f) и (f, g) если f = g. Если спектр представляет из себя просто спектр поднятий M(0), то joinable только кортежи, в которых не более одного элемента отлично от нуля.

Операция редукции высшей монады должна сжимать уже не type-aligned-цепи, но type-aligned-многочлены, где элементы склеиваются не только операцией последовательной композиции ∘, но и операцией конкурентного джойна +, а выполняться должна не только ассоциативность ∘, но ещё и ассоциокоммутативность + и дистрибутивность первого относительно второго. Заметим что любая монада с нулевым элементом над параметрическим типом M[T] тривиальным образом является высшей пунктированной монадой над спектром поднятий M[T], т.к. в спектре поднятий, как уже сказано выше, запрещено использовать + в любых нетривиальных случаях.

Очень интересен аналог MonadFix (монада с дополнительной операцией, допускающей рекурсивные определения отображений X -> M[Y]) для джойнад. Идейно это в точности монады, допускающие интерпретацию Join Calculus (варианта асинхронного пи-исчисления, особенно близкого к линейной логике и Actor Model), там как раз рекурсивные определения содержащие определения кортежей частичных элементов @def f(x : X) + g(y : Y): /* определение */, т.е. элементов высших ступеней спектра, не являющихся тривиальным поднятием с более низких уровней.

А сейчас я расскажу, чем меня особенно зацепила эта конструкция. Дело в том, что существует обобщение монад — индексированные (над моноидом) монады, где у нас операция контракции не только сжимает цепочку, но ещё и “аккумулирует веса” элементов цепи. Так вот, разумеется вот эти вот придуманные выше высшие пунктированные монады тоже можно индексировать так, чтобы операция сжатия не только “вычисляла” полином, но и “аккумулировала веса”. Только тип весов при этом должен обладать не структурой моноида, а структурой “обобщённого полукольца”, а именно “алгебры над спектром сфер”, как её определяет Ален Конн в “Absolute algebra and Segal's gamma sets”. В частности любая такая монада автоматически индексирована над “полем с одним элементом” (а результат сжатия имеет нулевой вес, если он сам нулевой, и единичный во всех остальных случаях; комбинация набора элементов при помощи сложения допустима только если не более одного из них имеет ненулевой вес), а монады Partial[T] и MultiPartial[T] над минимальным (двухэлементным идемпотентным) полукольцом единичной характеристки. Особый же мой интерес вызывают монады инкапсюлирующие квантовые процессы, индексированые над комплексными числами.

Date: 2016-11-12 05:45 pm (UTC)
From: [identity profile] vit-r.livejournal.com
В программировании манады будут важны, когда система останется стабильной при случайных ошибках.

Date: 2016-11-12 07:12 pm (UTC)
ext_615659: (ДР Цертуса 2011)
From: [identity profile] akuklev.livejournal.com
Вполне вероятно, я тут не предсказатель. Может и вообще никогда не будут важны, кроме нишевых применений. Но честно говоря, меня мало интересует вопрос актуальности темы в прикладной деятельности прямо сейчас, если тема интересна мне уже чисто математически.

Date: 2016-11-12 07:18 pm (UTC)
From: [identity profile] vit-r.livejournal.com
О том, что это красиво, никто не спорит. :-)

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 21st, 2017 03:37 pm
Powered by Dreamwidth Studios