Observations

Вчера... вчера я где-то в полчетвёртого зафигачил новый парсер, запустил тесты на ночь на стейджинге, и в шестом часу ломанулся опять в город, на, блин, встречу категорщиков. До города-то доехал нормально, но в городе застрял на всяких там улицах. Да затрахало. Последний раз (в этом году). Заявился в офис Прези в 7:15, меня уже искали.

Ну офис ладно, мы проникли в конце концов; нас было шестеро в сумме. В комнате, куда мы пришли, на доске были остатки урока венгерского, и я обнаружил, что ха, на этом-то уровне mindent tudom. Должны были проходить третью главу книжечки Пирса - typed lambdas, categorical style. Ну и чо. Собралось опять половина новых; объясняй им, что за пределы такие... нет, что такое декартово произведение! И что за суммы такие! Короче, протрахались минут сорок с этой ерундой, потом как-то хитростью (без сопряженных функторов) протащили экспоненту.

Тут ещё новенький, Сергей, всё норовил возразить, в русском стиле, мол, нам эти ваши абстракции и даром не нать, у нас всё множества кругом, и можно ограничить дискурс малыми категориями - теория множеств, дескать, и есть основа вычислительных наук. На предложение охарактеризовать Cat было молчание. Я пытался добиться, какая польза вычислениям от аксиомы выбора. потом нарисовал пример неизмеримого подмножества отрезка [0,1]. Молчанье.

Ну ладно. Я уже совсем был почти pissed off. Плюс голодный; обещанной еды Прези не предоставило.

С божией и шахафовой помощью втянулись, наконец, в книжку. Дошли аж до примерно 20-й строки. Потом мне стали объяснять рулеса типовой лямбды; в частности, постоянно фигурировала какая-то гамма. У меня в книжке никакой гаммы не было, и я стал приставать, откуда взялась эта невидимая гамма.

И тут оказалось, что гамма невидима только у меня в книжке, а у остальных в книжке гамма есть. Пришлось мне руками вписывать гамму!

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

Я же как этот стал приябываться к каждому рулесу. Ну типа вот вы говорите, что x имеет тип A × B - а это ж изоморфно B &time; A, так оно имеет и этот тип? Или чо? Или как?

Меня долго убеждали, что тип парсится в процессе валидации фразы, и определяется однозначно, но тут я совсем озверел - как вы нахер определите однозначно, если пределы в категории, как и вообще все сопряженные, определены с точностью до изоморфизма? Это же бред, почему unit имеет тип Unit, а не Unit^Unit × Unit^X?

И тут Шахаф сказал.

Дык. Для этого Воеводский HoTT и впендюрил, что типы не однозначно, а с точностью до изоморфизма определяются.

О блин. Мы вышли на гомотопическую дорожку. Уже Дан Пипони книжку читает, и ещё кто-то там в Гугле. Короче, надо всё бросать и переучиваться заново. Потому что у Пирса в третьей главе булшит. И что, никто не видел? Тьфу.

Ну и вот, и был уже десятый час, и я сказал всё, у меня завтра в 7 класс, пора. Подцепил Мэтью и Шахафа, потому что блин я ценю каждый момент когда можно поговорить с умным человеком, а Шахаф просто блистает. Он скромен до ужаса, но вот с кем бы я работал.

И вот едем мы, я какую-то музычку по радио поставил, и обсуждаем какую-то хрень ну типа как бы нам перекатиться с семинаром в Заливную, желательно в Маунтин Вью (и другого Мэтью ещё притащить - тоже израильтянин); и с Валерией да с Дэном согласовать, чтоб всем удобно было.

И тут Шахаф говорит - а, а кстати, в хаскеле все монады происходят от карриинга.

Чо?! О блин! Вот чо! Это же representable functors! Главное - пределы сохранять.

Перевариваю.

Ну и заодно, к слову, посмотрел как Максим жжет глаголом на киевском fprog:

http://www.youtube.com/watch?v=lJlqQDMpY3I&feature=youtu.be&a

Ну как мы уже поняли, всё не так просто. Но и не так уж запрещено.

Вот возьмём-ка монадку X2, из моего поста.

"Какая ж тут у нас монада? Монада берёт множество X и сопоставляет ему X×X. Монадная единица - диагональ (η(x) = (x,x)), а монадное умножение, X×X×X×X → X×X строится, согласно картинкам из начала этой части, из ε: (Y1×Y2, Y1×Y2) →(Y1,Y2) - проектированием по первой и последней координатам. μ(x1,x2,x3,x4) = (x1,x4)."

Так вот, а какие ж бывают алгебры над такой монадой? Нам надо, чтобы был f: A×A → A, соблюдающий условия:

f(a,a) == a

f(f(a1,a2),f(a3,a4)) == f(a1,a4)

Мне вот что-то сдаётся, что в условиях булевости и точечности (ну, скажем, в множествах) только проекция удовлетворяет такому условию. p1(a1,a2) = a1; p2(a1,a2) = a2.

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

Итак, если у нас имеются две категории, C и D, и два функтора, F: C → D и G: D → C, мы говорим, что эти два функтора образуют сопряженную пару, F ⊣ G если имеется взаимно-однозначное соответствие

F(X) → Y

<====>

X → G(Y)

