Лекция 12
3.5. Проверка типов
Для обсуждения проверки типов обобщим понятия операндов и выражений, чтобы включить в эти понятия подпрограммы и операторы присваивания. Будем считать вызовы подпрограмм выражениями, операндами которых являются их параметры. Символ присваивания будем рассматривать как бинарную операцию, а операндами будут l-переменная и r-выражение.
Проверка типов обеспечивает совместимость операндов выражения. Совместимым называется тип, который изначально допускается для данного выражения, либо правила языка позволяют с помощью команд компилятора неявно преобразовать его в тип, допускаемый для данного выражения. Это автоматическое преобразование называется приведением. Применение выражения к операнду неприемлемого типа называется ошибкой определения типа.
Если в языке все связывания переменных с типами являются статическими, то проверка типов, как правило, всегда может выполняться статически. Динамическое связывание типов требует проверки во время выполнения программы, называющейся динамической проверкой типов.
Некоторые языки, например APL и SNOBOL4, осуществляющие динамическое связывание типов, допускают только динамическую их проверку. Однако лучше обнаруживать ошибки во время компиляции, поскольку исправление на ранних стадиях, как правило, обходится дешевле. Платой за статическую проверку типов является снижение гибкости программирования.
Проверка типов осложняется, если язык позволяет хранить в ячейке памяти в разное время выполнения программы величины разных типов. Это можно сделать, например, с помощью вариантных записей языков Ada и Pascal, оператора EQUIVALENCE языка FORTRAN, объединений языков C и C++. В этих случаях проверка типов, если она производится, должна быть динамической, кроме того, она требует, чтобы система поддержки выполнения программ хранила типы текущих значений, записанных в таких ячейках памяти. Таким образом, даже если в языках, подобных C и Pascal, все переменные статически связаны с типами, не все ошибки определения типа будут выявлены при статической проверке типов.
3.6. Строгая типизация
Одной из идей «структурной революции» в программировании 1970-х годов была строгая типизация, признанная весьма полезной концепцией. В программах на строго типизированном языке каждое имя имеет связанный с ним тип, известный во время компиляции. Основой такого подхода является статичность связывания всех типов. Его слабая сторона – игнорирование того факта, что ячейка памяти, с которой связана некоторая переменная, в разное время может содержать величины различных типов. Чтобы учесть эту возможность, можно определить строго типизированный язык таким образом, чтобы в нем всегда могли обнаруживаться ошибки типов. Для этого требуется, чтобы типы всех операндов могли определяться либо во время компиляции, либо во время выполнения. Важность строгой типизации заключается в возможности выявления всех неправильных употреблений переменных, приводящих к ошибкам определения типов. Строго типизированные языки позволяют также обнаружить (в процессе выполнения) использование величин некорректных типов в переменных, которые могут содержать величины нескольких типов.
Язык FORTRAN не принадлежит к строго типизированным языкам, поскольку в нем не проверяются соответствия между фактическими и формальными параметрами подпрограмм. Кроме того, использование оператора EQUIVALENCE между переменными различных типов позволяет переменной одного типа ссылаться на переменную другого типа.
Язык Pascal относится к почти строго типизированным языкам. Этим «почти» он обязан своей структуре вариантных записей, которые позволяют совмещать значения различных типов без возможности их проверки.
Язык Ada также почти строго типизирован. Хотя в нем содержимое вариантных записей динамически проверяется на наличие величин корректных типов, он позволяет программистам нарушать правила проверки, вводя требование о временной отсрочке проверки для конкретного преобразования типов с помощью специальной системной функции UNCHECKED_CONVERSION.
Языки C и C++ не относятся к строго типизированным языкам, поскольку в них допускаются функции без проверки типа параметров. Кроме того, типы объединений в этих языках также не проверяются.
Строго типизированным является язык ML, правда, с некоторыми отличиями от императивных языков. В ML все типы переменных известны статически из объявлений либо правил логического вывода типов (см. п.3.4.2.3).
Языки Java и C#, хотя они в значительной мере созданы на основе C++, являются строго типизированным в том же смысле, что и язык Ada. Типы могут приводиться явно, что может вызвать ошибку определения типа. Тем не менее, не существует неявных путей, позволяющих ошибкам определения типа остаться незамеченными.
Правила приведения типов существенно влияют на результаты их проверки. Выражения в языке Pascal строго типизированы, но допускается использование арифметических операций с операндами различных типов. Например, возможна операция сложения вещественной и целой величин. Значение целого операнда приводится к числу с плавающей точкой, и в результате выполняется операция над числами с плавающей точкой. Такое, казалось бы, естественное приведение типов снижает результат строгой типизации – возможность выявления ошибок. Языки, в которых широко используется приведение типов, например, FORTRAN, С и C++, значительно менее надежны, чем языки, в которых приведение типов применяется нечасто, например, Ada. В языках Java и C# содержится существенно меньше возможностей приведения типов, чем в C++.