thedeemon | Арифметика типов как следствие

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

lcm(a, gcd(b,c)) == gcd(lcm(a,b), lcm(a,c))   (a,b,c - натуральные числа)
(a, Either b c) == Either (a,b) (a,c)         (a,b,c - типы данных в Хаскеле)
A & (B | C) == (A & B) | (А & C)              (A,B,C - логические высказывания)

и еще примерно 9213 теорем похожего вида.

Вот возьмем логику высказываний и логическую связку ИЛИ (|) оттуда, дизъюнкцию. Ее определением служат правила ввода и избавления. Правила ее ввода: если доказана достоверность высказывания А, то доказана и достоверность А|В. Если доказано В, то также доказано А|В. Правило избавления от дизъюнкции: если доказаны импликации А=>C и В=>С и доказано А|В, то отсюда выводится достоверность С.

Очень похоже выглядит сумма двух типов в ЯП (sum type aka discriminated union). В том же хаскеле это Either a b. Если есть значение х типа а, то можно построить значение Left х типа Either a b. Аналогично из значения х типа b можно построить значение Right x того же типа Either a b. Что можно с такими значениями делать, кроме как где-то хранить и куда-то передавать? Можно только одно - использовать в выражении case (и сводящемся к нему паттерн-матчинге). Конструкция case берет по сути две функции: одна что-то умеет делать со значением типа "а", другая - со значением типа "b", обе они возвращают результат одного типа "с", этот тип становится типом всего выражения case. Например,

h :: Either Int String -> Float
h x = case x of
  Left i -> fromIntegral i + 2.0
  Right s -> read s + 3.0

Сходство суммы типов и связки ИЛИ кристаллизуется в категорном определении суммы: объект sum(А,В) называется суммой объектов А и В, если из А и из В в него есть стрелки, и для любого другого объекта С, в который тоже есть стрелки из А и В, должна существовать уникальная стрелка из sum(A,B) в C да такая, чтобы получающаяся диаграмма коммутировала:

"Диаграмма коммутирует" означает, что если на ней между двумя точками (объектами) есть несколько различных путей, то неважно каким путем двигаться из первой точки во вторую, результат будет одинаковый. Применим ли мы сразу fromIntegral i + 2.0 к целому числу или сперва обернем в Left, а затем разберем через case и ту же функцию - результат один. Воспользуемся ли сразу импликацией А => С для вывода С из доказанного А или сперва выведем достоверность А|В, а затем с помощью той же импликации и правила избавления от | выведем С, результат не изменится. На языке CPL определение суммы записыватся так:

left object sum(a,b) with case is
  left  : a -> sum
  right : b -> sum
end object

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

f0: *b -> *a  f1: *c -> *a
-----------------------------
case(f0,f1): sum(*b,*c) -> *a
- equations:
(LEQ1): case(f0,f1).left=f0
(LEQ2): case(f0,f1).right=f1
(LFEQ): sum(f0,f1)=case(left.f0,right.f1)
(LCEQ): g.left=f0 & g.right=f1 => g=case(f0,f1)

(точка означает композицию стрелок)

Из одного этого определения можно получить важное следствие. Если у нас есть объект sum(A,B), то что можно сказать о sum(B,A)? Это какой-то другой объект, но в него тоже есть стрелки из А и В, а значит должна быть стрелка из sum(A,B) в sum(B,A), этого требует определение. Назовем ее f1. Аналогично, должна быть и стрелка из sum(B,A) в sum(A,B), назовем ее f2. Тогда их композиция f2 . f1 есть стрелка из sum(A,B) в sum(A,B). В категории у каждого объекта есть стрелка id в самого себя, а поскольку обсуждаемые стрелки тут таковы, что получаемые диаграммы с ними должны коммутировать, то не важно, попадем мы из sum(A,B) в себя по стрелке id или по стрелке f2 . f1, т.е. f2.f1 = id. Обратная композиция, f1.f2 аналогично идет из sum(B,A) в sum(B,A) и по тем же соображениям f1.f2 = id. Т.е. f1 и f2 - изоморфизмы, они делают объекты sum(A,B) и sum(A,B) изоморфными. Для теории категорий такие объекты - близнецы-братья, т.к. все связи одного объекта автоматически есть и у другого, ибо определение категории требует наличие стрелки-композиции для каждой пары последовательных стрелок. Мы только что показали коммутативность сложения: sum(A,B) == sum(В,А), где == означает изоморфность. В некоторых теориях изоморфность означает равенство, например, в категории, где объекты - натуральные числа, а стрелка означает делимость одного числа на другое, категорной суммой объектов служит gcd (наибольший общий делитель), и доказанное означает gcd(a,b) = gcd(b,a). А в категории, где объекты - типы данных, а стрелки - функции, изоморфность означает не равенство типов, а эквивалентность в том, какую информацию значения этих типов содержат. Изоморфность означает наличие стрелок-изоморфизмов, композиция которых равна id, а значит между такими типами должны существовать функции конверсии такие, что их композиция не теряет информации, сконвертив значение туда-обратно мы получим его же без изменений.

