Категорические вычисления

[thedeemon]

А вот можно ли вычислить ответ на главный вопрос, пользуясь одной лишь теорией категорий? Оказывается, можно. Давным-давно в одной далекой галактике Tatsuya Hagino придумал язык CPL (Categorical Programming Language), а чуть менее давно другой японец Masahiro Sakai сделал годный его интерпретатор. Hagino свою реализацию делал на Лиспе, а Sakai догадался таки задействовать языки программирования - сперва Руби, затем Хаскель (ибо Руби медленный, на Хаскеле в сто раз быстрее заработало). И вот полный текст программы на CPL:

right object 1 with !
end object;

right object prod(a,b) with pair is
  pi1: prod -> a
  pi2: prod -> b
end object;

right object exp(a,b) with curry is
  eval: prod(exp,a) -> b
end object;

left object nat with pr is
  zero: 1 -> nat
  s: nat -> nat
end object;

let add=eval.prod(pr(curry(pi2), curry(s.eval)), I);
let mult=eval.prod(pr(curry(zero.!), curry(add.pair(eval, pi2))), I);
let h = mult . pair(s, I);
simp h.h.h.s.zero;

которая выводит результат
s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.zero
т.е. ровно 42.

Что же тут происходит? В CPL мы начинаем с чистого листа - там изначально нет ни базовых типов, ни каких-либо операций. Зато есть возможность определять универсальные категорные объекты (вот где настоящий объектно-ориентированный язык! :)). В категории у нас есть объекты и есть морфизмы между ними (они же стрелки), подчиняющиеся паре простых правил (наличие и ассоциативность композиции, наличие и годность identity - тождественного морфизма). Я сразу возьму несколько примеров, чтобы на них все примерять. Первый пример категории: объекты - типы данных функционального языка (int, bool, string, etc.), а морфизмы - функции (string_of_int : int -> string, succ : int -> int, etc.). Пример другой категории: объекты - логические высказывания, а стрелки показывают выводимость одного высказывания из другого (have_a_son -> have_a_child, А & B & C -> A...). Третий пример: объекты - натуральные числа, а стрелка соединяет два числа, если первое делится на второе (6 -> 3, 5 -> 5...). Мы можем придумывать какие-то универсальные объекты - они характеризуются наличием определенных связей с другими объектами категории, причем из всех аналогично связанных объектов они "самые-самые": всякий похожий объект связан с нашим уникальным морфизмом. Простейший пример - терминальный объект категории. Это такой объект, в который есть по уникальной стрелке из всех объектов категории. С т.з. универсальности это объект без особенных связей, но всякий похожий объект (а раз никаких особенностей не требуется, то любой объект категории) связан с ним уникальным морфизмом. На CPL это записывается так:

right object 1 with !
end object;

Здесь 1 - название определяемого объекта, ! - название для морфизма, связывающего любой похожий объект (т.е. в данном случае вообще любой объект) с 1, а "right" показывает направление для ! - определяемый объект стоит справа от стрелки:
! : X -> 1
для всех объектов Х.

В категории типов терминальный объект - тип (), он же unit, он же void. Из любого типа Т можно сделать функцию Т -> (), она и станет морфизмом "!". В категории логических высказываний терминальный объект - особое высказывание True, Истина, оно выводится из любого истинного высказывания (то бишь из всех). В категории натуральных чисел, где стрелки означают делимость, терминальный объект - это 1. Всякое натуральное число делится на 1.

Чуть сложнее, но в том же ключе выглядит произведение:

right object prod(a,b) with pair is
  pi1: prod -> a
  pi2: prod -> b
end object;

Объект АхВ (обозначенный тут как prod(a,b)) называется произведением объектов А и В, если из него есть стрелка в А, есть стрелка в В (обозначим их pi1 и pi2), и для любого похожего объекта С (т.е. из которого тоже есть стрелки в А и В) есть стрелка из С в наш объект АхВ. Ее назовем pair, а факт того, что определяемый объект в ней справа (pair: C -> AхB), отметим указанием "right". При этом должна работать ("коммутировать" - разные пути между двумя точками должны определять эквивалентные морфизмы) такая диаграмма:

