type RecJWRT2[RectRep,PointRep] = {pointPackage: PointWRT[PointRep], mkrect: [PointRep у PointRep) RectRep, top If:: RectRep -» PointRep, botrht: RectRep PointRep

}

type RectWRTI [PointRep] =

3RectRep. RectWRT2[RectRep,PointRep]

type Rect = 3PointRep. RectWRTI [PointRep]

type RectModule =

VPointRep. PointWRT[PointRep] RectWRTI [PointRep;

value rectModule = all [Point Rep]

fun (p: PointWRT[PointRep])

pack[PointRep = PointRep in RectWRT1 [PointRep]] {pointPackage = p,

mknect = fun (tl: PointRep, br: PointRep) (tl.br), toplft = fun {r: PointRep v PointRep) fst(r), botrht = fun (r: PointRep у PointRep) snd{r)

}

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

type FiguresWRT3[RectRep, Circle Rep, Point Rep] = {c ire le P а с к age: CircleWRT[C ircle Rep, P oi ntR e p; re ct Рас к a ge: RectW RT[Rect Rep, Poin tRep] bounding Rect: CircleRep -» RectRep

}

type FiguresWRT1 [PointRep] =

3RectRep. 3CircleRep. FigureWRT3[RectRep,CircleRep,PointRep]

type Figures = 3PointRep FigureWRTI [PointRep]

type Figures =

VPointRep. PointWRT[PointRep] -> FiguresWRTI[PointRep]

value figuresModule = all [Point Rep]

fun (p: PointWRT[PointRep])

pack[PointRep = PointRep in FiguresWRTI [PointRep]] open circleModule[PointRep](p) as с [CircleRep] i n open rectModu I e [Poin tRep] (p} as г [Re ct Rep] in {circlePackage = c. rectPackage = r, boundingRect =

funic: CircleRep) ..r.mkrect{..c.center(c)..)..

)

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

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

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

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

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

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

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

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

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

П..РЛ £ n..m iff n£n and m£m"

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

value f = fun (х: 2..5) х + 1 f: 2 .5 ->3 .6

f(3)

Константа 3 имеет тип 3..3 и также имеет тип любого супертипа включая тип x:2..5 выше. Поэтому это правильный аргумент в f. Также следующее тоже должно быть правиьлно:

value д = fun {у: 3..4) f<y)

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

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

s -»t £ s -j Г iff s£S and t£t

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

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

Из-за этих правил включения для поддиапозонов , стрелок и приложений. То же рссуждение подходит и для типа запись.Предположим у нас есьт типы:

type Саг = {agelnt, speed Int, fuel:String} type Vehicle = {age:Int, speed:Int}

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

<al:tl- -- -anV - -агл:,гг, ) {а,:,.. ,an:un} iff tj £ Uj for i e 1..n.

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

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

type Object = {age:Int}

type Machine = {age:Int, fuel:String}

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

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

[a,:!,, .. ,an:tn] s ub .. ,an:un,.. ,am:uj iff t < Uj for i e 1..П.

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

type brightColor = [red:Unit, green:Unit, blue:Unit]

type color = [ned:Unit, green:Unit, blue:Unit, gray:Unit, browrvUnit]

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