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

1) Расскажите своими словами о понятии «тип всех типов данных».

2) Какой прием применяется при определении типа данных при наличии понятия «тип всех типов данных»?

4.9. Родовые типы данных

Согласно определению конкретного типа данных, приведенному в разделе 1.5, операция конструирования типа данных в самой развитой форме должна содержать четыре аргумента: внешность, абстрактное описание, конкретное описание и описание связи. Первые два из них составляют спецификацию типа (приращение теории или сигнатуры системы типов в простейшем случае), а последние два – реализацию типа (приращение алгебры системы типов). Для дальнейших рассуждений операцию конструирования типов будем изображать в сокращенном виде с двумя аргументами – спецификацией и реализацией; саму операцию обозначим служебным словом модуль¹, за которым в квадратных скобках следует первый аргумент (спецификация типа) и затем в скобках начало  конец - второй аргумент:

модуль [ спецификация типа ] начало реализация типа конец.

Список операций в спецификации типа представляется в виде r₁ : T₁, r₂ : T₂, … , r_n : T_n, где r_i – имя, а T_i – тип (индекс) i –й операции.

Каждый из типов (индексов) операций T_i содержит обозначение конструируемого типа как типа одного или нескольких аргументов и/или типа результата. Ранее конструируемый тип в типах операций обозначался конкретным именем. Со сконструированным типовым объектом мы можем в принципе связать любое внешнее имя (например, мы можем описать типовою переменную и затем присваивать ей различные типовые значения). С другой стороны, во многих языках программирования существует прием, когда создаваемый тип данных никак не именуется. Поэтому требуется способ обозначения конструируемого типа внутри себя. Будем использовать для этой цели символ «*» (звездочка) и считать, что в каждом типе звездочка в его спецификации и реализации означает «я сам».

В соответствии с этими замечаниями конструкция определения абстрактного типа nat приобретает вид

тип nat = модуль [ операции zero :  *;

succ : *  *;

,  : * , *  bool

аксиомы  m, n : *

zero  n = true;

succ(m)  zero = false;

succ(m)  zero = true;

succ(m)  succ(n) = m  n;

m  n = and(m  n, n  m)]

начало реализация типа конец.

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

T_r = функция () тип ; модуль [  ] начало реализация типа конец,

где  = { p₁ : T₁, p₂ : T₂, … , p_n : T_n, } – спецификация параметров функции,  - спецификация операций типа.

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

T_r = модуль () [  ] начало реализация типа конец.

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

Tk = Tr (q₁, q₂, …, q_n).

В том случае, когда в  не зафиксировано значение ни одного формального параметра, тип, представленный конструктором T_r, называется исходным родовым типом, объединяющим некоторое максимальное множество типов данных со сходным поведением. Обращение к конструктору с фиксацией части параметров приводит к образованию конструктора редуцированного типа, представляющего частный родовой тип, являющийся потомком исходного множества типов данных (т.е. область значений этой функции является подмножеством исходной области значений). Фиксация всех параметров приводит к выработке конкретного типа данных с операциями из семейства T_r.

В качестве примера рассмотрим спецификацию родового типа множества:

тип set = модуль ( elem : тип

 операции  : * , *  bool

аксиомы  x, y, z : *

x  x = true;

x  y = y  x;

and((x  y), (y  z)) = (x  z) )

[ операции empty :  * ;

insert : * , elem  * ;

has : * , elem  bool};

аксиомы  s : *,  x, y : elem,

has(empty, x) =false;

has(insert(s, x), y) = or(x  y, has(s, y))]

начало реализация типа nat конец.

Заметим, что символ «*» в спецификации elem (в круглых скобках) обозначает тип этого elem, а в спецификации (в квадратных скобках) и в реализации (в скобках начало … конец) определяемого типа обозначает определяемый тип.

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

подтип setofnat = set(nat)

порождает тип с множеством операций

empty :  setofnat ;

insert : setofnat , nat  setofnat ;

has : setofnat , nat  bool;

а конкретизация

подтип setofinteger = set(integer)

порождает тип с множеством операций

empty :  setofinteger ;

insert : setofinteger , integer  setofinteger ;

has : setofinteger , integer  bool.

Механизм непосредственного построения конкретных типов данных обеспечивает пошаговое расширение алгебры системы типов. Механизм родовых типов позволяет осуществить обобщение этого процесса в тех случаях, когда необходимо построить ряд «родственных» типов данных. Естественно, что каждый конкретный тип из семейства родового типа мог бы быть построен непосредственным образом.