Что необходимо знать, прежде чем спорить о системах типов

Перевод статьи Криса Смита What To Know Before Debating Type Systems

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

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

Классификация систем типов

Системы типов, как правило, характеризуются устоявшимися терминами. Наиболее употребительными являются «статическая», «динамическая», «сильная» и «слабая». Данный раздел описывает распространенные используемые типы классификации. Возможно, что-то здесь окажется для вас полезным, а что-то нет.

Сильная и слабая типизация

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

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

• Сильная типизация: система типов, которая мне нравится, и я чувствую себя комфортно, используя ее.
  

• Слабая типизация: система типов, которая доставляет мне беспокойство, и, используя ее, я чувствую себя несколько неуверенно.
  

А как быть, когда выражения используются в более ограниченном смысле? Сильная типизация, в зависимости от автора и контекста разговора может означать «статическая» или “чистая” обе описаны ниже.

Статическая и динамическая типизация

Это практически единственная классификация систем типов, имеющая реальное значение. На самом деле значимость такой классификации часто недооценивается. Я понимаю, что может показаться смешным; но к этой классификации мы будем еще не однажды возвращаться в этой статье. Динамическая и статическая система типов – это два абсолютно разных понятия, цели которых лишь иногда частично перекрываются.

Статическая система типов - это механизм, с помощью которого компилятор анализирует исходный код и присваивает синтаксическим единицам метки (так называемые "типы"), а затем используют их для того, чтобы что-то сделать вывод о поведении программы. Динамическая система типов представляет собой механизм, на основании которого компилятор генерирует код для отслеживания вида данных (иначе «типа») используемого в программе. Использование одного и то же термина "тип" в каждой из этих двух систем, конечно, не совсем совпадающее, но, несмотря на это, так будет лучше понять его исторический или обобщенный смысл. Огромную путаницу вызывают попытки определить «тип», как понятие, означающее одно и то же для обеих систем. Его нет. Наилучшим способом решения данной проблемы является осознание некоторых фактов:

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

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

• Динамическая типизация не ограничена проблемами, которые можно решить, используя статическую типизацию.
  

• По своей сути эти две системы - не одно и то же в принципе
  

Исследование второго из этих четырех простых фактов популярное занятие в некоторых кругах. Совсем недавно я прочитал этот набор заметок и натолкнулся на запутанный комментарий «система типов определила зацикливание». Забавно, что с теоретической точки зрения, решение задач зацикливания – это одно их простейших возможных вещей, которые вы можете сделать со статической типизацией! Легко-типизированное (simply-typed) лямбда-исчисление, на котором в принципе основаны все остальные системы типов, доказывает, что программа завершаема за конечный промежуток времени. Действительно, более интересным является вопрос, как можно расширить систему типов, способную описать незавершаемую программу! Несмотря на это, нахождения зацикливаний не является классом задач, которые, по мнению большинства людей, относятся к системам типов. Данный вопрос недоказуем в динамической типизации (это называется проблемой останова (halting problem), вы, вероятно, слышали об этом). Но нет ничего специального для статической типизации. Почему? Потому что она совершенно непохожая на динамическую типизацию.

Разделение типизации на статическую и динамическую порой водит в заблуждение. Большинство языков, даже если они являются динамически типизированными, имеют в своем распоряжении некоторые особенности статической типизации. И, как мне известно, все языки имеют некоторые особенности динамической типизации. Однако любой язык можно отнести к той или иной системе типов. Почему? Это вытекает из первого из четырех фактов, которые приведены выше: большинство проблем решается совмещением особенностей каждой из систем, таким образом, проектирование любой из систем, что бы она была только статической или только динамической обеспечит маленькую пользу и громадную стоимость.

Другие Виды

Существует множество других способов классифицировать системы типов. Они не являются такими фундаментальными, однако ниже представлены наиболее интересные:

