функции ,например функция вычисления длины списка передается в качестве параметра и используется на списках разного типа.Чтобы показать некоторую свободу ,которую мы имеем при определении полиморных функций ,мы напишем две версии twice ,которые различаются в способе передачи параметров.Первая версия twice1 имеет функциональный параметр f универсального типа. Определение

fun(f: Va. а -> a) bodv-of-ftmction

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

value twicel = all[t] fun(f. Va. a -> a) fun(x: t) f[t](flt](x)) Таким образом twice1 имеет три связанные переменные ,для которых фактичсекие параметры должны быть предоставлены во время означивания функции.

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

furiff: Va. a -> a} - требует функцию типа va. a ->a f(x:t) - требует аргумента подставляемого вместо типа t.

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

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

Va". a -»a.

правильным так как succ не имеет тип

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

value twice2 = all[t] fun(f: t -> t) fun(x: t) f<f<x»

twice2[Int]yield? run(f: Int -> lnt)fun(x: Int) Щх))

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

twice2[lnt](succ) twice2[lnt]:>ucc)(3)

yield? run(x: Int) succ(succ(x)) yield? 5

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

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

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

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

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

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

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

type BoolPair = Bool * Bool type IntPair = Int * Int

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

type Pair[TJ = T -*T

tyoe PairGfGool = Pair[Bool]

type PairOflnt = Pair[lnt]

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

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

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

type А[Т] = Т -> Т type В = VT. Т Т

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

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

гес type List[ltem] = [nil: Unit

cons: head: Hem, tail: List[ltem]}

]

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

value nil = all Item, [nil = ()] value intNil = nil[lnt] value hoolMil = nil[Bool]

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

nil: Vltem. List[Item] intNil: List[lnt] IjooINN : List[Bool]

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

value cons : Vltem. (Item x List[ltem]) -* List[ltem] = all Item.

fun (h: Item, t: List[ltem]>

[cons = {head = h, tail = t}]

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

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

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

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

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

(3,4): За. ax a (3,4): За. a

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

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