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

Определяет тип функционального параметра f как шаблонный тип и принимает функции любого типа и возвращает значения этого же типа. Означенные функции f в теле twice1 должны иметь формальный парметр типа f[t] и требуеют, чтобы был предоствлен фактический тип, при означивании функции twice1.Полное определение twice1 требует связывания параметра-типа t как универсально квантифицированного типа и связывания x к t.

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

all[t] - требует фактический параметр-тип

- требует функцию типа

f(x:t) - требует аргумента подставляемого вместо типа t.

Означивание функции twice1 типа Int функцией Id и аргументом 3.

Заметьте что третий аргумент 3 имеет тип Int первого аргумента и что второй аргумент Id универсально кватинфицированный тип. Заметьте что twice1[Int](succ) не будет правильным так как succ не имеет тип

Функция twice2 отличается от twice1 типом аргумента f ,куоторый не универсально квантифицирован. Сейчас нам не надо означивать f[t] в теле twice:

Сейчас возможно посчитать twice как succ.

Поэтому twice2 сперва принимает параметр –тип Int, который служит для конкретизировать тип функции f :Int -> Int, потом принимает в качестве параметра функцию succ этого типа, и потом принимает специальный элемент типа Int, которым функция означивается дважды. Дополнительное означивание требуется для twice2 от id, который должен быть первым конкретизирован типом Int:

Заметьте, что как λ-абстракция так и универсальная квантификация связывают опеаторы

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

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

В Fun типв и значения строго отличаются(значения это объекты, а типы это множества); следовательно нам нужно 2 разных механизма связывания : fun и all. Эти две модели связывания могут быть объединены, в некоторых моделях, где типы это значения, достигая некоторой экономии конценпций, но это объединеие не подходит под нашу базовую семантику. В таких моделях возможно объединить параметрический механизм связывания описанный в следующей главе с fun и all.

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

Если у нас есть два одинаковых определения типа похожей структуры, например:

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

Объявление типа просто вводит новое имя для выражения типа и оно эквивалентно выражению этого типа в любом контексте. Объявление типа не вводит нового типа. Следовательно 3,4 это IntPair, так как оно имеет тип Int*Int – определение IntPair.

Параметрическое определение типа вводит новое определение оператора типа.Pair сверху это оператор типа отображающий тип Т на Т*Т. Следовательно Pair[Int] это тип Int*Int и следовательно 3,4 имеет тип Pair[Int].

Операторы типов это не типы ; они только опереируют над типами. В частности они не должны нарушать следующие нотации:

Гдеэто оператор типа, который когла он применяется к типу Т дает функциональный тип T->T и В это тип функции идентификации и никогда не применяется к типам.

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

Шаблонный пустой список может быть определен и потом конкретизирован как:

Сейчас [nil=()] имеет тип List[Item] для любого Item. Следовательно типы шаблонного nil и его конкретных представлений

Похоже мы можем определить шаблонную функцию cons и другие операции над списками.

Заметьте, что cons может строить только однородные списки, так как его аргументы и результат относятся к одному типу Item.

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

5. Экзистенциональная квантификация.

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

Имеет свойство для некоторого типа а, р имеет тип t(a)

Например:

где а = Int в первом случае и а=Int*Int во втором.

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

Определяет множество всех значений, которые мы должны иногда называть Top(наибольший тип):

тип любого значения.

Множество всех упорядоченных пар может быть определено следующим экзстенциональным типом.

тип любой пары.

Это тип любой пары p, q,так как для некоторого типа и для некоторого типа b, p и q имеют тип a*b. Тип любого объекта вместе с операцией возвращяющей integer, которая может быть применена к нему может быть определен следующим экзистенциональным типом.

Пара (3,succ) имеет этот тип, если мы возмем а=Int. Аналогично пара ([1,2,3],length) имеет этот тип, если мы возмем а=List[Int].