• Чистая типизация. Чистая система типов, это такая, которая обеспечивает определенные виды гарантий. Это четко определенная концепция, относящаяся к статической типизации, которая имеет доказательства и все необходимые навороты. Многие современные системы являются чистыми. Но более старые языки, такие как C часто не являются чистыми системами; системы типов таких языков спроектированы только для предоставления некоторых предостережений в общем случае. Данное понятие можно применить и к динамическим системам, но точное определение там может быть изменчивым в зависимости от их употребления.
  

• Явная/неявная типизация. Когда используются эти определения, они определяют меру, согласно которой компилятор выводит статические типы частей программы. Все языки программирования имеют определенный уровень выводимости типов. У некоторых он больше, чем у других. ML и Haskell используют неявную типизацию из-за чего объявление типов не требуется (или почти не требуется, в зависимости от языка и используемых расширений). Java и Ada используют явную типизацию и требуют объявление типа операндов. Все из вышеперечисленных языков (к примеру, по сравнению с C и C++) имеют сильную статическую типизацию.
  

• Лямбда-исчисление. Разнообразные вариации между статическими системами типов обобщены в абстракцию, называемую «лямбда-исчислением». Ее определение выходит за пределы данной статьи, но по существу, она определяет - поддерживает ли система типов некоторые особенности: параметризированные типы, зависимые типы, или операторы типов. Обратитесь сюда за дополнительной информацией.
  

• Структурная/Номинальная типизация. Этот вид типизации в основном используется применительно статической типизации с подтипами. В структурной типизации допущение о типе осуществляется всякий раз, когда это действительно возможно. К примеру, запись с полями X, Y, и Z может автоматически приводиться к одному из подтипов полей X и Y. В номинальной типизации нет таких допущений, пока оно не будет где-нибудь объявлено.
  

• Утиная типизация. Этот термин стал популярным недавно. Он базируется на динамическом аналоге структурной типизации и означает, что прежде чем делать допущение о том, является ли корректным тип некоторого объекта, используемого в процессе, система выполнения просто проверяет, поддерживает ли этот объект все операции допустимые для него. Данные операции могут иметь различную реализацию, для разных типов.
  

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

Заблуждения о статической и динамической типизации

Многие программисты подходят к вопросу предпочтения статической или динамической типизации путем сравнения некоторых языков, использующих обе техники, с которыми они знакомы. Это разумный подход для большинства вопросов предпочтения. И здесь основная проблема заключается в том, что большинство программистов имеют определенные пристрастия к некоторым языкам и даже не попробуют воспользоваться другими языками. Даже шесть или семь языков, известные им это не так уж и много. К тому же, для действительного эффективного использования этих двух, очень различных между собой стилей программирования, необходимо большее, чем их поверхностное представление. Вот два интересных следствия подобной ситуации:

• Многие программисты используют языки, имеющие очень слабую статическую типизацию.
  

• Многие программисты используют динамически типизированные языки очень ограниченно.
  

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

Заблуждение: Статическая типизация подразумевает объявление типа

Наиболее очевидным фактом относительно систем типов Java, C, C++, Pascal, и многих других распространенных «промышленных» языков является не то, что они статически типизированные, а то, что они явно типизированные. Другими словами, они требуют объявления типов. (В мире менее явно типизированных языков, где такие объявления опциональны, они часто иначе называются языками с аннотацией типов. Вы также можете найти использование мной этого термина.) Это опять заставляет некоторых людей нервничать, и программисты по этой причине часто отказываются от использования статически типизированных языков.

Это не имеет ничего общего со статической типизацией. Первые статически типизированные языки были явно типизированными по необходимости. Однако алгоритмы вывода типов – техника определения типов переменных, по их использованию в исходном коде – существовали давно. Язык ML, который использует их сегодня, является одним из числа старейших. Haskell, замечательно использующий данный подход, недавно отметил свое пятнадцатилетие. Даже C# принимает подобную идею, что вызовет много удивления (и несомненно вызовет массу недовольств относительно его «слаботипизированности» - см. определение выше). Если кому-то не нравится определение типов, то они более состоятельны в описании, отличном от явной типизации.

Я не хотел сказать, что объявление типов – это всегда плохо. Но в моей практике были ситуации, в которых это было обязательными. Вывод типов, как правило, обладает большим преимуществом.