(пунктиром обозначен морфизм, существование которого должно вытекать из существования стрелок, показанных сплошными линиями)
В категории типов данных произведение типов А и В - это тупл (А,В). Стрелки pi1 и pi2 - это функции fst и snd. Если из некоторого типа С тоже есть две стрелки (функции)
fa :: C -> A
fb :: C -> B
то можно сделать функцию
pair_fa_fb :: C -> (A,B)
pair_fa_fb c = (fa c, fb c)

В категории логических высказываний произведение - это связка И (&). Правила избавления от И выглядят как
A&B -> A
A&B -> B
а правило ввода аналогично pair.

В категории с числами и делимостью произведением АхВ будет наименьшее общее кратное (lowest common multiple) lcm(A,B). Оно делится на А, оно делится на В (т.е. из него есть стрелки в А и В), и любое другое натуральное число, которое тоже делится на А и В, делится на lcm(A,B), т.е. из него есть стрелка в АхВ.

Если чуть углубиться в теорию, то произведение prod(A,B) - это функтор СхС -> С, являющийся правым сопряженным для диагонального функтора С -> СхС (и указание "right object" на самом деле говорит о том, что определяемый функтор - именно правый сопряженный), и значит для объектов А, В и С имеется натуральный изоморфизм между множествами стрелок:
Hom(C,A) х HomC(C,B) ~= Hom(C, prod(A,B))
другими словами для любой пары стрелок C -> A и С -> В есть соответствующая им стрелка С -> prod(A,B), это и есть pair. Если же в качестве С подставить сам prod(A,B), получим
Hom(prod(A,B),A) х HomC(prod(A,B),B) ~= Hom(prod(A,B), prod(A,B))
Здесь слева можно найти наши стрелки-проекции pi1 и pi2 и обнаружить, что
pair(pi1, pi2) = I
Т.е. свойства произведения, которые в иных языках спецификаций нужно выражать явно аксиомами, здесь вытекают сами из понятия сопряженных функторов, на которых все строится. Кстати, стрелки pi1 и pi2 тут становятся естественными преобразованиями. Но это если углубляться в теорию, а мы этого делать не будем. :)

Теперь, раз у нас все строится из стрелок, соединящих пары объектов, всегда есть два возможных направления для стрелки - туда и сюда. Что будет, если взять и стрелки все поразворачивать? Если так сделать в определении какого-то объекта, получим двойственный (dual) к нему объект. Например, возьмем и развернем все стрелки в определении произведения. Получим вот что:

Это копроизведение - А+В. На CPL оно тоже определяется путем разворота всех стрелок:

left object coprod(a,b) with case is
  in1: a -> coprod
  in2: b -> coprod
end object;

Стрелки проекций pi1 и pi2 превратились в стрелки инъекций in1 и in2, стрелка-факторизатор pair превратилась в стрелку case, идущую в обратном направлении, и теперь это left object, и он вроде как правда левый сопряженный функтор для диагонального.

В категории типов данных копроизведение - это sum type, А+В (в хаскеле - Either A B). Конструкторы Left и Right в Either как раз служат стрелками in1 и in2. Универсальность диктует, что если есть другой похожий объект С, в который тоже есть стрелки из А и В, то должна быть и уникальная стрелка А+В -> С. Действительно, если у нас есть функции
fa :: A -> C
fb :: B -> C
то можно построить функцию

g_fa_fb :: Either A B -> C
g_fa_fb x = case x of 
  Left a -> fa a
  Right b -> fb b

В категории логических высказываний копроизведение - это связка ИЛИ. Правила ввода выглядят в точности как in1 и in2, а правило избавления - в точности как case.

В категории натуральных чисел с делимостью в качестве стрелок копроизведение А и В - это наибольший общий делитель gcd(A,B). На него делится А, на него делится В (стрелки in1, in2), и для любого другого числа С, на которое тоже делятся А и В (т.е. любой общий делитель А и В), gcd(A,B) делится на С, это стрелка-факторизатор case.

Еще один полезный универсальный объект - экспоненциал. Вот его фотокарточка:

Для двух объектов А и В их экспоненциал exp(A,B) характеризуется наличием морфизма eval из произведения exp(A,B) и A в B, а универсальность диктует, что для любого похожего объекта С, для которого тоже есть такой морфизм f из СхА в В, должен быть уникальный морфизм
curry(f): C -> exp(A,B)
На CPL это записывается очень просто:

right object exp(a,b) with curry is
  eval: prod(exp,a) -> b
end object;

