Декларативное программирование

[ Содержание | 1 | 2 | 3 | 4 | 5 | 5.1 | 5.2 | 5.3 | 5.4 | 5.5 | 5.6 | 5.7 | 5.8 | 5.9 | 6 | 6.1 | 6.2 | 6.3 | 6.4 | 6.5 | 7 | 7.1 | Литература ]

© 2003 И.А. Дехтяренко

7. Типы

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

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

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

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

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

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

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

domains
IntList = Integer*
StringList = String*
RealList = Real*

predicates
append_int(IntList,IntList,IntList)
append_real(RealList,RealList,RealList)
append_string(StringList,StringList,StringList)

clauses

append_int([], X, X).
append_int([H|T], X, [H|L]) :- append_int(T, X, L).

append_real([], X, X).
append_real([H|T], X, [H|L]) :- append_real(T, X, L).

append_string([], X, X).
append_string([H|T], X, [H|L]) :- append_string(T, X, L).

А если учесть что кроме append нужны еще и другие процедуры для списков стиль программирования покажется несколько надоедливым. Впрочем, привыкшим к Си или Паскалю, возможно и не покажется.

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

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

Термин "полиморфизм", введенный в практику Кристофером Стрейчи означает возможность использовать ту же самую функцию с различными типами данных. Стрейчи определил и два вида полиморфизма: параметрический полиморфизм и специальный (ad hoc) полиморфизм.

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

Другой вид полиморфизма, ad hoc полиморфизм или перегрузка, связан со способом записи, а не со способом определения процедур. Примером может служить функция сложения. Мы часто обозначаем сложение целых чисел и сложение действительных чисел одним и тем же знаком "+". Это похоже на применение append к двум спискам целых чисел и двум спискам действительных чисел. Однако схожесть лишь частичная: функция append использует один и тот же алгоритм для соединения списков любого типа, но алгоритм сложения целых чисел отличается от алгоритма сложения действительных чисел. То есть символ "+" используется в сущности для обозначения двух различных функций (в алгоритмическом смысле этого слова). В каждом конкретном случае выбор функции, которую следует использовать, зависит от типа аргументов. ML не позволяет определять перегруженные функции, но некоторые встроенные функции уже перегружены, что как раз и создает проблемы с выводом типов. Дело еще более осложняется, если язык программирования допускает неявное приведение типов.

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

• 7.1 Типы в ML.

[ Содержание | 1 | 2 | 3 | 4 | 5 | 5.1 | 5.2 | 5.3 | 5.4 | 5.5 | 5.6 | 5.7 | 5.8 | 5.9 | 6 | 6.1 | 6.2 | 6.3 | 6.4 | 6.5 | 7 | 7.1 | Литература ]