Дисциплина типов и важнейшие концепции гетерогенной среды вычислений

Теория типов и типизация в .NET

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

Прежде всего, мы сформулируем интуитивное и более строгое определения типа. Затем будет представлена классификация систем типизации при различных подходах к программированию с указанием места изучаемых в книге языков и подходов. Далее будут подробно исследованы особенности системы типизации Common Type System в среде Microsoft .NET. Особое внимание уделено реализации механизмов организации и управления типами, а именно преобразованиям типов и пространствам имен.

Иерархия типов Microsoft .NET проиллюстрирована примерами описаний типов данных для случаев типов-значений и ссылочных типов.

Напомним ход эволюции теорий, лежащих в основе современного подхода к типизации и теории типов.

В 1960;х гг. Р. Хиндли (Roger Hindley) исследовал типизацию в комбинаторной логике. При этом основной проблемой, стоящей перед исследователем, было моделирование языков функционального программирования со строгой типизацией, к каковым, в частности, относятся изучаемые нами языки F# и С#. В конце 1960;х гг. тот же ученый исследовал полиморфные системы типов, т. е. такие системы типов, в которых возможны параметризованные функции или функции, имеющие переменный тип. В 1970;х гг. Р. Милнер предложил практическую реализацию расширенной системы полиморфной типизации для языка функционального программирования ML, давшего начало языку программирования F#.

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

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

Тип, подобно множеству, может определяться двояко. Во-первых, возможно определение типа посредством явного перечисления всех принадлежащих ему элементов (заметим, что такой подход применяется и в математике, и в программировании, где существуют так называемые перечислимые типы). Другим способом определения типа Т является формализация общих свойств тех элементов d из предметной области D, которые объединяются в этот тип, посредством задания индивидуализирующей предикатной функции 4^х, значение которой истинно, если элемент принадлежит данному типу, и ложно в противном случае:

T={d: D^}.

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

.

где S — подмножество констант, называемых сортами; А — множество аксиом вида c: s, здесь с является константой, as — сортом; R — множество троек сортов, определяющих возможные функциональные пространства и их сорта для системы.

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

#М |- Т и будем в таком случае говорить, что лямбда-терм М имеет тип Т.

При более общем подходе (который верен и для математики, и для программирования) система типов формируется следующим образом. Во-первых, задается множество базисных типов (обозначим их символами d_{, d₂ и т. д.). Во-вторых, примем соглашение, что всякий базисный тип считается типом. Наконец, условимся, что если, а и Ь считаются типами, то функция из, а в Ь также считается типом и при этом имеет тип а—>Ь.

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

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

Введение

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

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

Напомним классификацию систем типизации в языках программирования.

Исторически наиболее распространенной для языков программирования является строгая типизация. При таком формировании системы типов в языке в любой момент существования любого языкового объекта существует однозначное соответствие между объектом и его типом. Другими словами, можно запрограммировать функцию, определяющую тип объекта, подобную ранее рассмотренной нами функции typeof языка программирования С#. Строго типизированными являются классические императивные языки программирования Pascal, FORTRAN, PL/1 и др. Отметим, что классический вариант языка программирования С не является строго типизированным.

Сильная типизация необходима для обеспечения корректности связывания переменных со значениями до выполнения программы. Таким образом, каждое выражение языка программирования с сильной типизацией при успешном завершении анализа корректности типизации является корректно типизированным. Примером языка программирования с сильной типизацией может служить F#. Использование механизма выводимости типов гарантирует сильную типизацию даже при отсутствии строгости. Язык программирования, не имеющий сильной системы типизации, может быть назван языком со слабой типизацией.

Еще одним важным видом систем типизации языков программирования является полиморфная типизация. При таком подходе допустимы выражения переменного типа (скажем, функция упорядочения списка с неопределенным типом элементов). Процедура контроля соответствия типов (type-checking) может быть реализована как во время компиляции (compile time), т. е. более безопасным образом, гак и во время выполнения (run time) программы, что потенциально менее безопасно для программного кода.

Исследуем особенности управления типами в системе типизации Common Type System технологии Microsoft .NET. Из соображений безопасности программного кода Microsoft .NET типы Common Type System, так же, как объекты и классы, могут использоваться после инициализации. При этом необходимо учитывать особенности вызывающего метода, а также определенных методов доступа get и изменения set.

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

Иерархия типов в соотнесении с Microsoft .NET может быть представлена в форме той или иной совокупности (в частности, в виде пространства имен, файла или сборки).

Как уже отмечалось, наиболее крупными и важными подкатегориями иерархической системы типизации в Microsoft .NET являются ссылочные типы (reference type) и типы-значения (value type). Рассмотрим более подробно особенности реализации ссылочных типов и типов-значений в языке программирования C# (рис. 3.1). Прежде всего, типы-значения, в отличие от ссылочных типов, содержат непосредственно объекты данных. Кроме того, типы-значения не могут быть пустыми (т.е. принимать значение null). Ссылочные типы, в противоположность типам-значениям, содержат не сами объекты, а лишь ссылки на них, и могут принимать значение null.

Рис. 3.1. Сопоставление ссылочных типов и типов-значений.

В качестве иллюстрации особенностей реализации ссылочных типов и типов-значений в языке программирования C# рассмотрим следующий фрагмент программы на языке С#:

int i=25;

string s="John_Smith" ;

В первой строке программы происходит означивание целочисленной константы (т.е. типа-значения), а во второй — строковой (т.е. типа-ссылки). В результате при выполнении первой строки программы происходит связывание со значением в памяти, а во втором — со ссылкой, т. е. указателем на область памяти.

Проиллюстрируем иерархию системы типов Common Type System программной среды Microsoft .NET примерами из языка программирования С#, конкретизирующими подтипы для типов-значений и ссылочных типов. При этом типы-значения распадаются на следующие подтипы:

• элементарные (в частности, целочисленные и вещественные) —.

int i; float х;

• • перечислимые (в частности, моделирующие переключатели) — enum State { Off, On };
• • структурные (в частности, моделирующие точки на плоскости) — struct Point (int х, у;};.

В свою очередь, ссылочные типы подразделяются на следующие подтипы:

• корневой подтип (указатели на произвольные объекты в иерархии типов в Common Type System) —.

object;

• • строковые (указатели на строки символов) — string;
• • классы (указатели на объекты типа class) — class Foo: Bar, IFoo {…};
• • интерфейсы (указатели на объекты типа interface) — interface IFoo: IBar {…};
• • массивы (в частности, указатели на строки из 10 символов) — string!) a=new string! 10];
• • делегаты (усовершенствованные указатели на функцию) — delegate void Empty ();

