Type ::= ... QuanfifiedType QuantifiedType ::=

VA. TypeUniversal Quantification

ЗА. Type IExtendi! Quantise aioa

VAcType. Type ЗАсТуре. TypeBounded Quantification

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

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

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

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

Секция 7 кратко обозревает проверку типов и наследование типов для Fun.Она дополнено приложением перечисляющее все правила вывода.

Секция 8 иерархическую классификацию объектно-ориентированной системы типовш! предоставляет более общую систему типов в этой

классификации. Отношение Fun к менее общим системам соостветствующих ML , Galileo , Amber и систем типов других языков.

Надеемся ,что читателем будет интересно читать о Fun , так же интересно как авторам писать об этом.

2.1 Нетипизированное -исчисление

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

e::=xпеременная это Х-выражение

e::=fun(x)e абстракция e e::=e(e) аппликация е к е

Функции идентификации и функция successor могут быть поределены в Х-исчислении следующим образом.Мы используем ключевое слово value ,чтобы определить новое имя и связать его со значением или функцией.

Value id = fun(x)xфункция индентификации

Value succ = fun(x)x + 1 функция successor для integer.

Функция идентификации может быть применена к любому Х-выражению и возвращает всегда Х-выражение.Чтобы определить сложение над целыми в чистом Х-исчислении мы используем представление и определим сложение таким образом ,чтобы результате сложения получалось Х-выражение ,представляющее. Функция successor может применима только к Х-выражениям ,которые представляют целые числа. Инфиксная нотация х+1 это упрощение функциональной нотации +(х)(1).Здесь символы 1 и + ,должны рассматриваться как сокращения выражений для них из чистого Х-исчисления.

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

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

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

value twice = fun(f)fun(y)f(f(y)) - функция twice

Применяя функцию twice к функции successor можно получит функцию ,которая будет счистать successor от successor.

twice(succ) -> fun(y) succ(succ(y)) twice(fun(x)x+1) -> fun(fun(x)x+1)((fun(x)x+1)(y))

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

Типизированное Х-исчисление это Х-исчисление кроме того ,что каждая переменная должна иметь явный тип ,когда она вводится как связная переменная.Поэтому функция successor в типизированном Х-исчислении имеет следующую форму.

value succ = fun (x:int) x+1

Функция twice из целых в целые имеет параметр f ,чей тип int->int и может быть записана следующим образом.

Value twice = fun(f:int->int) fun (y:int)f(f(y))

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

Value succ= fun(x:int) (returns int)x +1

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

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

type IntPair=Int*Int type IntFun=Int*Int

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

Тот факт ,что значение v имеет тип Т пишется так v:T.

(3;4):IntPair Succ:IntFun

Нам нужно ввести переменные путем объявления типов в форме vat:T ,так как тип переменной может быть установлен по стрктуре присвоенной переменной.Например , тот факти ,что IntPair имеет тип IntPair может быть установлено тем фактом ,что (3,4) имеют тип Int*Int ,который был объявлен как эквивалентный к Int.

value intPair = (3,4)

Однако ,если мы хотим показать тип переменной как чатсь инициализации ,то мы можем сделать это при помощи нотации value var:T = value.

value IntPair:IntPair = (3,4)

value succ:Int -> Int = fun(x:Int) x + 1