О понимании типов ,абстракций данных и полиморфизма.

Автор: Luca Cardelli.

Резюме

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

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

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

Типовое лямбда-исчисление расширяется всеобщей квантификацией ( это кванторы всеобщности для любого x типа A в функции F(x) ) для моделирования шаблонных(§епепс) функций с параметрами-типами ( шаблонная функция определяет абстрактную операцию , указывая имя операции и список параметров ,но не реализацию. Она шаблонная в том смысле ,что она может принимать любые объекты в качестве аргументов.Но сама по себе шаблонная функция не может ничего делать.Если мы просто определим шаблонную функцию , то без разницы с какими параметрами мы её вызовем она будет выдавать ошибку.Чтобы шаблонная функция обрабатывала определенные аргументы мы должны определить одну или более реализаций шаблонной функции ,называемых методами.Каждый метод представляет реализацию шаблонной функции для определенных классов аргументов);расширяется кванторами существования и пакетированием(сокрытие информации) для моделирования абстракных типов данных;расширяется кванторами ограничения для моделирования выделения подтипов и наследования типов. Итак мы получаем простое и точное описание мощной системы типов ,котороая включает в себя абстрактные типы данных ,параметрический полиморфизм и множественное наследование в единой непротиворечивой среде. Обсуждаются механизмы проверки типов для расширенного лямбда исчисления. Расширенное лямбда исчисление используется как язык программирования для различных пояснительных примеров.Мы будем называть этот язык Fun вместо лямбда (Fun ключевое слово для абстракции функций) так как это удобнеешп матиматически прост и может служить как основа для построения и реализвции реального языка программирования с системой типов ,которая более мощная и выразительная чем существующие системы в других языках программирования.В частности этот язык может служить основой для построения строго типизированного объектно-ориентированного языка.

1. От нетипизированных к типизированнным множествам

1.1.Организация нетипизированыых множеств

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

(1)Битовые строки в памяти компьютера

(2)S-выражения в читсом Lisp

(3)Х-выражения в Х-исчислении

(4)Множества в теории множеств

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

Лисповские S-выражения формируют другое нетипизированное множество ,которое обычно строится на вершине предыдущего множества битовых строк. Программы и данные не различаются и в конечном итоге все они - S-выражения. Опять мы имеем только один тип (S-выражение) ,хотя этот тип более структурирован(различаются атомы и последовательные ячейки) и этот имеет лучшие свойства нежели битовые строки.

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

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

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

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

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

Эти вопросы нехорошее последствие организации нетипизированных множеств не пройдя всего пути к типизированным системам.

1.2 Статическое и строгое типизирование

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

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

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

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

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

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

1.3 Виды полиморфизма

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

( parametric universal <

( inclusion

polymorphism

( overloading ati-hoc <

С coercion

Figure 1: Varieties of polymorphism. Straychey [67] различал неформально два главных типа полиморфизма.