![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Высшие монады и “поле с одним элементом”
Оригинал взят у ![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
akuklev в Высшие монады и “поле с одним элементом”
akuklev в Высшие монады и “поле с одним элементом”Как выясняется, есть глубокая аналогия между монадическими эффектами и индуктивными типами. А что соответствует с эффектной стороны высшим индуктивным типам? Мне кажется, у меня есть ответ на этот вопрос для важного частного случая.
Давайте начнём с моноида. Для наших рассуждений удобно сказать, что моноид это такая структура (ею могут быть оснащены множества), которая сопоставляет цепочкам элементов этого типа "a ∘ b ∘ c" (включая пустую цепочку) элемент этого типа, притом ассоциативным образом:
Нейтральный объект моноида восстанавливается как contract(nil). Ещё бывает, что моноид содержит нулевой элемент — это такой элемент z, что контракция любой цепочки, содержащей z, равна z. Несложно доказать, что такой элемент может быть только один (z = z ∘ z' = z). Для моноида натуральных (или любых других) чисел по умножению таким элементом как раз является ноль.
Монада это уже не структура на типе, но на параметризованном типе M[T], где можно ассоциативно «сжимать» цепочки "f ∘ g" отображений f : X -> M[Y], g : Y -> M[Z] с подходящими на стыке типами, т.е.
Монадная операция return[T]: T -> M[T] восстанавливается как contract(nil[T]). Монады тоже бывают снабжены нулевым объектом, точнее семейством нулевых объектов zero[T] : M[T] со всё тем же свойством, что ежели такой попадается где-то в цепочке l : TypeAlignedList[X, Y], то contract(l) = zero[Y].
Две очень важных в программировании монады снабжены таким объектом — монада Partial[T] частичных вычислений возвращающих T или зависающих, и монада MultiPartial[T] вычислений, постепенно перечисляющих (порядок и повторения неважны) какое-то счётное подмножество типа T. И в первом и во втором случае нулевым элементом служит зависающее (т.е. никогда ничего не выдающее) вычисление.
Указанные монады обладают дополнительной крайне интересной особенностью: для них можно задать частично определённую операцию (коммутативную, ассоциативную, идемпотентную и с нулевым элементом в качестве нейтрального) «запуска наперегонки» f + g. В случае 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] в том, что это “подлежащие складыанию” пары, тройки и т.д. элементов M(0)[T]. Для монады Multipartial[T] “складыванию подлежат” любые пары, тройки и т.д. элементов. Для монады Partial[T] — только пары вида (f, 0), (0, f) и (f, g) если f = g. Если спектр представляет из себя просто спектр поднятий M(0), то “складыванию подлежат” только кортежи, в которых не более одного элемента отлично от нуля.
Операция “контракции” высшей монады должна сжимать уже не type-aligned-цепи, но type-aligned-многочлены, где элементы склеиваются не только значком ∘, но и значком +, а выполняться должна не только ассоциативность ∘, но ещё и ассоциокоммутативность + и дистрибутивность первого относительно второго. Заметим что любая монада с нулевым элементом над параметрическим типом M[T] тривиальным образом является высшей пунктированной монадой над спектром поднятий M[T], т.к. в спектре поднятий, как уже сказано выше, запрещено использовать + в любых нетривиальных случаях.
А сейчас я расскажу, чем меня особенно зацепила эта конструкция. Дело в том, что существует обобщение монад — индексированные (над моноидом) монады, где у нас операция контракции не только сжимает цепочку, но ещё и “аккумулирует веса” элементов цепи. Так вот, разумеется вот эти вот придуманные выше высшие пунктированные монады тоже можно индексировать так, чтобы операция сжатия не только “вычисляла” полином, но и “аккумулировала веса”. Только тип весов при этом должен обладать не структурой моноида, а структурой “обобщённого полукольца”, а именно “алгебры над спектром сфер”, как её определяет Ален Конн в “Absolute algebra and Segal's gamma sets”. В частности любая такая монада автоматически индексирована над “полем с одним элементом” (а результат сжатия имеет нулевой вес, если он сам нулевой, и единичный во всех остальных случаях; комбинация набора элементов при помощи сложения допустима только если не более одного из них имеет ненулевой вес), а монады Partial[T] и MultiPartial[T] над минимальным (двухэлементным идемпотентным) полукольцом единичной характеристки. Особый же мой интерес вызывают монады инкапсюлирующие квантовые процессы, индексированые над комплексными числами.
Давайте начнём с моноида. Для наших рассуждений удобно сказать, что моноид это такая структура (ею могут быть оснащены множества), которая сопоставляет цепочкам элементов этого типа "a ∘ b ∘ c" (включая пустую цепочку) элемент этого типа, притом ассоциативным образом:
@Structure WMonoid[T : *]: contract(l : List[T]) : T associativity : /* complicated proposition */
Нейтральный объект моноида восстанавливается как contract(nil). Ещё бывает, что моноид содержит нулевой элемент — это такой элемент z, что контракция любой цепочки, содержащей z, равна z. Несложно доказать, что такой элемент может быть только один (z = z ∘ z' = z). Для моноида натуральных (или любых других) чисел по умножению таким элементом как раз является ноль.
Монада это уже не структура на типе, но на параметризованном типе M[T], где можно ассоциативно «сжимать» цепочки "f ∘ g" отображений f : X -> M[Y], g : Y -> M[Z] с подходящими на стыке типами, т.е.
@Structure WMonad[M : * -> *]:
contract[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] восстанавливается как contract(nil[T]). Монады тоже бывают снабжены нулевым объектом, точнее семейством нулевых объектов zero[T] : M[T] со всё тем же свойством, что ежели такой попадается где-то в цепочке l : TypeAlignedList[X, Y], то contract(l) = zero[Y].
Две очень важных в программировании монады снабжены таким объектом — монада Partial[T] частичных вычислений возвращающих T или зависающих, и монада MultiPartial[T] вычислений, постепенно перечисляющих (порядок и повторения неважны) какое-то счётное подмножество типа T. И в первом и во втором случае нулевым элементом служит зависающее (т.е. никогда ничего не выдающее) вычисление.
Указанные монады обладают дополнительной крайне интересной особенностью: для них можно задать частично определённую операцию (коммутативную, ассоциативную, идемпотентную и с нулевым элементом в качестве нейтрального) «запуска наперегонки» f + g. В случае 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] в том, что это “подлежащие складыанию” пары, тройки и т.д. элементов M(0)[T]. Для монады Multipartial[T] “складыванию подлежат” любые пары, тройки и т.д. элементов. Для монады Partial[T] — только пары вида (f, 0), (0, f) и (f, g) если f = g. Если спектр представляет из себя просто спектр поднятий M(0), то “складыванию подлежат” только кортежи, в которых не более одного элемента отлично от нуля.
Операция “контракции” высшей монады должна сжимать уже не type-aligned-цепи, но type-aligned-многочлены, где элементы склеиваются не только значком ∘, но и значком +, а выполняться должна не только ассоциативность ∘, но ещё и ассоциокоммутативность + и дистрибутивность первого относительно второго. Заметим что любая монада с нулевым элементом над параметрическим типом M[T] тривиальным образом является высшей пунктированной монадой над спектром поднятий M[T], т.к. в спектре поднятий, как уже сказано выше, запрещено использовать + в любых нетривиальных случаях.
А сейчас я расскажу, чем меня особенно зацепила эта конструкция. Дело в том, что существует обобщение монад — индексированные (над моноидом) монады, где у нас операция контракции не только сжимает цепочку, но ещё и “аккумулирует веса” элементов цепи. Так вот, разумеется вот эти вот придуманные выше высшие пунктированные монады тоже можно индексировать так, чтобы операция сжатия не только “вычисляла” полином, но и “аккумулировала веса”. Только тип весов при этом должен обладать не структурой моноида, а структурой “обобщённого полукольца”, а именно “алгебры над спектром сфер”, как её определяет Ален Конн в “Absolute algebra and Segal's gamma sets”. В частности любая такая монада автоматически индексирована над “полем с одним элементом” (а результат сжатия имеет нулевой вес, если он сам нулевой, и единичный во всех остальных случаях; комбинация набора элементов при помощи сложения допустима только если не более одного из них имеет ненулевой вес), а монады Partial[T] и MultiPartial[T] над минимальным (двухэлементным идемпотентным) полукольцом единичной характеристки. Особый же мой интерес вызывают монады инкапсюлирующие квантовые процессы, индексированые над комплексными числами.