В категории типов данных exp(A,B) - это функция из А в В. Тогда eval получает данную функцию и ее аргумент типа А, и вычисляет результат типа В (отсюда название). А curry, имея функцию типа
СхА -> В
и значение типа С, делает нам функцию из А в В, это простое каррирование.

В категории логических высказываний exp(A,B) - это импликация А=>B. Стрелки curry и eval полностью совпадают с логическими правилами ввода и избавления от импликации. Например, по правилу избавления из пары утверждений А=>B и А выводится В.

В категории чисел и делимости exp(A,B) = lcm(a,b) / a. Именно такое определение позволяет всем стрелкам на диаграмме сходиться как надо. (Update: тут я наврал, функция не такая, чуть сложнее.) Например, если А=30, В=35 и С=2310, то
exp(A,B) = lcm(30,35)/30 = 210/30 = 7
exp(A,B) x A = lcm(7,30) = 210
C x A = lcm(2310, 30) = 2310
210 делится на 35, 2310 делится на 35, 2310 делится на 210, 2310 делится на 7, все стрелки на месте.

Солнце клонится к закату, а мы еще не приблизились к вычислениям. Давайте определим натуральные числа. Это объект nat, характеризуемый наличием двух стрелок: zero из 1 в него, и succ из nat в nat (для краткости будет просто s), да такой, что всякий похожий объект с ним связан стрелкой-факторизатором pr (означающей "примитивную рекурсию"). И вот такая картинка должна коммутировать:

На CPL это опять очень просто:

left object nat with pr is
  zero: 1 -> nat
  s: nat -> nat
end object;

Интепретатор CPL умеет без лишних слов понимать про устройство диаграмм, соответствующих описываемым объектам, и из них (и свойств сопряженных функторов) выводить связи между разными морфизмами. Определив объект, можно попросить интерпретатор показать, что он про сей объект понял. Вот, что он выдает про наши объекты (самое интересное см. в графе equations, точка означает композицию стрелок):

> show object prod
right object prod(+,+)
- natural transformations:
    pi1: prod(*a,*b) -> *a
    pi2: prod(*a,*b) -> *b
- factorizer:
    f0: *a -> *b  f1: *a -> *c
    ------------------------------
    pair(f0,f1): *a -> prod(*b,*c)
- equations:
    (REQ1): pi1.pair(f0,f1)=f0
    (REQ2): pi2.pair(f0,f1)=f1
    (RFEQ): prod(f0,f1)=pair(f0.pi1,f1.pi2)
    (RCEQ): pi1.g=f0 & pi2.g=f1 => g=pair(f0,f1)
- unconditioned: yes
- productive: (yes,yes)

> show object coprod
left object coprod(+,+)
- natural transformations:
    in1: *a -> coprod(*a,*b)
    in2: *b -> coprod(*a,*b)
- factorizer:
    f0: *b -> *a  f1: *c -> *a
    --------------------------------
    case(f0,f1): coprod(*b,*c) -> *a
- equations:
    (LEQ1): case(f0,f1).in1=f0
    (LEQ2): case(f0,f1).in2=f1
    (LFEQ): coprod(f0,f1)=case(in1.f0,in2.f1)
    (LCEQ): g.in1=f0 & g.in2=f1 => g=case(f0,f1)
- unconditioned: yes
- productive: (no,no)

> show object exp
right object exp(-,+)
- natural transformations:
    eval: prod(exp(*a,*b),*a) -> *b
- factorizer:
    f0: prod(*a,*b) -> *c
    ---------------------------
    curry(f0): *a -> exp(*b,*c)
- equations:
    (REQ1): eval.prod(curry(f0),I)=f0
    (RFEQ): exp(f0,f1)=curry(f1.eval.prod(I,f0))
    (RCEQ): eval.prod(g,I)=f0 => g=curry(f0)
- unconditioned: yes
- productive: (no,no)

> show object nat
left object nat
- natural transformations:
    zero: 1 -> nat
    s: nat -> nat
- factorizer:
    f0: 1 -> *a  f1: *a -> *a
    -------------------------
    pr(f0,f1): nat -> *a
- equations:
    (LEQ1): pr(f0,f1).zero=f0
    (LEQ2): pr(f0,f1).s=f1.pr(f0,f1)
    (LFEQ): nat=pr(zero,s)
    (LCEQ): g.zero=f0 & g.s=f1.g => g=pr(f0,f1)
