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

[thedeemon]

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

Comments

[gds]

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

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

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

[109]

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

[gds]

ваистену!

[maxim]

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

[109]

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

[gds]

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

[109]

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

[gds]

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

# type uninh = [ ];
type uninh = [ ]
# value f (x : uninh) = match x with [ ];
value f : uninh -> 'a =
#
То есть, из значения ненаселённого типа можно единственным образом (применением ровно одной функции) получить любое значение любого типа. По крайней мере, теоретически никто не мешает. Да вот только не создать значение, имеющее ненаселённый тип, поэтому и в функцию передать особо нечего, поэтому и функция выполняться не будет, поэтому и не вернёт ничего.
Если в C# есть исключения, то можно рассмотреть тип функции, единственной работой которой будет бросить исключение, как инициальный объект, но я не знаю C# вообще, поэтому не могу гарантировать здравость этой идеи.

[voidex]

Согласен с предыдущими ораторами. Огромное спасибо за статью.

[udpn]

Лучше бы ты образовал себе месяцок свободного времени да написал учебник по теоркату c примерами на CPL. Он был бы куда популярнее всяких "категорий для программистов".

[thedeemon]

Мне бы сперва самому чему-то научиться, на это не один месяцок уйдет. А CPL все же недостаточно выразительный, как упоминалось ранее, на нем даже pullback не описать.

[udpn]

Тогда вопрос по теме.

Если из наличия экспоненциалов следует наличие дистрибутивности сложения относительно умножения, то из чего следует дистрибутивность умножения относительно сложения?

[thedeemon]

В посте говорится про "дистрибутивность умножения относительно сложения" как раз. А обратное бывает где-то?