На CPL все доказательство будет выглядеть так:
let f1 = case(right, left);
Мы выше определили, что right и left - это стрелки типов *b -> sum(*a,*b) и *a -> sum(*a,*b) (звездочка перед именем означает, что это свободная переменная, произвольный объект, подобно 'a в окамле, где это произвольный тип). Тип case CPL вывел сам (приведен выше), отсюда он выводит тип f1: sum(*a,*b) -> sum(*b,*a). Соответственно, f1 . f1 будет иметь тип sum(*a,*b) -> sum(*a,*b), а значит f1.f1 = id (диаграмма должна коммутировать), и f1 - изоморфизм, доказывающий изоморфность этих двух объектов. "case(right, left)" - три слова на CPL, доказывающие коммутативность суммы сразу в куче теорий. Любое выражение на CPL определяет морфизм (стрелку), и при переводе на хаскель это выражение превращается в функцию:

f1 :: Either a b -> Either b a
f1 x = case x of
  Left a -> Right a
  Right b -> Left b

В некоторых категориях бывает определен инициальный объект. Он характеризуется тем, что из него есть по уникальной стрелке во все объекты категории. В логике высказываний таким объектом выступает особое высказывание ⊥ - ложь или абсурд. Его нельзя построить конструктивно (нет правила ввода), зато из него есть импликации во все возможные высказывания (из абсурда следует что угодно). В теории типов это пустой тип ⊥, у которого нет значений. На CPL инициальный объект (обозначим его 0) определяется так:

left object 0 with any
end object;

У него нет особенных стрелок кроме универсального морфизма any в каждый из объектов категории. CPL выводит:
any : 0 -> *a
Пользуясь этими определениями, можно составить на CPL выражение case(I,any). "I" в CPL обозначает тождественный морфизм, имеющийся у каждого объекта: I : *a -> *a. Выведенный тип для case(I,any) таков: sum(*a, 0) -> *a. Т.е. для любого объекта А есть стрелка из А+0 в А. А по определению суммы, из А есть стрелка left в А+0. И поскольку эти стрелки таковы, что соответствующие диаграммы обязаны коммутировать, наличие стрелок из А в А+0 и обратно опять нам дает изоморфизм, поэтому А+0 == А (я для простоты буду писать А+В вместо sum(A,B)). Значит, инициальный объект 0 - нейтральный элемент для сложения. В логике это превращается в знакомое правило P | False == P. В типах - Either a ⊥ == a (ведь значения типа слева всегда будут вида Left х, ибо в Right нам подставить нечего).

Сумму объектов в теоркате часто называют ~~гуаноэкстермина~~ копроизведением, потому что это dual к произведению: одно получается из другого разворотом всех стрелок. Соответственно, произведением объектов А и В называется такой объект prod(A,B), из которого есть стрелки в А и в В (назовем их fst и snd), и для любого похожего объекта С (из которого тоже есть стрелки в А и В) есть уникальная стрелка pair из С в prod(A,B):

Опять диаграмма должна коммутировать, т.е. fst.pair(f,g) = f и т.д. На CPL определение выглядит так:

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

Из него интерпретатор сам выводит

f0: *a -> *b  f1: *a -> *c
------------------------------
pair(f0,f1): *a -> prod(*b,*c)
- equations:
(REQ1): fst.pair(f0,f1)=f0
(REQ2): snd.pair(f0,f1)=f1
(RFEQ): prod(f0,f1)=pair(f0.fst,f1.snd)
(RCEQ): fst.g=f0 & snd.g=f1 => g=pair(f0,f1)

Ровно те же рассуждения что и с суммой позволяют показать коммутативность произведения. На CPL выражение pair(snd, fst) имеет тип prod(*a,*b) -> prod(*b,*a) и служит изоморфизмом между А*В и В*А, доказывающим их изоморфность. В логике произведением служит связка И, в категории типов - тупл, в категории натуральных чисел и делимости - lcm (наименьшее общее кратное).

Двойственным объектом к инициальному (0) является терминальный (1), характеризующийся наличием уникальных стрелок из всех объектов категории в него. На CPL его определение выглядит так:

right object 1 with !
end object;

В логике высказываний это особое высказывание "истина". В ЯП это тип unit, он же (), с единственным значением (). Его построить можно из чего угодно, функция "f x = ()" служит стрелкой из любого типа в (). Именно она названа на CPL !, где ее тип: *a -> 1. Как несложно догадаться, терминальный объект для произведения подобен инициальному для копроизведения - это нейтральный элемент, т.е. А*1 == А. Выражение "pair(I, !)" имеет тип *a -> prod(*a,1), а "fst" дает обратную стрелку из prod(*a,1) в *a. Композиции их дают стрелки из *a в *a и из prod(*a,1) в prod(*a,1), т.е. это изоморфизмы, и действительно А*1 == А. В категории с числами и делимостью 1 - это само число 1, на него делятся все натуральные числа. Получаем знакомые соотношения
(a, ()) == a
P & True == Р
lcm(a, 1) = a

Дальше нам понадобится экспоненциал. В логике это импликация (A => B), в ЯП это функциональный тип (a -> b), в категории натуральных чисел и делимости это хитро вычисляемое число. На CPL его определение:

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

C такими выводимыми интерпретатором следствиями:

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)