Так как типы включает не толькопростые типы но еще и универсальные типы и тип Top, ъкзистенцианально квантифицированные типы имеют некоторые свойства, котрые могут спевар показаться не интуитивными. Тип *а это не просто тип пар эквивадентных типов, как некотроые могут ожидать. В действительности даже тип 3,true имеет этот тип. Мы знаме, что 3 и true имеют тип Top, следовательно есть тип а=Top, такой что 3,true:a*a. Поэтому тип это тпи всех пар, также как Также любая ффункция имеет тип ,если мы в качестве а возмем Top.

Однако это отношение между типом объектом и типом функией, возвращающей integer. Например (3,length) не имеет этого типа (если посчитаем 3 типом Top, тогда нам надо показать, что length имеет тип Top-> Int, но мы уже знаем что, Length имеет тип , который отображает целочисленный список на integer, и мы не моджем предположить ,что произкольный объект типа Top можно отобразить на Integer)

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

Экзистенционально типипзированные объекты могут быть полезны, если они достаточно структурированны. Например x: предоставляет достаточную структурированность, чтобы над ним проводить вычисления. Мы можем выполнить:

и получить integer.

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

Эти экзистенциональные типы могут быть использованы ,например, разнородных списков:

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

5.1 Экзистенциональная ква нитфикация и сокрыие информации.

Реальная польза экзистенциональных типов становится видимой, только тогда когда мв понимаем, что простой пример абстракции данных с множеством своих операций. Переменная а сама является абстрактным типом, котрый скрывает представление. Представление было Int и List[Int] в предыдущем примере. Тогда это множество операторов над абстрактным типом: константа типа а и оператор типа a -> Int. Эти оперраторы не обозначены, но мы можем ввести обозначенные версии, используя тип запись вместо декартова произведения:

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

Как мы объявляли ранее, мы были немного свободны в применении разных операторов к объектам экзистеционального типа. Это будет теперь запрещено, чтоюы сделать наш формализм более простым для проверки типов. Вместо этого мы будем иметь явные языковые кострукции для создания и манирулироввания объектами экзистенционального типа, так как мы имели абстракции типов all[t] и означивание типов exp[t]

Для создания и использования объектов универсальных типов.

Обычный объект (3,succ) может быть в абстрактный объект, имеющий тип

при помощи пакетирования и поэтому некоторая структура его скрыта. Операция pack снизу инкапсулирует объект (3,succ) , так чтобы пользователь знал только, что это объект типа существует без знания фактического объекта. Естествено подумать, что результирующий объект имеет экзитсенциональный тип

Пакетированный объект такой как р называется пакетом. Значение (3,succ)

Это содержание пакета. Тип это интерфейс: он определяет структурное пределение содержания и соответствует определению части абстракции данных. Связывание а=Int это представление типов : оно связывает абстрактный тип данных с конкретным представлением Int и соответствует скрытому типу данных ассоциированный с абстракцией данных.

Общая форма операции pack

Операция pack это единственный механизм для создания объектов экзистенционального типа. Таким образом если переменная экзистенционального типа была объявлена так :

Тогда р может брать только значения созданные операцией pack.

Пакет должен быть открыт перед тем как его использовать

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

к компонентам открытого пакета можно обращаться по имени.

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

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

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

И pack и open не имеют влияния времени выполнения на данные. Предоставляя достаточно умный проверяльщик типов, некоторые могут опустить эти конструкции и вернуться к нотации, использованной с предыдущих секциях.

5.2 Пакеты и абстрактные типы данных.

Чтобы проиллюстрировать применимость нашей нотации к реальным языкам программирования, мы покажем как записи с функциональными компонентами могкт быть исползованы для моделирования пакетов в Ада и как экзистенциональная квантификация может быть использована для моделтрования абстракций данных в Ада[83].Рассмотрим тип Point1 лдя создания геометрических точек от глобально определенного типа Point – пары действительных чисел и для выбора х и у координат точек.

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

В Ада пакет с функциями makepoint, x_coord, y_coord может быть определен так:

Определение пакета это не определение типа, но частично определение значения. Чтобы завершить определение значений в Ада, мы должны представить тело пакета в следующей форме:

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

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

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

Package body localpoint is

Point :Point ; -- разделяемая глобальная переменная функций marketpoint, x_coord, y_coord