Заблуждение: Динамически типизированные языки являются слабо типизированными.

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

Поступая таким образом, программист отказывается от эффективного использования динамической типизации. Это подобно тому, как купить себе новый автомобиль, и не желать ехать быстрее велосипеда. Использование автомобиля ограничено: вы не можете на нем взобраться по горной тропе, и помимо всего он требует бензина для своего использования. Действительно, такие ограничения автомобиля идут только на пользу целесообразности использования велосипеда! Подобным образом динамически типизированные языки могут оправдывать использование языком со статически типизированной системой.

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

В порядке комментария и конечно для продолжения дискуссии: нет возможности сделать исчерпывающее блочное тестирование на Haskell, как бы его можно было сделать на Ruby или Smalltalk. Это попросту пустая трата времени. Интересно отметить, что разработка через тестирование (Test-Driven Delevopment) исходит от людей, предпочитающих динамически типизированные языки.

Заблуждение: Статическая типизация подразумевает использование подхода «дизайн наперёд» (BDUF) или водопадную методику.

Некоторые статически типизированные языки спроектированы с учетом идеи так называемого хорошего процесса разработки. То есть они часто требуют или всячески способствуют необходимости детального описания интерфейса в одном месте, и только после этого можно писать исходный код. Это становится затруднительным, в случае, когда требуется разрабатывать изменяемый код или когда необходимо исследовать некоторую идею. Это иного означает, что для изменения функциональности требуется делать изменения в различных местах. Наихудшая форма подобного явления и того что мне известно (хотя отчасти это сделано скорее не про идеологическим, а прагматическим соображениям) это заголовочные файлы C и С++. У Pascal есть подобная проблема, требующая объявления всех переменных в отдельной группе в заголовке файла. Хотя и некоторые другие языки также навязывают подобное разделение, многие избавлены от такой необходимости.

Абсолютно справедливо, что подобные языковые ограничения могут мешать существующим практикам разработки программного обеспечения, завоевавшим признание, включая гибкие методологии. Так же справедливо, что данные ограничения не имеют ничего общего со статической типизацией. В серьезных источниках о статической типизации вы не найдете ни слова о необходимости разделять интерфейсы от реализации, объявлять все переменные заранее, или выполнять какие-то другие ограничения. Подобные ограничения иногда являются пережитком тех времен, когда считалось допустимым их подобное использование в угоду применяемых компиляторов. Иногда подобное решение основано на идеологических предпочтениях авторитетных людей. Но это не связано со статической типизацией.

Если кто-то не желает, что бы используемый язык определял процесс написания кода, то это абсолютно понятно. Но, к несчастью, данный факт, как правило, вводит в заблуждение относительно системы статических типов.

Подобное заблуждение находит отражение в различных выражениях: «Мне нравится заниматься исследованием в программировании» - это популярная фраза. То есть, взяв во внимание существующие мнения, будто статически типизированные языки обязывают сначала написать весь код, и поэтому они не так хороши для проведения своего рода экспериментов и изучения их результатов. Основные инструменты для исследования программирования имеют в своем распоряжении интерактивную среду REPL (read-eval-print loop), которые в основном являются интерпретаторами и принимают строку выражения, обрабатывают ее, и выводят результат операции. Подобные инструменты достаточно полезны, и они существуют для многих языков, как статических, так и динамических. Их нет для Java, C, или C++, и в связи с этим появился неприятный миф, что они могут быть только у динамических языков. Динамически типизированные языки, возможно, обладают некоторыми преимуществами в этой области (бесспорно, ряд преимуществ у них разумеется, есть), но это в первую очередь определяется наличием подобных инструментов для конкретного языка а не спецификой системы типов.

Заблуждение: У динамически типизированных языков нет возможности отловить ошибки.

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