В категории с экспоненциалами можно доказать дистрибутивность умножения относительно сложения. Вот такое выражение на CPL:

let d1 = pair( case(fst,fst), case( left.snd, right.snd ) )

определяет стрелку типа sum(prod(*a,*b),prod(*a,*c)) -> prod(*a,sum(*b,*c)), т.е. из A*B+A*C в A*(B+C). А вот так можно определить обратную:

let flip = pair(snd, fst);
let cs = case(curry(left.flip), curry(right.flip));
let d2 = eval.pair(cs.snd, fst);

d2 имеет тип prod(*a,sum(*b,*c)) -> sum(prod(*a,*b),prod(*a,*c)), т.е. это стрелка из A*(B+C) в A*B+A*C. Вместе d1 и d2 служат изоморфизмами, доказывая A*(B+C) == A*B+A*C, дистрибутивность. Они выглядят понятнее, если их перевести на хаскель (не идиоматично, зато близко к коду на CPL):

d1 :: Either (a,b) (a,c) -> (a, Either b c)
d1 x = (a,b) where
  a = case x of { Left p -> fst p; Right p -> fst p }
  b = case x of { Left p -> (Left . snd) p; Right p -> (Right . snd) p }

d2 :: (a, Either b c) -> Either (a,b) (a,c)
d2 x = ((cs . snd) x) (fst x) where
  cs s = case s of
    Left b -> \a -> Left (a,b)
    Right c -> \a -> Right (a,c)

Конечно, d2 можно записать намного проще:

d2' :: (a, Either b c) -> Either (a,b) (a,c)
d2' (a, e) = case e of
              Left b -> Left (a, b)
              Right c -> Right (a, c)

Но загвоздка в том, что в категорном и CPL-ном определении case он параметризуется стрелками (функциями): одна стрелка здесь должна уметь из значения "b" сделать Left (a, b), а вторая из "с" сделать Right (a, c), но где им для этого взять "а"? По сути, эти функции в d2' - замыкания, они берут значение "а" из окружения. Приходится их реализовать более явно: не имея значения "а", мы возвращаем не Left (a, b), а функцию, которая из "a" сделает Left (a, b). Аналогично с Right (a, c). Тип у этих двух возвращаемых функций одинаковый, и он становится типом всего выражения case. И возвращенная им функция уже применяется к параметру типа "а", взятому из исходной пары. Именно поэтому нам потребовались экспоненциалы.
CPL-ные определения стрелок d1 и d2 можно превратить в диаграммы со стрелочками (они там, особенно для d2, довольно развесистые получаются, могу потом картинку показать) и сформулировать категорное доказательство дистрибутивности. Оно намного длиннее, чем те пара строчек на CPL. Итак, дистрибутивность показали, получили упомянутые в начале поста следствия для конкретных теорий.