Ранее обсуждались механизмы boxing и unboxing, реализованные в различных средах разработки программного обеспечения Microsoft .NET. Напомним, что эти механизмы используются для преобразования типов выражений языков программирования из ссылочных в типы-значения и обратно.

Схема на рис. 3.2 иллюстрирует перечень классов Common Type System среды проектирования и реализации программного обеспечения Microsoft .NET применительно к языку программирования С#. В частности, все многообразие типов можно разделить на предопределенные (заранее заданные системой программирования) и определенные пользователем (user defined). К последним относятся перечисления, массивы, классы, интерфейсы и делегаты (указатели на функцию).

Предопределенные типы делятся на ссылочные типы (объекты и символьные строки) и типы-значения (встроенные — короткие и длинные целые со знаком и без знака, а также числа с плавающей точкой — с одинарной и двойной точностью).

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

Рис. 3.2. Иерархия типов языка С# (фрагмент).

Неявные преобразования инициируются Common Type System и производятся автоматически. При этом результат неявного преобразования всегда успешен и не приводит к потере точности. Явные преобразования инициируются программистом или пользователем приложения, а следовательно, требуют явного вызова и при этом могут завершаться ошибкой, а также приводить к потере точности.

Приведем ряд примеров преобразований типов на языке программирования С#:

int х=25; long у=х;

// неявное short z=(short)x;

// явное.

double d =3.141 592 536; float f=(float)d;

// явное long l=(long)d;

// явное Заметим, что система Common Type System среды Microsoft .NET обеспечивает безопасную типизацию, т. е. гарантирует отсутствие побочных эффектов (переполнение оперативной памяти компьютера, некорректное преобразование типов и т. д.). Заметим также, что как явные, так и неявные преобразования типов могут инициироваться пользователем.

Как показали исследования системы типизации Common Type System среды проектирования и реализации программных систем Microsoft .NET, эта иерархия имеет внушительный объем.

С целью повышения эффективности организации описания типов и манипулирования ими в программном обеспечении, работающем иод управлением среды Microsoft .NET, вводится понятие пространства имен (namespace). Пространством имен будем называть механизм среды Microsoft .NET, предназначенный для идентификации типов объектов языков программирования и среды реализации. Значение механизма пространств имен состоит в том, что появляется возможность логической структуризации системы типизации Common Type System в среде разработки приложений Microsoft .NET.

Описания пространств имен, но аналогии с описаниями типов данных размещаются в файлах.

Перечислим основные свойства, которыми характеризуются пространства имен в среде Microsoft .NET:

• 1) пространства имен могут объединять различные сборки;
• 2) пространства имен могут быть вложенными друг в друга;
• 3) между пространствами имен и файлами не существует однозначного соответствия (т.е. отображения, переводящего название пространства имен в имя файла);
• 4) полное имя типа должно содержать все необходимые пространства имен.

Для иллюстрации применения механизма пространств имен в среде программирования Microsoft .NET приведем развернутый пример описания пространств имен на языке программирования С#:

namespace Nl{.

//N1.

class Cl{.

// N1. C1 class C2{.

// N1. C1.C2.

} }.

namespace N2{.

//N1.N2 class C2{.

// N1. N2.C2.

} } }.

