воскресенье, августа 19, 2007

Про типы

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

Все описанное в статьях (как тех на которые я ссылался, так и первоисточниках имени 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

2 комментария:

Ivan N. Veselov комментирует...

Спасибо, хорошая вводная статья.

Tanya Bond комментирует...

Был такой язык Паскаль... где области значений уделялось большое внимание. Тогда считалось, что это будет способствовать написанию более устойчивого кода. Но, как я предполагаю, проблемы с производительностью (проверки при каждом изменении значения) привели к отказу от жесткого контроля на уровне определения переменной.
Этот вопрос необходимо знать и постоянно держать в голове. При блочном программирвании нелишне добавлять проверки.
И, конечно, тип переменной определяет объем обрабатываемых/хранимых данных (массивов), производительность программы, соотвествие ресурсным ограничениям.