Скрытые локальные переменные могут быть реализованы в нашей нотации при помощи конструкции let.

Хотя Ада не имеет концепции типа пакета, она имеет определение понятия шаблона пакета, который имеет некоторые, но не все свойства типа. Шаблоны пакетов вводятся ключевым словом generic

Значения point1 и point2 шаблонного пакета Point1 могут быть введены как:

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

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

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

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

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

В Ада пакет point2 с приватным типом Point может быть определен как :

Приватный тип Point может быть смоделирован при помощи кваторов существования.

Иногда удобно представлять определение типа экзистенционально квантифицированного типа как параметрическую функцию от скрытого параметра-типа. В примере мы можем определить Point2WRT[Point] так:

Нотация WRT в Point2WRT должна читаться как, подчеркивает тот факт, что это определение типов соотносится с парамертром-типом. Значие point2 экзистенционального типа Point2 может быть создан операцией pack.

Оперция pack скрывает представление Real*Real типа Point и имеет экзистенционально параметризируемый тип Point2WRT[Point] как часть своего определения и предоставляет как свой скрытые тело предыдуще определеного типа point1 , который реализукет операции для данного представления данных.

Заметьте, что Point2WRT[Point] представляет параметризированный типовое выражение, которое предоставляется с фактическим параметром таким как Real, устанавливает тип ( в случае типа записи с тремя компонентами).Отношение между ътим типом параметризации и дургим видом параметризации представленным только недавно проиллюстрированы ниже:

1.Функциональная абстракция : fun(x:type) value-expr(x).Параметр х это значение и результат подстановки фактического параметра вместо формального определяет значение.

2.Квантификация :all(a) value-expr(a).Парамеир а это тип и результат подстановки фактического параметра вместо формального определяет значение.

3.Абстракция типов. TypeWRT[T] = type –expr(T).Параметр Т это тип, результат подстановки формального параметрав вместо фактического тоже тип.

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

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

5.3 Комбинирования универсальной и экзистенциональной квантификации.

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

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

Мы начинаем с конкретного типа IntListStack c целочисленными элементами и списковым представлением данных. Этот конкретный тип может быть реализован как кортеж операций без всякой квантификации.

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

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

Пример IntArraySTack это пример типа кортежа с полдями операции инициализиваронными операциями представления стека в виде массива.

Конкретный стек выше может быть обощен элементы шаблонеными типами и скрывая реализацию стека. Следцющий пример илюстрирует как шаблонный тип моэет быть реализован универсальной квантификацией. Сперва мы определим тип GenericListSTack

Как универсально квантифицируемый тип.

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

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

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

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

Тип с двумя параметрами GenericStackWRT[Item][Stack] может быть в свою очередь определен как кортеж двойных параметризированный операций.

Заметьте, что нет ничего в жтом определении, чтобы различать роли этих двух параметров Item и Stack. Однако в определении GenericStack параметр Item универсально квантифицирован, показывая, что он представляет скрытый абстрактный тип данных.

Мы можем сейчас абстрагировать наши genericListStack и genericArrayStack пакеты в пакет типа GenericStack:

Оба listStackPackage и arrayListPackage имеют один и тот же тип и мало отличаются формой представления скрытых данных.

Более того функции такие как useStack могут работать без знания о реализации:

И можно дать любую реализацию GenericStack как параметра:

В определении GenericStack тип Stack в большинстве не относится к Item, но наша цель в том, что какая бы не была реализация Stack ,стеки должны быть коллекциями элементов. Из-за этого возможно построение объектов типа GenericStack, где стеки не могут ничего джелать с эелементами, и не подчиняются свойствам таким как : Это ограничение является правильным в более мощных системах таких как {86] и [84] ,где можно деалть абстрактными операторы типов вместо самих типов, и некоторые могут напрямую выражать, что предствление Stack должно быть онсовано на Item (но даже в таких более выразительных системах типов возможно возможно так подделать пакеты стека, что он не будет подчинятся свойствам стека)

5.4 Квантификация и модули

