Определение типов

Определение 7.1. Типом (сортом) называют относительно устойчивую и независимую совокупность элементов, которую можно выделить во всем рассматриваемом множестве (предметной области).

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

Тип, подобно множеству, может определяться двумя способами.

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

2. Определение типа T путем формализации общих свойств тех элементов d из предметной области D, которые объединяются в этот тип, посредством задания индивидуализирующей предикатной функции Ψ, значение которой истинно, если элемент принадлежит данному типу и ложно в противном случае:

T = {d: D|Ψ}.

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

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

<S, A, R>,

где:

S - подмножество констант, называемых сортами;

A - множество аксиом вида c:s, где с является константой, а s является сортом;

R - множество троек сортов, определяющих возможные функциональные пространства и их сорта для системы.

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

В частности, для ламбда-терма M приписывание ему типа T обозначим как

#M ||- T

и будем в таком случае говорить, что ламбда-терм M имеет тип T.

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

1. Задается множество базисных типов (обозначим их символами d₁, d₂, и так далее).

2. Примем соглашение, что всякий базисный тип считается типом.

3. Условимся, что если a и b считаются типами, то функция из a в b также считается типом и при этом имеет тип a→b.

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

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

Дата добавления: 2014-01-07