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

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