- unconditioned: no
- productive: ()

Выделенные уравнения про стрелку примитивной рекурсии pr показывают ее суть - имея две операции и натуральное число, она строит их композицию, где одна из операций применяется однажды (она соответствует нулю), а другая - столько раз, какое у нас есть число (т.е. для числа 2 она будет применена дважды). Имея в категории натуральные числа, а также стандартный набор CCC - cartesian closed category - терминальный объект, произведения и экспоненциалы, можно определить сложение чисел, а через него и умножение.
let add=eval.prod(pr(curry(pi2), curry(s.eval)), I);
let mult=eval.prod(pr(curry(zero.!), curry(add.pair(eval, pi2))), I);
Тогда можно построить h(x) = x*(x+1):
let h = mult . pair(s, I);
И трижды применить ее к единице (которая s.zero, а не 1 - терминальный объект), чтобы получить 42.

Принцип вычислений примерно такой. Мы берем за основу терминальный объект и смотрим, какие есть морфизмы из него, назовем их элементами. Например, zero: 1 -> nat. В категории типов это функции из () - т.е. те, что могуть дать какое-то значение "из ничего". В логике это высказывания, истинность которых нам известна изначально, они как бы выводятся из True (терминального объекта), а не из каких-то других высказываний. Это те высказывания, из которых мы начинаем свой логический вывод (посылки?). И дальше мы из этих элементов строим конструкции путем композиции стрелок (вроде succ: nat -> nat), использования факторайзеров объектов для получения новых стрелок, их применения и т.д. Такое движение от терминального объекта задает разделение стрелок на два класса. Один - "по ходу движения" - это натуральные преобразования левых объектов и факторизаторы правых, они напоминают конструкторы данных в ЯП. Другой вид получается как бы "против движения" - это факторизаторы левых объектов и натуральные преобразования правых объектов, они напоминают управляющие структуры:

Получается такое разделение на данные и вычисления. В обычных языках программирования это разделение зафиксировано в явном виде, а тут оно возникает само из симметрии теории категорий. Можно придумывать объекты, к ним автоматически создавать двойственные, и разные их компоненты будут сами задавать способы строить данные и определять подходящие к ним управляющие конструкции, такой вот дуализм данных и кода (но совсем не тот, что в лиспе). Вычисления в CPL идут по уравнениям, связывающим морфизмы объектов (выводимым автоматически из свойств объектов), путем замены неканоничных частей выражения на каноничные, пока оно не будет целиком состоять из каноничных, т.е. всякий "код" должен выполниться и должны остаться одни "данные".

Comments

[thedeemon.livejournal.com]

А теория категорий - это такая абстракция над абстракциями, ею сейчас очень разные области математики связывают, т.к. она абстрагируется от внутренней структуры объектов и старается все выражать через их взаимоотношения. Так что есть шанс то бесконечное число абстракций свести в одну главную. :) Больше всего шансов у CCC - cartesian closed category, к ней сводится типизированное лямбда-исчисление, а к нему любые привычные нам вычисления и языки программирования. С другой стороны, меня давно привлекают всякие необычные способы делать вычисления, это имеет прямой практический выход - защита программ от взлома.

Хе, только сегодня тебя узнал - по ссылке на именной сайт в одном из постов. До этого было подумал, что появился новый знакомый из Швейцарии, ан нет, это старый. :)

[thedeemon.livejournal.com]

>HTM от Numenta?

Тут я не в теме совсем. Это детище дядьки, который написал книжку On Intelligence, которой у меня давно лежит русский перевод, но все никак не доходят руки прочитать. :) На первый взгляд HTM - это очередная нейросеть, а к нейросетям я скептически отношусь. Но тут я не хочу с выводами спешить.

[thedeemon.livejournal.com]

Поддерживаю.

Насколько я представляю, обычные нейросети обречены все время сваливаться в локальные минимумы, их решения обычно субоптимальны.

[thedeemon.livejournal.com]

Это весьма интересный вопрос - насколько наше мышление дискретно или непрерывно.

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

Если же смотреть с другой стороны - изнутри, интроспективно, то можно во-первых найти качественно разные явления: неконцептуальные ощущение цвета и ощущение звука отличаются качественно друг от друга и не кажутся дискретными, при этом есть собственно интеллект, оперирующий образами, концепциями, он качественно отличается от простых ощущений и содержание имеет вполне дискретное: каждый мысленный образ четко отделен от других. Когда наши с тобой предки еще даже не имели письменности, буддисты вовсю разрабатывали дисциплину, которая по-тибетски называется "цема" - "теория верного познания". Там говорится, что для того чтобы определить какой-то феномен, необходимо понять, что его отличает от других. Сплошная дискретность. :)