Для сопряженной пары мы вывели два естественных преобразования, η: Id_C → F;G и ε: G;F → Id_D.

Оказывается, если есть такие два естественных преобразования, для пары функторов, то они сопряжены.
Ну и правда, если есть f: F(X) → Y, то приложим к нему G, получим G(f): G(F(X)) → G(Y), и соединим это с ηX: X → G(F(X)), получим ту самую X → G(Y).

То же самое, по симметрии, проделывается и в другую сторону. Вообще, у меня тут половина рассуждений лишняя, потому что зеркальная симметрия ж (никаких бозонов).

Наши ηX и εY обладают чудесными свойствами:



Эти два чудесные свойства получаются в результате применения тех самых соответствий α и β, что были нарисованы в первой серии - попробуйте сами.

У нас есть теперь всё для монады и комонады.

Монада делается путём композиции, T = F;G; это функтор T: C → C. В качестве монадной единицы годится уже появлявшаяся у нас η, а в качестве монадного умножения (a.k.a. flatten) возьмём μX = G(εF(X)): G(F(G(F(X)))) → G(F(X)).

Единица оказывается единицей относительно монадного умножения, и умножение оказывается ассоциативно - всё это следует из описанных выше свойств сопряженных функторов.

Симметрично мы можем определить комонаду, путём композиции U = G;F.

Пример.

Возьмём категории C=Set и D=Set×Set - множества и пары множеств, и два функтора, Δ(X) = (X,X) и Π((X,Y)) = X×Y.

Первый функтор - диагональ, он множеству сопоставляет пару, состоящую из двух экземпляров оного, а второй паре множеств сопоставляет декартово произведение.

Эти два функтора сопряжены, Δ ⊣Π.

А именно, если есть (f1,f2): (X,X) → (Y1, Y2), то это задаёт отображение X →Y1×Y2, и наоборот, отображение в декартово произведение Y1×Y2 задаёт пару отображений, по компонентам.

Какая ж тут у нас монада? Монада берёт множество X и сопоставляет ему X×X. Монадная единица - диагональ (η(x) = (x,x)), а монадное умножение, X×X×X×X → X×X строится, согласно картинкам из начала этой части, из ε: (Y1×Y2, Y1×Y2) →(Y1,Y2) - проектированием по первой и последней координатам. μ(x1,x2,x3,x4) = (x1,x4).

Кто любит симплициальные категории, увидит тут различные краюшки и рёбрушки, но это ладно, это мы лучше не будем трогать.

"Практический смысл" в программировании у этой монады вот какой: есть двоичный флаг; и наши данные от него зависят - в одном случае вызов возвращает Y1, а в другом Y2. Ну и если у нас есть функция, зависящая от того же флага, то нам надо как-то комбинировать и сплющивать; это же Reader Monad, сведённая к двоичному флагу. Ну вот эта монада и есть.

Вопросы?

(Завтра продолжу, хочу показать, как из монады можно построить сопряженную пару, и не одну.)

В разных там WriterMonad требуется, чтобы внутре был моноид, и возникает иной раз такое ощущение, что и везде нужен моноид. Ан нет, бывает и полугруппы достаточно.

Скажем, Option[T], где Т - полугруппа, можно считать моноидом - к полугруппе присоединяется внешний нуль.

def sum(maybeX; Option[T])(maybeY: Option[T]) = maybeX match {
  case Some(x) => maybeY match {
    case Some(y) => Some(x+y)
    case None    => Some(x) }
  case None => maybeY
}

Так получается, что тот нуль, что был в T раньше, теперь не будет нулём.

Та же фигня и с мапредьюсом - в качестве типа накапливаемых значений берётся полугруппа, а нуль присоединяется внешний.

Это, заодно, ответ на мой старый вопрос - шо за моноид в мапредьюсе. Да вот этот, с присоединённым нулём.

Mostly Scala 2.10

sassa_nf высказал недоумение, если не больше, по вопросу как это мы вставляем ap между нашими аппликативными штучками, как это? Я думал, э, всё просто.

Протрахался с 7 до 11. Вот код с примером; а текст потом поправлю, спать же уже пора, ё.

  import scala.collection.immutable._

  trait Functor[T[_]]{
    def map[A,B](f:A=>B)(ta:T[A]):T[B]
  }

  trait Applicative[T[_]] extends Functor[T]{
    def pure[A](a:A):T[A]
    def ap[A,B](tf:T[A=>B])(ta:T[A]):T[B]
  }

  implicit def applicablize[A, B](fs: Set[A=>B]) = new {
    def <*>(as: Set[A]) = (for (f <- fs; a <- as) yield f(a)).toSet
  }

  implicit object AppSet extends Applicative[Set] {
    def pure[A](a: A) = Set(a)
    def ap[A,B](fs:Set[A=>B])(as:Set[A]):Set[B] = (for (f <- fs; a <- as) yield f(a)).toSet
    def map[A,B](f:A=>B)(as:Set[A]) = ap(pure(f))(as)
  }

  val p = AppSet.pure((s:String) => "'" + s + "'")
  val p2 = AppSet.pure((first: String) => (second:String) => first + " " + second)
  val names = Set("Jedi", "Michael Valentine")
  p <*> names
  val lasts = Set("Smith", "Frazer")
  p2 <*> names <*> lasts