Можно обсуждать причины таких заблуждений, и при этом иметь в данном вопросе веские аргументы. К примеру, одна причина заключается в том, что средний уровень программистов, знакомых с Ruby выше программистов, которые знакомы с Java. Еще причиной может быть то, что C++ и Java имеют относительно бедную систему типов. Еще одна причина – это тестирование. Как упоминалось выше, блочное тестирование пришло с динамических языков. Оно имеет некоторые недостатки, по сравнению с гарантиями, предоставляемыми статическими типами, но также имеет и ряд преимуществ; системы статических типов не могут обеспечить проверку многих свойств исходного кода, которые доступные в блочном тестировании. Игнорируя этот факт, общаясь с кем-нибудь, кто действительно знаком с Ruby, вы также можете оказаться проигнорированными.

Заблуждение: Статическая типизация предполагает больший объем кода.

Это заблуждение тесно связано с одним из вышеперечисленных об объявлениях типов. Объявление типов – это одна из причин, по мнению множества людей, влияющая на увеличение объема кода при статической типизации. Но есть и другая сторона данного аспекта. Статическая типизация часто позволяет писать более компактный код.

Это заявление может выглядеть удивительным, но так оно и есть. Типы несут информацию, и эта информация может использоваться в дальнейшем, предотвращая необходимость дублирования кода. Это нельзя показать на простых примерах, но действительно изумительное решение существует в стандартной библиотеке Haskell в модуле Data.Map. Этот модуль реализует сбалансированное бинарное дерево поиска и содержит функцию, подобную этой:

lookup :: (Monad m, Ord k) => k -> Map k a -> m a

Это магическая функция. Она позволяет находить нечто в Map и получать результат. Достаточно просто, но здесь есть ньюанс, что делать, когда результата нет? Как правило, результатом выполнения функции в таком случае может быть специальное значение “nothing” (пусто), или прерывание текущего вычисления и инициирование обработчика ошибок, или же завершение выполнения всей программы. Функция, описанная выше делает все из перечисленного! Ниже представлен код, описывающий сравнение результата со специальным значением “nothing”:

case (lookup bobBarker employees) of
Nothing -> hire bobBarker
Just salary -> pay bobBarker salary

Как Haskell определяет, что вариант возвращения Nothing для дальнейших действий для меня более предпочтителен генерации прочих видов ошибки, когда запрашиваемое значение отсутствует? Это происходит по причине того, что я указал сравнение результата со значением Nothing! Если бы я не написал такого непосредственного кода по обработке подобной ситуации, но описал бы вместо этого где-то обработку всех трех вариантов обработки ошибок на предмет отсутствия необходимого значения, мне пришлось бы последовательно реализовывать семь или восемь дополнительных проверок и использовать в вычислениях результат без наличия проверок на значение Nothing. Это исчерпывающее решение возможных вариантов обработки подобной ситуации является серьезной полемикой «исключение или возвращаемое значение» при возникновении ошибки во многих других языках. Но она не имеет однозначного ответа, как лучше поступать. Возвращаемые значение – это хорошо, когда вы сразу проверяете его, исключения хороши, когда вы их обрабатываете на верхних уровнях выполнения программы. Данный же код, просто делает так, как вам удобно обрабатывать подобную ситуацию.

Детали данного примера специфичны для Haskell, но подобные примеры могут быть сконструированы во многих статически типизированных языках. Нет оснований полагать, что код на ML или Haskell более длинный, чем эквивалент на Python или Ruby. Следует запомнить это, прежде чем заявлять, что статически типизированные языки требуют большего объема кода. Это неочевидно, и у меня по этому поводу большие сомнения.

Преимущества статической типизации.

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

Существует ряд основных преимуществ статической типизации. Я перечислю их в порядке увеличения значимости. (Это поможет для формирования структуризации)

Производительность

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

Для большинства вычислительных окружений, производительность – это та проблема, которая осталась в прошлом. Проблемы последнего десятилетия отличаются от тех, что были раньше, и во многом благодаря новым технологическим достижениям. У нас есть новые проблемы, и проблемы производительности, уже не так актуальны, как прежде.

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

Документирование

В самом деле, если не стоит вопрос о производительности, на чем тогда заострить внимание? Одним из вариантов может быть документирование. Документирование – это важный аспект программного обеспечения, и статическая типизация может здесь помочь.

