gds (gds) wrote,
gds
gds

А теперь мы займёмся профанацией. Особо-приёбистым "дважды крутым мудакам" просьба не читать. nivanych не соберётся никак, поэтому приходится мне.
Речь пойдёт про индукцию и коиндукцию, кое-как в применении к функциональным языкам программирования. Но чуть-чуть.

[Ко]индукция -- общие принципы протаскивания утверждений по термам, заданным [ко]алгебрами.
Алгебра -- набор операций, из 0..n значений данного типа создающих одно значение этого типа. (Когда есть операция, берущая 0 значений, т.е. константный конструктор, эта алгебра хорошая, "начальная".)
Коалгебра -- способ из одного значения определённого типа определить, какой операцией оно было создано и из каких 0..n значений данного типа. (Когда есть вариант, содержащий 0 значений, эта коалгебра хорошая, "терминальная".)
Примеры:
1. Множество действительных чисел и различные элементарные математические функции -- алгебра. Не коалгебра хотя бы потому, что вы не сможете определить, является ли число двенадцать суммой именно семи и пяти (респект авторам лепросказок и tumarkin).
2. Списки в функциональных языках обладают свойствами как алгебры, так и коалгебры: можно и создать список из начального пустого списка и операции приклеивания бошки, и посмотреть, чем же список является (пустой он или же состоит из элемента, приклеенного к хвосту).
Ещё интересно, что при наличии рекурсивных значений не всякий список можно создать индуктивно (пример -- let rec x = 1 :: x), но всякий список можно разрушить коиндуктивно.
3. Поток событий от вашего любимого оконного менеджера, если его моделировать математически, является коалгеброй: из состояния мира (или из хендла окна) мы сможем получить следующее событие, но там неприменим вопрос в стиле "из каких будущих событий является сложенным текущее состояние окна" -- состояние просто есть, и мы его можем просто "разрушать" (какими-нибудь GetMessage в случае венды, например).

Ещё интересным является то, что коалгебру можно кодировать значениями с типом x -> T x, и это кодирование остаётся приемлемым независимо от ленивости языка программирования, так как имеется лямбда-абстракция в типе.

Зачастую тип T будет представляться индуктивным типом.
Однако, для бесконечных потоков, тип T может быть туплом из пользовательского типа A, значения которого будут возвращаться при разрушении, и из нового значения нашей коалгебры, то есть,
type infinite_stream 'a = ('a * infinite_stream 'a);


Например, если рассмотрим окамловские Stream как коалгебру, в качестве T возьмём следующий тип:

# type stream_coalgebra 'a = [ End_of_stream | Elem of 'a and Stream.t 'a ];
type stream_coalgebra 'a = [ End_of_stream | Elem of 'a and Stream.t 'a ]

# value (stream_destruct : Stream.t 'a -> stream_coalgebra 'a) strm =
    try (Elem (Stream.next strm) strm)
    with [Stream.Failure -> End_of_stream]
  ;
value stream_destruct : Stream.t 'a -> stream_coalgebra 'a = <fun>


(кодирование нечестное из-за мутабельности значений типа Stream.t, но это не мешает иллюстрации)

Пака.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 32 comments
Ну вот узнали мы, что такие-то конструкции можно назвать таким-то словом. А дальше-то что? Какой от этого профит? Может, есть какие-нибудь интересные теоремы или следствия, могущие пригодиться при работе с такими конструкциями?
Гомоморфизм от начальных алгебр называется катаморфизмом и представляет собой обобщение очень многих схем рекурсии, которые при правильном применении помогают во всяком reasoning о программе.
Гомоморфизм к терминальным коалгебрам (грубо говоря, генераторов данных с таким-то состоянием, например, разных автоматов) называется анаморфизмом и есть обобщение схем корекурсии, то есть, генерации чего-то-там, и в частности, всякие unfold'ы.
Отлично, слов стало еще больше. А толку?
Конечно, я описал очень кратко, с основной целью выделить некоторые ключевые слова, как начальные алгебры(initial algebras), терминальные или финальные коалгебры (terminal or final coalgebras), катаморфизм (catamorphism), анаморфизм (anamorphism), схемы рекурсии (recursion schemes) или корекурсии. Вообще, в двух предложениях это не описать.

Многие комбинаторы, которые придумываются в ходе разработки, уже рассмотрены в теории и было бы полезно это знать, чтобы не придумывать слишком много велосипедов. Скажем, если конкретное выражение удаётся выразить, как катаморфизм (а уже давно есть и описаны достаточно неплохо работающие процедуры вывода типа (ко)рекурсии), из этого следует очень многое полезное. Например, завершимость процедуры, или же, возможность довольно круто соптимизировать, даже если оно и ленивое. Иногда это бывает просто удобно при разработке. Да и знать будет не лишним.

thedeemon

8 years ago

Вот тут человек созвучную моим вопросам мысль выражает:
http://algebraic-brain.livejournal.com/110185.html?thread=807785#t807785
Для меня теория категорий абсолютно неинструментальна сейчас, то есть "неприложима", "неприкладная". Только мечты о ее приложениях, но до этого еще пахать и пахать.
Этот пост был действительно "теоретически-терминологическим", но кое-кто реквестировал "даёшь коиндукцию за 21 минуту" -- и я оформил.

Для меня теория категорий -- это такие зародыши интуиции. Типа как центры кристаллизации в насыщенном растворе, или как GC roots для сборщика мусора. Это то, от чего можно попробовать начать идти в рассуждениях. Не более.

Кое-какие интуитивные штуки мне стоило бы вербализовать. Однако весьма сложно вытаскивать подобное, да ещё и формулировать в виде текста. Но я постараюсь. Соберу примеров на пост -- и сразу. Будет скорее не про теорию категорий, а ближе к {,ко}{индукции,рекурсии,данным}.

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

little_arhat

8 years ago

gds

8 years ago

thedeemon

8 years ago

nivanych

8 years ago

Понимать что-то в общем виде всегда было только полезно - придумывать конкретную реализацию становится проще, чем без этого понимания.
Ну и кое-какие приложения есть, хотя и слабоватые.
Те же классические монады в хацкеле, это пока откровенно слабо.
Хотя и сейчас уже делаются более корректные хацкельные библиотеки про категорное, к которым претензий (в рамках возможного и удобно используемого в языке) уже нет.
А почему к вашейссылке доступзакрыт? Там мат?

thedeemon

5 years ago

andybil

5 years ago

thedeemon

5 years ago

andybil

5 years ago

thedeemon

5 years ago

andybil

5 years ago

thedeemon

5 years ago

fold обобщать на какие-нибудь другие структуры, кроме списков, по аналогии.
Для этого умных слов знать не надо, берешь и делаешь.

metaclass

8 years ago

ждем продолжения!
Правильной дорогой идете, товарищи.
Ну как причем - такой же бессмысленный и беспощадный. Эстетическое единство - неужели не ощущаете?
в соап нет эстетики, поэтому подобного единства быть не может.

andybil

5 years ago