[thedeemon.livejournal.com]

Действительно, человек умеет задаваться такими вопросами, на которые сам потом затрудняется дать удовлетворительный ответ (и даже выбрать критерий удовлетворительности). В чем смысл жизни? Есть ли Бог? Чего хотят женщины? Крокодил более длинный чем зеленый или наоборот? :) Нередко сложность с нахождением ответа вызвана бессмысленностью вопроса, просто не всегда эта бессмысленность очевидна.

Но это не значит, что все вопросы такие, и что неспособность ответить - базовый алгоритм. И если мы сделаем нечто, что тоже не будет способно отвечать на вопросы, это не значит, что мы воспроизведем свое мышление.

Если серьезнее, то ты тут сейчас говоришь об алгоритмизуемости нашего мышления. Вот это правда непростой вопрос. И нейросети тут действительно кстати - часто в них не видно четкого и явного алгоритма, он там неявный, нечеткий.

[thedeemon.livejournal.com]

Посмотрел сегодня лекцию Хокинса про HTM в иллинойском универе. Идеи очень интересные, но оценить перспективность не берусь. Видно, что там получается очень много вычислений, а стоят ли они того, и нельзя ли тот же результат получить более простыми и прямыми способами...

[nivanych.livejournal.com]

> Больше всего шансов у CCC

В смысле, со стороны программирования?
CCC, это только простая интуиционистская логика.
Ещё есть моноидальные категории для работы с линейными логиками, моноидальный комонад, как интуиционистская модальность "необходимости", ...
Опять же, про зависимые типы, следует вспомнить всякоразные LCCC, и в частности, П-претопосы.

[thedeemon.livejournal.com]

Азы защиты от взлома:
1. непробиваемых защит нет
2. если взлом требует достаточно больших трудозатрат, то почти наверное он не состоится.

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

[thedeemon.livejournal.com]

Тут вы совсем в другую степь подались. Мне стоило чуть конкретнее выражаться, видимо.

Речь не о взломе серверов через эксплоиты, многие из которых действительно возможны благодаря ошибкам в обработке входных данных. Речь о защите устанавливаемого (десктопного или мобильного) софта от нелегального использования: некоторая функциональность должна быть доступна только по факту оплаты, который подтверждает введенный регистрационный код, например. Это то, что становится предметом взлома - обойти требование регистрации или найти способ генерировать регистрационные ключи без покупки. Смысл защиты в том, чтобы не дать так просто модифицировать программу и не дать возможность сделать кейген. В этом смылсе ваша "непробиваемая программа" уже пробита - ею можно пользоваться бесплатно.

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

[nivanych.livejournal.com]

Удивительно тут то, что такими примитивными типами можно описать уже весьма немало.
А ведь там даже зависимых типов нет, только чуть больше, чем (ко)алгебры.

[thedeemon.livejournal.com]

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

[nivanych.livejournal.com]

Бесконечных списков в виде индуктивных типов там не может быть.
А вот коиндуктивных запросто — это же просто другая запись вычисления следующего значения. А вычисление завершимое.

[nivanych.livejournal.com]

> чтобы описать pullbacks

Чтобы такое проверить в compile time, это должно быть уже нечто с элементами автоматического доказательства теорем.

[clayrat.livejournal.com]

А почему пуллбэк не описать?

[thedeemon.livejournal.com]

Сейчас взаимосвязи между стрелками выводятся из описания объектов, а их параметрами выступают только объекты. Для пуллбэка нужны параметры-стрелки и возможность явно задать связи между ними. Что-то такое:

right object pullback(f:A -> C, g:B -> C) with pbpair is
  pi1: pullback -> A
  pi2: pullback -> B
 where
  f . pi1 = g . pi2
end object

[thedeemon.livejournal.com]

И в подтверждение слов nivanych'a выше, цитата Хагино:
CDT we presented in this thesis was bounded by the restriction of computability. If we introduce equations, it becomes increasingly difficult to connect them to computing. If we had ‘pullback’ in CDT, we would have to prove f . k = g . h before using pbpair(k, h). Therefore, the programming would involve some proving.