Почему? Потому что документирование – это не только комментарии к исходному коду. Это все, что помогает людям понять программное обеспечение. Система статических типов построена на идее, помогающей объяснить систему и задачи, которые она выполняет. Получение информации о входных и выходных параметрах различных функций и модулей. Это именно та информация, которая необходима для документирования. Конечно, если все данные об ньюансах исходного кода описаны в комментариях, то вполне может случиться, что, в конечном счете, эта информация в процессе поддержки исходного кода может стать не актуальной. Если эта информация будет описана в именах идентификаторов, то станет практически невозможно таким образом описать все необходимые аспекты. Это доказывает тот факт, что использование для подобных целей информации описываемой типом это очень хорошее решение.

Это наскучившее мнение. Как известно каждому, лучше иметь самодокументируемый код, чем исходный код, требующий хоть небольшого количества комментариев (даже если он их и имеет!). Достаточно удобно, что большинство языков с интересной статической системой типов имеют в своем арсенале механизм выводимости типов, который является непосредственным аналогом самодокументируемого кода. Информация необходимая для правильного использования части кода извлекается из самого кода (то есть он самодокументируемый), но только когда он верифицирован и представлен в подходящем формате. Эта информация, которую не нужно поддерживать или даже записывать, но она доступна по требованию даже без чтения исходного кода.

Инструменты и анализ

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

Фундаментально новым может быть возможность систем типов помочь понять код компьютерным программам. Хотя здесь необходимо некоторое пояснение. В конце концов, один мудрый человек (если мне не изменяет память Мартин Фаулер) сказал:

«Любой дурак может написать код, который понятен компьютеру. Хороший же программист пишет код, который понятен человеку.»

Я не согласен с Мартином, но у нас с ним различный смысл слова понимание. Понимание компьютером кода шаг за шагом – это несложно. Способность компьютера проанализировать код и решить более сложные вопросы, чем просто построчное понимание им кода, это совершенно другое, и это очень сложно.

Мы часто хотим, чтобы наши инструменты разработки понимали то, что мы пишем. Это великое дело. Можно опять таки возвратиться к Мартину Фаулеру, который хорошо это отметил.

Корректность

В конечно счете, оправданием статической типизации является возврат к написанию корректного кода. Корректность, естественно, это когда программа делает то, «что вы хотите».

