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] над минимальным (двухэлементным идемпотентным) полукольцом единичной характеристки. Особый же мой интерес вызывают монады инкапсюлирующие квантовые процессы, индексированые над комплексными числами.
From:
Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
User
Account name:
Password:
If you don't have an account you can create one now.
Subject:
HTML doesn't work in the subject.

Message:

 
Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.

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 Jul. 20th, 2017 10:29 pm
Powered by Dreamwidth Studios