учебники, программирование, основы, введение в,

 

Теория типов и комбинаторная логика

Рассмотрим построение системы типизации на основе комбинаторной логики.
В математике принято называть типами (или, иначе, сортами) относительно устойчивые и независимые совокупности элементов, которые можно выделить во всем рассматриваемом множестве (предметной области). Заметим, что разделение элементов предметной области на типы или сорта во многом является условным и носит субъективный характер, т.к. зависит от эксперта в этой области.
Тип, подобно множеству, может определяться двояко.
Во-первых, возможно определение типа посредством явного перечисления всех элементов, принадлежащих типу (заметим, что такой подход применяется и в математике, и в программировании, где существуют так называемые перечислимые типы).
Другим способом определения типа  T является формализация общих свойств тех элементов d из предметной области D, которые объединяются в этот тип, посредством задания индивидуализирующей предикатной функции Y, значение которой истинно, если элемент принадлежит данному типу и ложно в противном случае:
T = {d: D|Ψ}.
При более формальном подходе к теории типов и типизации в связи с исчислением ламбда-конверсий следует определить чистую систему типов.
Чистой системой типов называется семейство ламбда-исчислений, в которых каждый элемент характеризуется тройкой
<S, A, R>,
где:
S – подмножество констант, называемых сортами;
A – множество аксиом вида c:s, где с является константой, а s является сортом;
R – множество троек сортов, определяющих возможные функциональные пространства и их сорта для системы.
Далее введем обозначение, характеризующее то обстоятельство, что тот или иной объект является типизированным, или, иначе говоря, что тому или иному объекту приписан тип.
В частности, для ламбда-терма M  приписывание ему типа  T обозначим как
#M ||— T
и будем в таком случае говорить, что ламбда-терм M имеет тип  T.
При более общем подходе, который верен и для математики, и для программирования, система типов формируется следующим образом.
Во-первых, задается множество базисных типов (обозначим их символами d1 , d2 , и так далее).
Во-вторых, примем соглашение, что всякий базисный тип считается типом.
В-третьих, условимся, что если a и b считаются типами, то функция из a в b также считается типом и при этом имеет тип  a→b.
Заметим, что в основе теории типов лежит принцип иерархичности, который заключается в том, что производные типы содержат базисные как подмножества.
Этот принцип построения справедлив и для языков программирования. В частности, иерархии классов в объектно-ориентированных языках программирования формируются аналогично приведенному выше построению математической системы типов.
Для иллюстрации построения теории типов расширим комбинаторную логику операцией приписывания типа.
Напомним аксиомы комбинаторной логики, задающие свойства отношения конвертируемости:
(I) Ix = x;
(K) Kxy = x;
(S) Sxyz = xz(yz).
Аксиома (I) означает существование комбинатора (функции) тождества, т.е. наличие тождественного преобразования, при котором любой аргумент отображается сам в себя.
Аксиома (K) означает существование комбинатора (функции) взятия первой проекции, т.е. первого элемента упорядоченной пары или первого элемента списка. Интуитивно ясно, что эта аксиома близка языкам функционального программирования, оперирующим списками, и соответствует фундаментальной операции взятия головного (первого) элемента списка.
Оказывается, что комбинаторная логика обладает возможностью не только моделировать процесс реализации программного обеспечения на языке функционального программирования, но и прозрачно формализовать процедуру приписывания типов объектам этого языка.
Под типом (сортом) будем понимать относительно устойчивую и независимую совокупность элементов, которую можно выделить во всем рассматриваемом множестве (предметной области).


Сравним математическую теорию типов с подходом к типизации выражений, принятым в языке программирования SML.
Каждому выражению (константа, переменная, функция) языка SML поставлен в соответствие тот или иной тип. Такая система типизации в языках функционального программирования называется системой сильной типизации, а сам язык – языком с сильной типизацией.
Система типов в SML формируется по следующей схеме:
Во-первых, определяется множество базисных типов. В частности, в языке программирования SML выделяются следующие базисные типы:
  • int – целые числа;
  • string – строки символов;
  • bool – логические значения.

