О теории типов для чайников

Когда собираешься почитать что-то про зависимые типы, желание обычно быстро угасает после примерно таких разъяснений:

«Зависимые типы должны описываться слоями морфизма; чтобы придать этому смысл в категориях, мы перестаём говорить о слоях морфизма, а начинаем просто говорить о том, что зависимый тип (x: X) -> Y(x) задаётся морфизмом X -> Y; таким образом, мы переходим к категории срезов над объектом Y. Слои морфизма как истинные объекты вообще не встречаются, и в этом смысле зависимые типы действительно живут в своей особенной категории — категории срезов над объектами исходной категории».

Cимметричные моноидальные категории, косвободные кокоммутативные комоноиды, экспоненциирование в слайс категориях…

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

Правда, теория типов была разработана ещё до появления языков программирования, о чём было подробно рассказано вот в этом сериале.

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

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

Рассел ввёл понятие иерархии типов, по сути концепцию аннотаций типов для функций программирования.
Простой пример на C#. Допустим, мы хотим функцию, способную исполнять любую функцию, получающую целый аргумент и вычисляющую целый результат.

int runFunction(Func<int,int> func) {return func(1);}

Вот такие функции мы хотим исполнять:

int addTwo(int param) {return 2 + param;}
int multiplyByTwo(int param) {return 2 * param;}

Наши программы могут быть такими:

int program1() { return runFunction(addTwo); }
int program2() { return runFunction(multiplyByTwo); }

Они корректно работают и вычисляют что надо.

Однако вот такой код уже не будет работать:

int program3() { return runFunction(runFunction); }

Компилятор сообщит, что преобразование типа из «группа методов» в нашу функцию Func<int,int> невозможно. Так происходит потому, что runFunction принимает на вход лишь функции первого порядка, а сама runFunction — функция второго порядка (получающая функцию первого порядка как аргумент).

Теория типов сама по себе недостаточна для описания новых оснований математики, когда все математические истины в принципе могли бы быть доказаны с использованием символической логики. Эта цель в полном объеме недостижима.

Системы типов к сожалению не могут предотвратить все ошибки, однако при грамотном использовании позволяют исключить огромное их количество — на пару порядков больше, нежели это происходит в мэйнстримовской разработке (без продумывания системы типов, без Type Driven Development)! И без сомнения, нынешние системы типов в популярных языках программирования можно очень сильно улучшить и усовершенствовать — исследования в этой сфере пока ещё очень далеки от завершения!

Поделиться статьей ...Share on Facebook0Share on Google+0Tweet about this on TwitterShare on LinkedIn0Share on VKPrint this page

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *