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




страница1/5
Дата14.07.2016
Размер0.68 Mb.
  1   2   3   4   5
О понимании типов ,абстракций данных и полиморфизма.

Автор: Luca Cardelli.

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

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

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

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



Содержание


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

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

    2. Статичное и строгое типизирование.

    3. Типы полиморфизма.

    4. Эволюция типов в языках прогаммирования.

    5. Подмножество языка выражения типов.

    6. Предварительное рассмотрение Fun.

  2. Лямбда исчисление.

    1. Безтиповое лямбда исчисление.

    2. Типовое лямбда исчисление.

    3. Основные типа , структурированныу типы , рекурсия.



  1. Типы и множества значений.

  2. Кванторы всеобности.

    1. Кванторы всеобщности и порождающие функции.

    2. Параметрические типы.

  3. Кванторы существования.

    1. Кванторы сущестования и сокрытие информации.

    2. Пакетирование и абстрактные типы данных.

    3. Совместное использование кваторов существования и всеобщности

    4. Кванотры и модули.

    5. Модули это значения первого класса.

  4. Кванторы ограничения.

    1. Включения типов ,поддиапозоны и наследование.

    2. Ограниченный кваторы всеобности и выделение подтипов.

    3. Сравнения с другими механизмами выделения подтипов.

    4. Ограниченные кванторы существования и частичная абстракция.

  5. Проверка и выводимость типов.

  6. Иерархическая классификация систем типов.

  7. Выводы.



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


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

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



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

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

  3. λ-выражения в λ-исчислении

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

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

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

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

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

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

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

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

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

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

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

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

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



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


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

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

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

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

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

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

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

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

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


Здесь перегрузочный полиморфмизм + может быть объяснен следующим способом.

- Оператор + имеет 4 прегруженные значения , один для каждой комбинации типов аргументов.

- Оператор + имеет 2 перегруженных значения , котороые соответствуют сложению целых и действительных чисел.Где один из аргументов это целое число ,а другой это действительное,в этом случае целое число приводится к типу действительного.

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

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



  1. Перегрузка : целые константы могут быть как типа integer так и типа real.Операции такие как + применими аргументам как типа Integer так и типа real.

  2. Приведение типов: значения типа integer могут использоваться там же где и значения типа real и наоборот.

  3. Выделение подтипов: элементы принадлежащие к поддиапозону типов ,принадлежат также к диапозону типов содержащий этот поддиапозон.

  4. Совметсное использование значений: nil в Паскале это константа ,которая совместно используется всеми типами указатель.

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

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

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

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

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

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

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

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

Четыре рассмотренных способа ослабления мономорфной типизации становятся более мощными ,когда мы рассматриваем их в связке с операторами ,функциями и процедурами.Давайте рассмотрим некоторые примеры.Символ + может быть перегружен для использования в одно и тоже время в качестве суммы типов integer ,типов real ,типов string.Использование одного и того же символа для этих трех операций отражает приблизительные похожесть алгебраической структуры ,но нарушает требование мономорфности.Противоречивость может быть устранена типами операндов в перегруженном операторе ,но этого может быть недостаточно.Например ,если 2 перегружено для определения целого 2 и действительного 2 ,то 2+2 останется неопределенным и разрешается это только присваиванием типовой переменной.

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

Полиморфизм вклячения может быть обнаруженво многих языках ,в котрых Симула 67 это самый ранний пример.Классы Симулы это определенные пользователем классыорганизованные в просто наследовательной иерархии,где каждый класс имеет единственный суперкласс.Объекты и процедуры Симулы полиморфны , так как объекты подкласса могет появится там где требуется объект суперкласса.Хотя Smalltalk это нетипизированный язык ,он тоже использует немного полиморфизма.Недавно Лисп расширил этот стиль полиморфизма до непосредственных суперклассов.Язык ,который представляет парадигму параметрического полиморфизма это ML ,который изначально был построен вокруг этого стиля типизирования.В ML вы можете написать тождественную функцию ,которая работает с любыми типами аргументов , функцию length ,которая отображает список на целое число.Также возможно шаблонную функцию сортировки ,которая сортирует элементы любых типов.

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

  1   2   3   4   5


База данных защищена авторским правом ©uverenniy.ru 2016
обратиться к администрации

    Главная страница