Во-вторых, принимается следующее соглашение для выводимости  производных типов: если a и b считаются типами, то функция из a в b имеет тип  a→b.
Как можно заметить, формирование системы типов в SML аналогично построению системы типов в формальных математических теориях, в частности в комбинаторной логике.
Язык функционального программирования SML представляет собой язык со статической типизацией. Это означает, что процедура контроля типизации, которая является неотъемлемой частью транслятора любого современного языка программирования, должна поставить тот или иной тип в соответствие каждому выражению в тексте программы. Таким образом, приписывание типов выражениям происходит во время компиляции (compile time), а не во время выполнения (run time) программы, т.е. статически с точки зрения выполнения программы.
Тот факт, что каждый объект программы должен быть типизирован до начала ее выполнения, не означает необходимости явного приписывания типа в ходе проектирования и реализации программы.
Важным преимуществом языка программирования SML, который, напомним, возник как инструментальное средство для доказательства теорем, т.е. построения цепочек логического вывода, является так называемое свойство выводимости типов (type inference). Это свойство означает, что тип некоторых выражений языка SML может быть выведен из контекста окружающих его выражений, типы которых уже известны, путем сопоставления (при этом учитываются объемлющие и внутренние функции, аппликация, присваивание и другие операции).
При этом выводимость допускает не строгое равенство типов параметров, а лишь их сводимость друг к другу. С математической точки зрения прослеживается аналогия с отношением конвертируемости.
В случае несоответствия типов сообщение об ошибке инициируется еще на стадии компиляции, что обеспечивает более упорядоченный и эффективный процесс проектирования и реализации программного обеспечения.
Как уже отмечалось, язык функционального программирования SML является языком со строгой типизацией, т.е., говоря математическим языком, каждому выражению языка должен быть приписан тип. При этом гарантируется корректная типизация языковых объектов, что выгодно отличает SML от таких языков программирования, как, скажем, классический вариант C, в котором допускаются потенциально небезопасные для среды выполнения программы преобразования типов.
Контроль соответствия типов в языке SML, в отличие от LISP и подобных ему языков программирования, в полном объеме осуществляется на этапе компиляции, что также способствует безопасности типизации.
Еще одной важной позитивной особенностью языка программирования SML является то обстоятельство, что в нем поддерживается так называемая полиморфная типизация, суть которой можно объяснить на основе следующего примера.
Рассмотрим функцию обработки списка, которая упорядочивает его элементы по возрастанию. В классическом языке программирования со строгой типизацией, например, в языке Pascal, неизбежно придется реализовать, по крайней мере, две функции: для случаев числовых и строковых элементов списка. В SML такой необходимости не возникает, т.к. существует возможность описания функции обработки списка с переменным типом аргументов, которая безошибочно обработает и список из чисел, и список из строк, существенно сэкономив трудозатраты.
Проиллюстрируем выводимость типов в языке программирования SML на примере.
Рассмотрим функцию
let
val Id = fn x => x
in (Id 3, Id true)
end    
С точки зрения анализатора корректности типизации эта функция является корректно типизированной (well-typed). Конструкция let, по сути, представляет собой подстановку одной функции в другую. В этой связи выводимость типов иначе называется let-полиморфизмом.
Рассмотрим другую функцию
fn Id => (Id 3, Id true)) (fn x => x)
В отличие от предыдущей, данная функция является некорректно типизированной (ill-typed), поскольку однозначно определить тип параметра x, в отличие от предыдущего примера, не представляется возможным.
Рассмотрев введение в математическую теорию типов и подходы к типизации в языках программирования, представим в концентрированном виде те преимущества, которые отличают языки программирования и формальные теории с типами.
Прежде всего, отметим то бесспорное преимущество типизированных исчислений, что при таком подходе моделируемая предметная область структурирована лучше, чем в том случае, если отсутствует сегментация на типы. Типизация структурирует предметную область по иерархическому принципу.
Введение типизации облегчает и упорядочивает не только восприятие, но и управление предметной областью. Манипулирование типизированными элементами носит более целенаправленный характер, причем появляется возможность обрабатывать разнородные сущности предметной области различным образом, а однородные (или, точнее, однотипные) – единообразно.
Перейдем к языкам программирования и практике проектирования и реализации программных систем. В случае построения языка программирования по принципу строгой типизации несоответствия типов фиксируются до начала этапа выполнения программы (на этапе контроля соответствия типов в ходе трансляции), что гарантирует отсутствие семантических (смысловых) и логических ошибок и безопасность программного кода.
Проиллюстрируем на примерах механизм работы процедуры, осуществляющей вывод типов в языке программирования SML. В качестве первого примера определим тип статической переменной x, которой присвоим значение, сводимое к целому типу:
val x=2*3;
val x = 6 : int
Как и следовало ожидать, значение переменной x оказывается целочисленным (int).
Заметим, что функция val, которая используется в примере, является стандартной функцией языка программирования SML для определения типа языкового объекта, т.е. фактически осуществляет приписывание типа (при необходимости используя механизм выводимости типов).
В качестве второго примера определим тип константы, которой присвоим значение, также сводимое к целому типу:
1+2;
3 : int
Как и следовало ожидать, значение константы 3 также оказывается целочисленным (int).
Наконец, определим тип функции сложения двух целочисленных аргументов:
fun add (x : int)(y : int) = x+y;
val add = fn : int -> int -> int
Как видно из результата, типом функции является функция из пары целочисленных значений в целочисленное значение (с точностью до скобок).
Продолжим ряд примеров. Проиллюстрируем означивание (вычисление значения) определенной выше функции сложения двух целочисленных аргументов:
add 1 3;
val it = 4 : int
Очевидно, что, как и следует из ранее вычисленного типа
(int -> int -> int), функция, принимая на вход пару целочисленных величин, возвращает значение целочисленного типа.
Рассмотрим далее тип функции, которая является производной от функции add и производит операцию прибавления единицы:
val f = add 1;
val f = fn : int -> int
Вновь введенная функция имеет тип «из целого числа в целое число» (int -> int) .
Наконец, означивание последней функции
f 4;   
val it = 5 : int
в соответствии с ее типом дает целочисленный результат.
Рассмотрим пример полиморфизма – оперирования функциями переменного типа.
Для иллюстрации исследуем поведение встроенной функции hd (от слова «head» – голова), которая выделяет «голову» (первый элемент) списка, вне зависимости от типа его элементов.
Применим функцию к списку из целочисленных элементов:
hd [1,2,3];
val it = 1 : int
Получим, что функция имеет тип функции из списка целочисленных величин в целое число (int list -> int).
В случае списка из значений истинности та же самая функция
hd [true, false, true, false];
val it = true: bool
возвращает значение истинности, т.е. имеет следующий тип:
bool list -> bool
Наконец, для случая списка кортежей из пар целых чисел
hd [(1,2)(3,4),(5,6)];
val it = (1,2) : int*int
получим тип:
((int*int)list -> (int*int)).
В итоге можно сделать вывод о том, что функция hd имеет тип  (type list) -> type, где type – произвольный тип, т.е. полиморфна.