(CDT - язык описания типов в CPL)

[maxim.livejournal.com]

Что тоже открыл для себя Хагино ?

[thedeemon.livejournal.com]

Не слышал о таком. :)

Странный вопрос, кроме Хагино кто-то еще про CPL писал подробно?

[maxim.livejournal.com]

Ты клево написал, спасибо тебе что пиаришь СPL.
Хагино не единственный который занимался диалгебрами, сигнатурами и факторизаторами для представления декартово-замкнутой категории.
Я когда то тоже изучал этот вопрос http://category-theory.livejournal.com/1436.html
Ниваныч обещал написать статью про диалгебры но так и не написал :)

[nivanych.livejournal.com]

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

[nivanych.livejournal.com]

Есть ещё Charity.
В чём-то, он даже более красивый и "консистентный" — там не диалгебры, а (ко)алгебры.
Про него описано достаточно подробно.

[thedeemon.livejournal.com]

Да, про Charity я в курсе, но пока не добрался еще до него.

[nivanych.livejournal.com]

Он немного попроще, реализация похуже.
И разработчики его вполне были в курсе Хагиновых придумок.

[thedeemon.livejournal.com]

В его троице два частных случая и один общий. И тема не раскрыта, только очевидный зачаток дан.

[udpn.livejournal.com]

Я вот пытаюсь понять, что я такого плохого сделал в жизнь, что моя карма испортилась настолько, что я попал в этот тред и даже прочёл его.

Как это вообще может работать? Это же теоркат, он даже не конструктивный.

[thedeemon.livejournal.com]

Ну это-то понятно - ввязался в дурную компанию. Мог бы как нормальный человек пить пиво и обсуждать футбол. :)

Работать это может как и лямбда-исчисление или там алгоритмы Маркова. Есть элементарные кирпичики - морфизмы, есть способы строить из них конструкции-редексы (композиция морфизмов и кое-что еще), и есть правила подстановки/редукции - такие-то конструкции заменять такими-то. Правила эти диктуются определениями объектов. Как-то так. Не могу сказать, что сам уже досконально разобрался.

[udpn.livejournal.com]

Тогда жду поста с объяснениями внутренностей или ссылок на статьи :) Редукция на морфизмах это что-то очень жестокое.

[thedeemon.livejournal.com]

Собсно, работа Hagino про Categorical Programming Language легко гуглится (но тяжело читается :) ), исходники интерпретатора есть на hackage, с замечательными комментариями на японском языке. :)

Редукцию морфизмов можно понимать синтаксически, просто правила ее диктуются теоркатом. Берем категорное определение натуральных чисел, там два морфизма: zero и succ. Причем zero очень хороший - он из терминального объекта идет. Из них мы можем композицией получить новые морфизмы: succ.zero, succ.succ.zero и т.д. Они тоже из терминального объекта исходят, получается, нас как раз такие интересуют, это наши "данные". Теперь определили произведение, там говорится, что ежели у нас есть объекты А и В и их произведение АхВ (из которого идут морфизмы pi1 и pi2 в А и В), то для любого объекта С, если из него есть тоже похожие морфизмы в А и В, назовем их f0 и f1, должен существовать морфизм из С в АхВ, назовем его pair(f0,f1). Описывается такое определение в CPL так, что тот знает, из существования чего должно вытекать существование чего, знает, какая диаграмма должна коммутировать. Из нее он выводит правила, например такое:
pi1.pair(f0,f1)=f0
Это всего лишь запись того, что на картинке про произведение композиция стрелок pair(f0,f1) и pi1 дает то же, что и стрелка f0. Смысл категорный, но уравнение получилось чисто синтаксическое, получилось правило для редукции.

Теперь возьмем построенные недавно морфизмы zero и succ.zero. Они исходят из одного и того же объекта (1 - терминального), а значит их можно поставить в формулу выше в качестве f0 и f1. Тогда если мы напишем выражение
pi1.pair(zero, succ.zero)
то интерпретатор может его редуцировать до просто zero. Профит!

[udpn.livejournal.com]

Не прошло и года, как я это понял.

Стоило всего лишь вынести немного теоркатов себе в диплом.

[thedeemon.livejournal.com]

Круто! Я когда универ заканчивал, и слыхом не слыхивал ни о теоркате, ни о теории типов...