Monday, August 13, 2007

Типы: микро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. Это он не потому что считает, что динамические языки это не тру, а потому что путаница получается серьезная.

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

6 comments:

mibori said...

Будем ждать продолжения.

Я, например, слабо себе представляю различие слабой от строгой типизации. А различие динамической типизации от статической, в моём понимании, состоит в том, что один и тот же идентификатор может принимать значение различных типов на всех этапах выполнения/вычисления алгоритма (почему "идентификатор"? потому, что, например, в функционально чистом языке нет понятия переменной).

lrrr said...

Ну "слабая" и "строгая" это buzzwords, никакого хорошего авторитетного определения тут и нету, как выяснилось. Я очень искал :)

Насчет различия динамической и статической - да, очень популярная мысль. Часто ее еще формулируют как "при статической типы привязаны к переменным, а при динамической - к значениям".

Но, имхо, это как определение динамической типизации не очень катит, т.к. тут речь больше о том, "как", а не "зачем".

Lev Kurts said...

Читая подборку мне показалось, что было бы полезно начать её с "простого" введения в типы. Попытался такое введение дать и опубликовал у себя в блоге. Мне кажется это введение сошло бы за 0-вую часть Вашей подборки: Про типы.

lrrr said...

Да, очень интересно :) Просто я сознательно старался тут поменьше математики тащить.

Yuri said...

Ну "слабая" и "строгая" это buzzwords, никакого хорошего авторитетного определения тут и нету, как выяснилось. Я очень искал :)

Ну какие ж это buzzwords??
Каким словом вы собираетесь описывать то, что язык позволяет (или не позволяет) операции над объектами разных типов? То, что нет авторитетного определения, не значит, что нету понятия.

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

lrrr said...

Yuri> Да в общем-то согласен, не совсем баззвордс. Но и не очень удачный термин, часто эти слова используются, как будто они обозначают некоторое самостоятельное свойство языка.

Более понятнее, имхо, описывать это как "более развитая система типов" или вроде того.