Сейчас мы уже готовы для большого примера: геометрические точки. Мы введим абстрактный тип с поерациями mkpoint(создает новую точку от двух действительных чисел), x-coord и y-coord (возвращает x-ую и у-ую координаты):

Наша цель определить значения этого типа, которые скрывают и представление PointRep и реализацию поераций mkpoint, x-coord и y-coord по отношению к этому преставлению.

Чтобы завершить это мы определим тип этих операций как параметрические типы с PointRep в качесвте параметра. Имя типа PointWRT подчеркивает ,что операции определены по отношению к определенномупредставлению и наоборот асьтрактный тип Point независит от представления.

Экзистенциональный тип Point может быть определен в терминах PointWRT при помощи экзистенциональной абстракции по отношению к PointRep.

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

Давай те определим пакет декартовой точки, в котором представление точки это пара децствительных чисел, операции над которыми mkpoint, x-coord , y-coord выглядят так:

Пакет с представлением точки Real*Real и с реализаций операций над точками может быть опеределен следующим образом:

Также мы можем определить пакет полярных точек, чье представление такое же как и декартовой точки, но другое представление операций над точками:

Этипримеры иллюстрируют как пакеты реализуцбт абстракции данных путем сокрытия и представления данных и реаллизации операторов. Пакеты декартовых и полярных точек имеют один и тот же экзистенциональный тип Point, сипользуют один и тот же параметрический тип PointWRT[PointRep] для определения структуры операций над точками и имеют один и тот же тип для представления данных. Они только отдичаются содержпнием пакета, который определяет реализацию функции. В общем случае экзистенциональные типы влияют на то, чтоюы пакеты таких типов имели одинаковую структуру для операций. Но и типы для представления внутренних данных и реализация операций может отличаться для разных реализаций абстракнтных типов данных.

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

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

Сейчас мы вернемся к модулю Point и покажем как другие можули могут быть построены на его верхушкею. В частности мы посроем модули Circle и Rectangle на верхушке модуля Point и потом определим модуль Picture, котрроый использует и Circle и Rectagle. Люббые экземпляры Point могут быть основаны на произвольных представлениях данных, мы должны удостоверится, что круги и прямоугольники основаны на одинаковых представалениях Point, если мы хотим, чтобы они взаимодействовали.

Пакет круг предоставляет опрерации для создания круга из точки (центр) и действительного числа(радиус) и операции которые возвращают центр и радиус круга.

Операция diff(расстояние между центрами двух кругов ) также определена. Два параметра diff это круги основанные на одинаковых представлениях Point. Пакет круг также предоставляет пакет точка, чтобы позволять иметь доступ к операциям надд точками.

Мы теперь можем постоить некотрорый пакет круг, применив circleModule к различным пакетам точкам. Мы можем также определить различные версии circleModule основанные на различных представлениях круга и все это можно применить к различным пакетам точкам, чтобы получить пакеты круги. Здесь мы применяем circleModule к cartesianPointPackage и к polarPointPackage для получения пакетов декартовых и полярных точек.

Чтобы испльзовать пакеты точек мы долоны спвар их открыть. Мы должны открыть их два раза, чтобы(заметьте что тип Circle имеет двойную экзистенциональную квантификацию) для связывания PointRep и CircleRep с представлениями точки и круга используемых в пакете. Здесь мы используем сокрашщенную форму open, которая эквивалентна последовательным открытиям.

Прямоугольник опредделяется двумя точками, верхняя левая и правая нижняя. Определение можулля прямоугольника очень похоже на определение модуо\ля круга. В добавление к жтотму мы должны удостоверится, что две точки определяющие прямоугольник основаны на одинаковом представлении Point.

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

boundingRect, возвращающую наименьший прямоугольник содержащийся в данном круге.

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

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

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

Процесс линкования модулей может быть тоже выражен : мы делали это в предудущем примере, например мы произвели cartesianCirclePackage линкуя cartesianPointPackage и circleModule. Следовательно процесс построения систем из модулей можкт быть выражен на том же языке на котром и программирруются модули и вся мощь языка может быть применима вы процессе линковки.

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

