Ремонт принтеров, сканнеров, факсов и остальной офисной техники


назад Оглавление вперед




[6]

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

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

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

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

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

Так как типы это множества ,подтипы просто соответствуют подмножествам.Более того семантическое свойтсво Т1 это подтип Т2 соответствует математическому условию Tl qT2 в структуре типов. Это дает очент простую интерпретацию поддиапозона типов и наследования , как мы увидим в последующих секциях.

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

Структура типов содержит много особенностей ,которые могут быть названы в любом типипзированнном языке. В действительности они включаэт бесчисленное множество особенностей ,так как они включают каждое подмножство целых.Цель языка типов это дать программисту возможность именовать эти типы ,которрые соостветствуют разным степеням поведения.Чтобы сделать это языки содержат конструкторы типов ,включая функции-констукторы типов(например тип T1 -> T2) Для составления функционального типа Т из типов Т1 и Т2.Эти конструкторы позволяют бесчисленое множество интеренсых типов для конструирования из конечного множество примитивных типов. Однако могут быть интересными и типы ,которые не могут быть используя эти конструкторы.

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


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

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

Идея типов в качестве параметров полно разработана в Х-исчислении второго порядка. Денотационная модель Х-исчисления второго порядка это модель ретрактов. Здест типы не множества объектов ,а специальные функции (называемые ретракты);это может быть интерпретировано как определение множеств объектов. Так как своство этих типов это объекты ,модель ретрактов может еще лучше описывать явные пипизированные параметры, тогда как идеалы могут описывать лучше ниявные типипзированные параметры.

4.Универсальная квантификация.

4.1.Универсальная квантификация и шаблоннные функции.

Типизированного Х-исчисления достаточно ,чтобы выражать мономорфные функции. Однако это надекуватная модель для полиморных функций.Например ,требуется ,чтобы функция twice необязательно была ограничена типом из целых в целые ,может мы хотим определить эту функцию как полиморфно а ->а для произвольных типов а. Фнукция идентификации может похоже быть огпределена только для конкретных типов ,таких как integer:fun(x:Int)x.Мы не можем зафиксировать тот факт ,что её форма не зависит ни от какого типа.Мы не можем выразить идею ,что функциональная форма будет одинаковой для множества типов и мы должны явно связвать переменные и значения определенного типа во время , когдатакое связование может быть преждевременным.

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

value id = all [a] fun(x:a) х

В этом определении id , а это переменная типа ,а all[a] предоставляет абстаркцию для а ,чтобы id была функцией для всех типов.Чтобы применить функцтию идентификации к аргументу определенного типа,мы должны сперва представить тип как параметр и затем аргумент данного типа


(Мы использовали условие ,что параметр типа заключен в квадратные скобки ,а аргумент - в круглые)

Мы будем определять функции такие как id ,которые требуют параметр тип прежде чем они могут быть применены как шаблонные функции.И это шаблонная функеция идентификации.

Заметьте ,что all это опрератор связывания ,такой же как fun и требует сопоставления фактического параметра при применении функции.Однако all[a] служит ,чтобы связывать тип ,когда как fun(x:a) служит для связывания переменной данного типа.

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

value id = fun(x:a) х id<3)

Вот алгоритм проверки типов имеет задачей опознать ,что а это свободная переменная типа и переопределить первоначальную информацию all[a] и [Ъп"].Это часть того ,что может делать полиморфные проверяльщик типов ,похожий на тот ,который используется в ML. В действительности ML идет дальше и позволяет программистам опускать даже оставшуюся информацию о типах.

value id = fun(x) и id{3)

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

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

tyoe Genericid = Va. а а id: Genericid

Ниже пример функции ,которая принимает параметр произвольного типа.

Функция inst берет в качестве аргумента функцию указанную выше и возвращает два

вида её , Integer и Boolean.

value inst = fun(f: Va. a -» a) (f[lnt],fIBool]) value intid = fst(inst(id)): nt- In:

value boolid = snd(inst{id)): Bool -v Bool

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



[стр.Начало] [стр.1] [стр.2] [стр.3] [стр.4] [стр.5] [стр.6] [стр.7] [стр.8] [стр.9] [стр.10] [стр.11] [стр.12] [стр.13]