Про типы

В Блоге Тру Программиста появилась подборка статей, посвящённых типам данных. Всем интересующимся рекомендуется к прочтению.

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

Итак, что же такое типы и зачем они нужны?

Типы данных пришли в программирование из математики. В математике же, как и многие другие понятия они появились по необходимости.

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

Представители логики и теории множеств предпочитали не иметь дело с переменными различных "типов". Однако, такая необходимость появилась весной 1901 года, когда, во время работы над фундаментальным трудом "Principia Mathematica" известный английский математик и философ Бертран Рассел сформулировал так называемый парадокс Рассела:

"Пусть S - это множество всех множеств, которые не содержат себя в качестве элемента. Содержит ли S само себя?"

Любой ответ, данный на этот вопрос практически мгновенно приводит к противоречию. Данный парадокс можно также переформулировать несколькими более "жизненными" способами:

• Деревенскому брадобрею приказали «брить всякого, кто сам не бреется, и не брить того, кто сам бреется», как он должен поступить с собой?
  
  
• В одной стране вышел указ: «Мэры всех городов должны жить не в своем городе, а в специальном Городе мэров», где должен жить мэр Города мэров?
  
  
• Некая библиотека решила составить библиографический каталог, в который входили бы все те и только те библиографические каталоги, которые не содержат ссылок на самих себя. Должен ли такой каталог включать ссылку на себя?

Решение этого парадокса, предложенное Расселом носит название "теории типов" и заключается в том, что каждой логической или алгебраической переменной приписывается "тип", который определяет, обозначает ли она [переменная] элемент, множество, множество множеств и так далее. Далее, Рассел постулировал, что любое утверждение вида" x является элементом из y" грамматически осмысленно лишьтогда, когда x - переменная типа элемент, а y - переменная типа множество или x - переменная типа множество, а y - переменная типа множество множеств и так далее. Любое утверждение, не удовлетворяющее этому правилу считается бессмысленным - вопрос о его истинности или ложности просто не существует, оно представляет собой просто набор букв.

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

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

Особенностями понятия типа являются:

1. Тип определяет класс значений, которые могут принимать переменная или выражение
2. Каждое значение принадлежит одному и только одному типу
3. Тип значения константы, переменной или выражения можно вывести либо из контекста, либо из вида самого операнда, не обращаясь к значениям, вычисляемым во время работы программы
4. Какой операции соответствует некоторый фиксированный тип операндов и некоторый фиксированный (обычно тот же самый) тип результата. (операции, обозначаемые одним и тем же символом, но производимые над различными типами операндом считаем разными)
   
5. Для каждого типа свойства значений и элементарных операций над значениями задаются при помощи аксиом.

Таким образом знание типа, позволяет обнаруживать в программе бессмысленные конструкции и предотвращает множество ошибок.

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

Использованные материалы:

1. Russel's Paradox
   
2. Парадокс Рассела - Википедия
3. Luca Cardelli. Type systems.
4. К. Хоор "О структурной организации данных" из книги У. Дал, Э. Дейкстра, К. Хоор "Структурное программирование", Москва, Мир, 1975