Типы: микроFAQ/ликбез

В основном это вольный перевод избранных мест из "What To Know Before Debating About Type Systems" и статьи L. Cardelli "Type Systems".

Итак,

Определение

Одного простого и общепринятого определения понятия "тип" или "система типов", как ни странно, нету. Основное назначение системы типов это обнаружение ошибок, которые могут возникнуть при выполнении программы. Весьма известный деятель в области computer science, лауреат премии Тьюринга Лука Карделли приводит такое несложное определение:

Тип переменной -- это множество значений которые может принимать переменная во время выполнения программы.

Определение так себе, конечно. Простое и очень обтекаемое. Не понятно какую роль типы играют для языка, как система типов  работает вообще и зачем она нужна.

Если хотите чего-нибудь более философского, то можно обратиться к книжке Б. Пирса "Types and Programming Languages", где он дает более хитрое определение для системы типов:

Система типов — это способ доказать за конечное время, основываясь на синтаксисе и классификации фраз программы по видам вычисляемых ими значений, что программа не ведет себя определенным образом.

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

К тому же, можно придраться и к требованию чтобы проверка типов заканчивалась за конечное время, например в языках Qi и Cayenne это не обязательно так.

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

Строгая типизация

Пара слов о "слабой" и "строгой" типизации — дело в том, что им никто еще сколько-нибудь приличного определения не дал. Выражение "в языке X нет строгой типизации" обычно означает завуалированное "ваш язык X — ацтой", и серьезные дядьки таких слов не используют.

Статическая vs Динамическая система типов

Отсутствие статической проверки типов означает, что операции в языке могут быть применены без проверок к абсолютно любым значениям, в том числе и "неправильным" ("неправильность" может определяться по разному в разных системах). Тут-то и кроется главный нюанс.

Если такие операции приводят к каким-то непредсказуемым в общем случае последствиям, можно смело говорить что типов нету вообще. Товарищ Карделли вот называет это untyped unsafe languages, и приводит в пример ассемблер.

Если последствия таких действий предсказуемы, например, вылетает исключение или в результате получается какое-то специальное значение, то это называется системой динамических типов. Реально между статической и динамической типизацией общего не так уж и много, и в основном все заблуждения здесь как раз происходят от желания найти какой-то общий знаменатель для них. Это бесполезно, слово "тип" в них означает совершенно разные вещи.

Карделли вот вообще осознанно не использует термин "динамическая типизация" — вместо этого у него "динамические проверка [значений]", а подобные языки называет untyped safe languages. Это он не потому что считает, что динамические языки это не тру, а потому что путаница получается серьезная.

 Продолжение следует