Рассмотренный пример содержит описания пространств двух имен: пространства N1 с описанием классов С1 и С2 и пространства N2 с описанием класса С2.

Заметим, что в комментариях к каждой строке программы на языке C# приведены полные наименования пространств имен. Так, для обращения к классу С2, описанному в пространстве имен N1, нужно использовать полное имя N1. C1.C2, а для обращения к классу С2, описанному в пространстве имен N2, — полное имя N1. N2.C2. Таким образом, при адекватном употреблении полных квалификационных наименований пространств имен удается избежать коллизии обозначений типов.

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

Для экономии трудозатрат и во избежание коллизий обозначений при разработке крупных программных систем в языке программирования C# предусмотрен оператор using. Чтобы проиллюстрировать применение механизма ликвидации коллизии обозначений типов в пространствах имен среды программирования Microsoft .NET посредством оператора using, приведем развернутый пример на языке программирования С#:

using N1;

Cl а;

// Имя N1. является неявным.

N1.C1 Ь;

// Полное имя.

C2 с;

// Ошибка: имя С2 нс определено.

N1.N2.C2 cl;

// Один из (под)классов С2.

С1.С2 е;

// Еще один из (под)классов С2.

using C1=N1.N2.C1;

using N2=N1.N2;

Cl a;

// Соответствует имени N1. N2.C1 N2. C1 Ь;

// Соответствует имени N1. N2.C1.

Заметим, что оператор using позволяет использовать типы как с указанием полного имени, так и без него, а также для указания альтернативных имен (alias).

Еще одним аспектом проектирования и реализации крупных программных комплексов под управлением среды Microsoft .NET является потенциальная коллизия имен типов в рамках масштабных проектов. Для решения этой проблемы в среде разработки программного обеспечения Microsoft Visual Studio для каждого из проектов могут быть указаны так называемые ссылки, каждая из которых идентифицирует уникальную сборку — самодостаточную единицу для компиляции и выполнения в рамках программного проекта.

Ссылки передаются компилятору в ходе трансляции программы на том или ином языке программирования под управлением среды Microsoft .NET по ссылке (при этом используется опция /г или /reference). Скажем, команда на компиляцию файла HelloWorld с исходным текстом программы на языке C# со ссылкой на пространство имен System.WinForms.dll будет иметь вид.

esc HelloWorld. es /reference:Systern.WinForms.dll.

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

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

После рассмотрения основных аспектов теории типов и типизации в языках программирования можно сделать следующие выводы. Во-первых, теории с тинами и языки программирования с типизацией имеют значительно более высокую вычислительную мощность, а следовательно, более высокую теоретическую и прикладную значимость. Во-вторых, технологическая платформа .NET обеспечивает ряд несомненных дополнительных преимуществ перед другими известными платформами в отношении системы типов. В частности, технология .NET использует централизованную, унифицированную, интегрированную систему типизации Common Type System (CTS), общую для всех языков программирования, реализуемых на данной платформе. Кроме того, в рамках технологической платформы .NET обеспечивается строгое, однозначное соответствие между примитивными типами языков программирования и базовыми классами .NET. Большинство компиляторов для языков программирования, которые реализованы для платформы .NET, имеют встроенную поддержку примитивных типов.

Целям безопасности типизации служит явное разделение на ссылочные типы и типы-значения, а также гибкий и надежный механизм преобразования типов-значений в ссылочные (известный также под названием boxing) и обратно (известный также под названием unboxing).

Контрольные вопросы

Вопрос 1.

Вариант 1: в чем состоит основное назначение типизации?

• а) структуризация предметной области (+);
• б) единообразие манипулирования объектами (+);
• в) упрощение процесса компиляции.

Вариант 2: какой из перечисленных языков программирования является бестиповым?

• а) LISP (+);
• б) С#;
• в) C++.

Вариант 3: каковы основные компоненты чистой системы типов?

• а) сорта, аксиомы, функциональные пространства (+);
• б) алфавит, сорта, аксиомы;
• в) сорта, аксиомы, правила вывода.

Вопрос 2.

Вариант 1: что является преимуществом типизации Microsoft .NET?

• а) унификация (+);
• б) однозначное отображение типов языков программирования во внутренние типы системы (+);
• в) большое количество типов.

Вариант 2: что понимается под типом?

• а) совокупность элементов предметной области (+);
• б) название предметной области;
• в) модель предметной области.

Вариант 3: что отличает теорию типов от прочих теорий?

• а) принцип индукции;
• б) принцип полноты;
• в) принцип иерархичности (+).

Вопрос 3.

Вариант 1: что из перечисленного является этапом развития теории типов?

• а) полиморфизм (+);
• б) теория простых функций;
• в) теория вычислений.

Вариант 2: каковы основные способы задания типа?

• а) явное перечисление элементов (+);
• б) индивидуализирующая функция (+);
• в) приписывание типа.

Вариант 3: каким образом осуществляется построение типов?

• а) посредством рекурсии;
• б) посредством дедукции;
• в) посредством индукции (+).