6.Ограниченная квантификация.

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

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

Как вступление к включению на типах записей, мы сперва представим постейшую теорию включений на целых поддипозрнах типов. Пусть n..m определяют подтип типа Int

Соответствующий поддиапозонам от n до m включая конечные точки, где m и n это произвольные целыеСледующие отношения включения справедливы для целых поддиапозонов типов:

Поддиапозоны типов могут появится как орпеделение типов в λ-выражениях.

Константа 3 имеет тип 3..3 и также имеет тип любого супертипа включая тип x:2..5 выше.

Поэтому это правильный аргумент в f. Также следующее тоже должно быть правиьлно:

так как тип у это подтип области определения f. Фактический параметр функции может иметь любой подтип соответствующего формального параметра.

Рассмотрим функциональный тип 3..7 -> 7..9 .Также это модно посчитать функцией типа 4..6 –>6.10, так как она отображает целые между 3 и 7 (и следовательно между 4 и 6)

На целые между 7 и 9 (и следовыательно между 6 и 10).Заметьет, что домен сужается, когда как подомен расширяется. В общем случае мы можем сформулировать правила включения следующим образом:

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

Может быть означено f: h(f)

Из-за этих правил включения для поддиапозонов, стрелок и приложений.

То же рссуждение подходит и для типа запись. Предположим у нас есьт типы:

Мы хотим показать, что все мащины это транспорт например Car это подтип Vehicle. Для достижения этого нам потребуется следующее правило включения для типа запись.

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

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

Мы можем даже выразить множественное наследование. Если мы добавим определения типов:

тогда car это подтип типов vehicle и machine, а эти в свою очередь подтипы типа object. Наследование на записях также расширяется для более высоких функциональных типов, в случае поддиапозонов, правило включения для постранства функции тоже поддерживается.

В случае вариантных типов мы имеем следующее правило включения.

Например, любой яркий цвет это цвет :

и любая функцие работающей с цветами будет доступны и яркие цвета.

Более детальные детали этих типов наследования могут быть найдены в [84b].

6.2 Ограниченная универсальная квантификация и выделение подтипов.

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

Возмем простейшую функцию от записи с одним компонентом:

Который можетможет быть применен к записям {one=3,two=true}.Это можно сделать полиморфным:

Мы можемиспользовать f[t] на записях формы {one=y} для любого типа t , и на записях типа {one=y , two=true}.

Нотация all[a]e позволяет нам выражать правило, что переменная типа может принимаь любое значение типа, но не позволяет нам распознавать переменные типов, которые принадлжат подмножеству множества типов. Общее средство для определения переменных, которые определены на произвольных подмножествах типов может быть реализовано как квантификация над множествами типов определенных специальными предикатами. Но нам не нужна такая общность и мы можем удовлетворится определив конкретный класс множеств – множество всех подтипов данного вида. Это может быть сделано ограниченной квантификацией.

Переменная типа определенная на множестве всех подтипов типа Т может быть определена путем ограничения квантора квантора :

а определено на всех подтипах Т в области е.

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

Заметьте, что немного отличий между go и fo, все что мы сделали это наложили ограничения, что аргумент должен быть подтипом {one:Int} от параметра fun к параметру all. Сейчас мы миеем два способа выражения огрничений включения : неявно путем параметров функции и явно путем ограниченных кванторов. Теперь, так как у нас есть ограниченные кванторы, мы можем забыть другие механизмы, требующих строгого сопоставления типов при передачи параметра, но мы оставим его для удобства.

Чтобы ввыразить тип нам нужно ввести оганиченные кванторы в выражение типа:

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

где all[b]e теперь сокращение для Новая функция g не может быть выражена при помщи параметрического полиморфизма или отдельно наследованием. Только их комбинация, достигаемая при помощи огрниченных кванторов, позоляет нам это записать.

Однако, ограниченные кванторы не показали какой-то дополнительной силы, так как мы можем перефразировать как и g как f, дав нам включение типов при передаче параметров. Но ограниченные кванторы более выразительны, как показывают следующие примеры.

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

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

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

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

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

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