Раз уж у нас появился экспоненциал, докажем кое-какие его свойства. Напомню, что exp(A,B) означает для ЯП тип функции А -> В, для логики импликацию А => В, но экспоненциалом называется в силу схожести с В^A - "В в степени А". От возведения в степень разумно ожидать, что А^1 = A и 1^A=1 для любого А, т.е. exp(1,A) == А и exp(A,1) == 1. Построим такие выражения-стрелки на CPL:

let e1 = eval.pair(I,!);
let e2 = curry(I);
let e3 = curry(!);

e1 имеет тип exp(1,*a) -> *a, т.е. дает нам стрелку из А^1 в A. e2 имеет тип *a -> exp(*b, prod(*a,*b)), для любых объектов А и В е2 дает стрелку из А в exp(B, A*B), в частности для В=1 это стрелка из А в (A*1)^1, а про А*1 мы уже знаем, что он изоморфен А. Это вроде как доказывает(?) A^1==A.
Выражение е3 имеет тип *a -> exp(*b,1) и для произвольных объектов A и B дает стрелку из A в 1^B, в частности из 1 в 1^B. Ну а стрелка из 1^B в 1 всегда есть по определению 1 - терминального объекта. И опять в силу характера этих стрелок, наличие двух стрелок туда-обратно между объектами делает стрелки изоморфизмами, а объекты изоморфными. Значит, 1^A == 1 для любого А. Как следствие a -> () == () для типов и (P => True) == P для логических высказываний.

Итого, из категорных определений произведения, копроизведения, экспоненциала, инициального и терминального объектов мы вывели как следствия такие арифметические свойства:
a+b == b+a
a*b == b*a
a+0 == 0+a == a
a*1 == 1*a == a
a*(b+c) == a*b + a*c
a^1 == a
1^a == 1
И из этого набора можно получить другие следствия. Например, обозначив 1+1 за 2, получим
a*2 == a*1 + a*1 == a + a
т.е. умножение (на натуральное число) выражается через сложение не только в привычной арифметике натуральных чисел, но и в арифметике типов, например.

Кроме того можно показать, что a^2 == a*a, т.е. возведение в натуральную степень выражается через произведение. Необходимые изоморфизмы на хаскеле выглядят так:

type Two = Either () ()

p1 :: (a,a) -> (Two -> a)
p1 (a,b) = \i -> case i of { Left _ -> a; Right _ -> b }

p2 :: (Two -> a) -> (a,a)
p2 f = (f (Left ()), f (Right ()))

Их можно записать на CPL и получить категорные диаграммы, но мне сейчас лень, чуть позже сделаю. Вот такая вот арифметика. Да простят меня за капитанство, но желание поделиться и показать возможности CPL перевесило.

Flat | Top-Level Comments Only

From:

gds.livejournal.com

> в которой я рассказываю сам себе постигнутые азы

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

А лингвистически, про копроизведение -- я давно догадывался! :]

From:

109.livejournal.com

копро-изведение?

From:

gds.livejournal.com

ваистену!

From:

maxim.livejournal.com

Да будет раскрыт педагогический потенциал CPL!

From:

109.livejournal.com

что-то я торможу. в сишарпе, тип (), он же void - это терминальный или инициальный объект?

From:

gds.livejournal.com

если брать "морфизм = функция, объект = значение", то терминальный, его из любого объекта можно получить, применив "fun _ -> ()".

From:

109.livejournal.com

okay, a что в сишарпе инициальный объект?

From:

gds.livejournal.com

а вот не знаю про C#. Обычно, если определять категорию как в моём каменте выше, это какой-то ненаселённый тип. Например, в окамле так:

# type uninh = [ ];
type uninh = [  ]
# value f (x : uninh) = match x with [ ];
value f : uninh -> 'a = <fun>
#

То есть, из значения ненаселённого типа можно единственным образом (применением ровно одной функции) получить любое значение любого типа. По крайней мере, теоретически никто не мешает. Да вот только не создать значение, имеющее ненаселённый тип, поэтому и в функцию передать особо нечего, поэтому и функция выполняться не будет, поэтому и не вернёт ничего.
Если в C# есть исключения, то можно рассмотреть тип функции, единственной работой которой будет бросить исключение, как инициальный объект, но я не знаю C# вообще, поэтому не могу гарантировать здравость этой идеи.

From:

sassa-nf.livejournal.com

если вы отображаете что-то в одно значение одного типа, то это не инициальный объект; это как раз терминальный объект.

From:

Арифметика типов как следствие

Page Summary

Style Credit

Expand Cut Tags