В Блоге Тру Программиста появилась подборка статей, посвящённых типам данных. Всем интересующимся рекомендуется к прочтению.
Все описанное в статьях (как тех на которые я ссылался, так и первоисточниках имени Chris Smith и Luca Cardelli), написано на довольно высоком уровне. Мне же кажется, что очень важным моментом здесь является "качественное" понимание, объяснение, так сказать "на пальцах". Потому что без подобного понимания знание фактов и определений скорее является следованием "культу карго", чем настоящим знанием.
Итак, что же такое типы и зачем они нужны?
Типы данных пришли в программирование из математики. В математике же, как и многие другие понятия они появились по необходимости.
Как известно математики часто проводят в своих рассуждениях чёткое различие между элементами, множествами элементов, функциями и так далее. Для новой переменной, используемой в первый раз, математик определяет "тип", например: "Пусть f - это функция действительного переменного". Часто в книгах (обычно во введении и предисловии) также даются подобные определения: "В дальнейшем для множеств будут использоваться прописные буквы". Эти определения являются не более чем "помощниками" для читателя, позволяют ему быстрее ориентироваться в дальнейшем тексте.
Представители логики и теории множеств предпочитали не иметь дело с переменными различных "типов". Однако, такая необходимость появилась весной 1901 года, когда, во время работы над фундаментальным трудом "Principia Mathematica" известный английский математик и философ Бертран Рассел сформулировал так называемый парадокс Рассела:
"Пусть S - это множество всех множеств, которые не содержат себя в качестве элемента. Содержит ли S само себя?"
Любой ответ, данный на этот вопрос практически мгновенно приводит к противоречию. Данный парадокс можно также переформулировать несколькими более "жизненными" способами:
- Деревенскому брадобрею приказали «брить всякого, кто сам не бреется, и не брить того, кто сам бреется», как он должен поступить с собой?
- В одной стране вышел указ: «Мэры всех городов должны жить не в своем городе, а в специальном Городе мэров», где должен жить мэр Города мэров?
- Некая библиотека решила составить библиографический каталог, в который входили бы все те и только те библиографические каталоги, которые не содержат ссылок на самих себя. Должен ли такой каталог включать ссылку на себя?
Решение этого парадокса, предложенное Расселом носит название "теории типов" и заключается в том, что каждой логической или алгебраической переменной приписывается "тип", который определяет, обозначает ли она [переменная] элемент, множество, множество множеств и так далее. Далее, Рассел постулировал, что любое утверждение вида" x является элементом из y" грамматически осмысленно лишьтогда, когда x - переменная типа элемент, а y - переменная типа множество или x - переменная типа множество, а y - переменная типа множество множеств и так далее. Любое утверждение, не удовлетворяющее этому правилу считается бессмысленным - вопрос о его истинности или ложности просто не существует, оно представляет собой просто набор букв.
Таким образом понятие типа делает невозможным использование в логических и математических выражениях некоторых ошибочных выражений. То есть проверку требований, накладываемых типом, можно делать на уровне формального просмотра текста, не обращаясь к значению, приписываемому символу в каждом конкретном случае.
Именно это понятие типа и используется в программировании и оно действительно используется в основном для того, чтобы "предотвратить ошибки при выполнении программ".
Особенностями понятия типа являются:
- Тип определяет класс значений, которые могут принимать переменная или выражение
- Каждое значение принадлежит одному и только одному типу
- Тип значения константы, переменной или выражения можно вывести либо из контекста, либо из вида самого операнда, не обращаясь к значениям, вычисляемым во время работы программы
- Какой операции соответствует некоторый фиксированный тип операндов и некоторый фиксированный (обычно тот же самый) тип результата. (операции, обозначаемые одним и тем же символом, но производимые над различными типами операндом считаем разными)
- Для каждого типа свойства значений и элементарных операций над значениями задаются при помощи аксиом.
Таким образом знание типа, позволяет обнаруживать в программе бессмысленные конструкции и предотвращает множество ошибок.
Конечно, данный текст представляет собой лишь краткое введение в системы типов, и не охватывает всего многообразия и сложности темы, но мне кажется что подобное введение необходимо для понимания более сложных концепций.
Использованные материалы:
- Russel's Paradox
- Парадокс Рассела - Википедия
- Luca Cardelli. Type systems.
- К. Хоор "О структурной организации данных" из книги У. Дал, Э. Дейкстра, К. Хоор "Структурное программирование", Москва, Мир, 1975
blog: 
LinkedIn
Мой Круг