Технологическая платформа .NET обеспечивает единообразное управление типами элементов всех языков программирования, реализованных на данной платформе. Это достигается за счет интегрированной обобщенной системы типизации, так называемой Common Type System, или, сокращенно, CTS.
Основная особенность CTS заключается в том, что она представляет собой единую иерархию типов, и типы объектов программы, написанной на произвольном языке программирования, который поддерживается технологической платформой .NET, в ходе трансляции автоматически преобразуются в соответствующие им типы  Common Type System.
Таким образом, для любого языка программирования существует отображение (функция), преобразующая произвольный тип этого языка в тот или иной тип  Common Type System. Естественно, язык программирования SML не является исключением. Приведем в подтверждение фрагмент отображения типов языка программирования SML в типы иерархии CTS, оформив это соответствие в виде.
Позднее мы обсудим подобное соответствие типов для языка программирования C#.
Рассмотрим более подробно обобщенную систему типизации, принятую в .NET.
Как явствует из схемы, Common Type System представляет собой иерархию, в которой стрелки указывают в сторону уменьшения общности типа.
Типы иерархии CTS подразделяются на ссылочные типы (pointer type) и типы-значения (value type).
Особенностями ссылочных типов являются необходимость использования указателей на типизированные объекты, а также централизованное хранение и освобождение памяти («сборка мусора»).
Одной из характеристик типов-значений является то обстоятельство, что они не участвуют в наследовании. Кроме того, типы-значения копируются при присваивании значения.
В свою очередь, ссылочные типы могут принимать одну из трех форм:

  1. объектные типы (object type);
  2. интерфейсные типы (interface type);
  3. типы указателей (pointer type).

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


Таблица 6.1. Отображение типов языка программирования SML в типы иерархии CTS

Тип

Класс.NET

1

int

System.Int32

Целое число

2

string

System.String

Строка

3

bool

System.Boolean

Логическое значение

...

...

...

...

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

 

 
На главную | Содержание | < Назад....Вперёд >
С вопросами и предложениями можно обращаться по nicivas@bk.ru. 2013 г.Яндекс.Метрика