Это действительно трудноразрешимая проблема, если разрешимая вообще. У теории вычисления есть подобные наработки, называемые Теоремой Райса (Rice's Theorem), которая гласит следующее: «Если взять произвольную программу, написанную на языке программирования общего назначения, то невозможно написать для нее компьютерную программу, позволяющую определить выходные данные этой программы». Если я буду обучать студентов программированию и дам им задание написать «Hello World», я не смогу воспользоваться другой программой для определения правильно ли работает написанное студентом решение. Найдутся некоторые программы, для которых ответ прост; если программа никогда не использует операции ввода/вывода, то значит ответ отрицательный. Если программа состоит из одного выражения печатающего результат, также несложно определить – решено задание или нет. Однако, могут быть и более сложные программы для которых определить корректность результата невозможно. Несущественный, но важный технический момент: нельзя запустить программу и дождаться, пока она выполнится, так как программа может не завершиться вовсе! Это справедливо для любого высказывания о программе, включая такие интересные, как «это программа имеет завершение?» или «эта программа нарушает мои правила безопасности?»

Учитывая, что фактически мы не можем проверить правильность программы, существует два подхода, которые помогут нам добиться приблизительного результата:

• Тестирование: устанавливает верхние границы корректности
  

• Доказательство: устанавливает нижние границы корректности
  

Конечно, мы больше озабочены нижними границами, чем верхними. Проблема с доказательством, такая же, как и проблема с документированием. Доказательство корректности тривиально только до некоторого времени в случае, когда для доказательства вы имеете постоянное тело кода. Когда исходный код поддерживается тремя программистами и подвергается изменениям семь раз в день, поддержание доказательства корректности становится невозможным. Статическая типизация здесь играет ту же роль что и в случае с документированием. Если (и только если) вы можете получить доказательство корректности, поступая определенным образом так, чтобы можно было воспроизвести эту последовательность действий на компьютере, компьютер сам может составить доказательство, которое позволит вам узнать, не нарушили ли корректность проведенные вами изменения кода. Фраза «определенным образом» - здесь означает структурную индукцию над синтаксисом кода, а доказательство называется проверкой типа.

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

А что с динамической типизацией?

Конечно, динамическая типизация имеет ответ на это. Динамически типизированные языки иногда могут исполняться достаточно хорошо (например, Dylan), иногда иметь огромный инструментарий (например, Smalltalk), и я уверен, что порой, они обладают хорошей документированностью, но предоставить сейчас такой пример, к сожалению, я не могу. Это ни в коей мере не понижает важность статической типизации, но это бесспорные факты.

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

Динамические языки для определения корректности используют тестирование. Напомню, что тестирование делает возможным только лишь определение верхних границ корректности. Дейкстра сказал об этом наилучшим образом: “Тестирование программы может использоваться для определения наличия ошибок, но не для проверки на их отсутствие”. Полагаю, что если кто-либо не сможет определить наличие ошибок, то вполне вероятно, что их нет. Если кто то не сможет доказать наличия лучшей верхней границы корректности, то вероятно действительно корректность такой программы 100%. Естественно, не стоит забывать о возможной корреляции этой позиции.

Что такое тип?

Это хорошая идея, сделать шаг назад и задаться фундаментальным вопросом: что такое тип? Я уже упомянул, что с моей точки зрения есть два ответа. Один для статической типизации, а другой - для динамической. Я рассмотрю вопрос для статических типов.

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

Проблемы с общими определениями

Одно общее высказывание, часто цитируемое в попытке согласовать особенности статической и динамической типизации, звучит подобным образом: статически типизированные языки присваивают типы переменным, тогда как динамически типизированные - значениям. Конечно, это в действительности не определяет понятие типа, но это уже очевидно и заведомо неверно. Можно исправить эту проблему, в определенной степени, констатировав, что "статически типизированные языки присваивают типы выражениям..." Однако, в таком случае типы становятся полностью аналогичны случаю с динамической типизацией, и это весьма сбивает с толку.

Итак, что такое тип? Когда типичному программисту задают этот вопрос, то у него может появиться несколько ответов. Возможно тип – это просто множество возможных значений. Возможно, это множество операций (очень структурно ориентированный взгляд на тип, чтобы быть уверенными в этом). Есть несколько аргументов в защиту каждого из этих ответов. Можно составить список: целые числа, действительные числа, даты, время, строки и так далее. Но в конечно счете, проблема в том, что это все скорее признаки, чем определения типа. Почему тип это множество значений? Потому что мы хотим быть уверенными в том, что программа не будет вычислять квадратные корни строковых переменных. Почему тип это множество операций? Потому что мы хотим знать, не попытается ли наша программа выполнить что-то недопустимое.

Давайте посмотрим на другие вещи, которые мы часто хотим знать: помещает ли наше веб-проложение данные клиента в SQL-запросы перед их отправклой? Если это то, что мы хотим знать, то почему бы не назвать это типом. Данная статья Тома Мортела построена как раз на таком подходе, и использует систему типов Haskell. Таким образом, это выглядит, как обоснованное определение “типа”: что-то, о чем мы хотим знать.

Система типов

Понятно, что это не достаточное определение типа. Есть множество вещей, которые мы хотим знать, о которых типы не могут сказать нам. Мы хотим знать, является ли наша программа корректной, но я уже говорил, что типы не в полной мере обеспечивают нас нижней границей корректности, и не исключают необходимости тестирования или ручного доказательства. Что тогда делает тип типа? Другим взглядом на тип является тот факт, что тип является частью системы типов.

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

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

Это комплексное определение, и его ключевая идея заключается в следующем:

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

• доказательство отсутствия определенного поведения программы: Это цель. Не существует списка "определенного" поведения. Фраза просто означает, что для любого конкретного типа системы, будет список сущностей, которые она сумеет доказать. Вопрос, что именно она доказывает и как, остается открытым. (Далее в тексте: "... каждая система типов содержит определение поведений, которая она имеет целью предотвратить".)
  

• легко поддающийся обработке: Это просто означает, что метод завершается в разумные сроки. Не желая претворить свои слова в уста кого-либо, я думаю, что можно с уверенностью сказать, большинство людей согласится, что ошибочно включать это в определение системы типов. Некоторые языки имеют даже нерешаемые системы типов. Тем не менее, это, безусловно, общая цель; никто не ожидает, что компилятор будет два года заниматься проверкой типов программы, даже если программа будет запущена на два года.
  

Последний фрагмент определения главным образом не является определяющим. “Вид значений, которые они вычисляют” по сути, это не несет определяющего смысла в контексте определения интересующих нас вопросов.

Пример к данному определению выглядит примерно так. Получено выражение 5 + 3 механизм проверки типов (type checker) может взять первый операнд ‘5’ и прийти к выводу, что результатом операции будет целое число. Также он может взять второй операнд ‘3’ и опять таки прийти к такому же выводу. Также он может взять оператор ‘+’ и сделать заключение, что данный оператор применим для двух целых чисел, и результат его выполнения так же целое число. Так доказывается отсутствие определенного поведения программы (таких, как добавление целого числа к строке) вызовом базовых элементов синтаксиса программы.

Примеры необычных систем типов

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

• http://wiki.di.uminho.pt/twiki/pub/Personal/Xana/WebHome/report.pdf Использование типов для гарантии корректности вида данных получаемых из реляционной базы данных. Используя систему типов, компилятор не в состоянии понять, как работать с концепциями подобных функциональных зависимостей и нормальных форм и осуществляет статическое доказательство уровней нормализации.
  

• http://www.cs.bu.edu/~hwxi/academic/papers/pldi98.pdf Использование расширения для системы типов ML, с целью доказательства, что массивы никогда не получат доступ за пределами своих границ. Это необычно тяжелая проблема для решения ее с помощью языков, у которых нет подобной реализации на уровне системы типов.
  

• http://www.cis.upenn.edu/~stevez/papers/LZ06a.pdf Замечательная статья. Данный пример использует систему типов Haskell для возможности определения политики безопасности программы Haskell и доказывая после этого что программа должным образом реализует эту безопасность. Если программист делает ошибку безопасности, компилятор скорее выразит свое недовольство, чем сделает возможным потенциальную ошибку безопасности в системе.
  

• http://www.brics.dk/RS/01/16/BRICS-RS-01-16.pdf Только в целях размышлений о системах типов, решение простой проблемы, немного кода на Haskell использующего систему типов для доказательства двух основных теорем о простом типизированном лямбда-исчислении, ветви теории вычислений.
  

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

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

Истинное значение типа

И все же, что такое тип? Единственно верное определение: тип это метка, используемая системой типов для доказательства некоторых свойств поведения программы. Если механизм проверки типов в состоянии назначить типы для всей программы - он получит доказательство корректности программы; иначе он потерпит неудачу и укажет на причину этого. Это и есть определение, но он не говорит нам ничего фундаментально важного. Некоторые дальнейшие исследования приводит нас к пониманию фундаментальных ньюансов, связанных с использованием механизма проверки статических типов.

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

Это различие означает, что статически типизированная система достаточно осторожна в оценке корректности. Если она пропускает некоторый код, то мы знаем, что его корректность доказана механизмом проверки типов. Если проверка потерпела неудачу... то в таком случае нам ничего не известно. Возможно, что такой код имеет некоторую некорректность, или, возможно, механизм проверка типов не способен вывести доказательство для, в принципе, корректного кода. Кроме того, существует строгое математическое доказательство того, что механизм проверки типов всегда достаточно консервативен. Создание механизма проверки типа, который принимает любые корректные программы, является очень нетривиальным; И по сути это невозможно.

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

Развитие дискуссии

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

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

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