Следует отметить, что в TL-схеме подавляющего большинства API-запросов использование полиморфных типов ограничивается типом Vector. Тем не менее, полезно иметь в виду общую картину.
Рассмотрим, например, тип IntList, определенный следующим образом:
int_cons hd:int tl:IntList = IntList;
int_nil = IntList;Конструкторы int_cons и int_nil, а также сам тип IntList, являются выражениями следующих типов (запись A : X означает, что A является выражением типа X):
IntList : Type;int_cons : int; IntList; IntList; int_nil : IntList;Ключевое слово Type используется для обозначения типа всех типов. Заметим, что Type не есть Object (Object — это тип всех термов). Альтернативный синтаксис, который мог бы использоваться в каком-нибудь другом функциональном языке программирования (но не в TL):
NewType IntList :=
int_cons hd:int tl:IntList
int_nil
EndTypeВ TL поддерживается следующий вариант (фигурные скобки обозначают необязательные поля, см. далее):
cons {X:Type} hd:X tl:(List X) = List X;
nil {X:Type} = List XАльтернативная запись в других функциональных языках с зависимыми типами:
NewType List {X:Type} :=
| cons {X:Type} hd:X tl:(List X)
| nil {X:Type}<br>EndTypeВ любом случае эти варианты эквивалентны друг другу с точки зрения формальной теории типов и приводят к определению следующих термов:
List : Type ->; Type;
cons : forall (X:Type), X - List X - List X;
nil : forall (X:Type), X - List X;На всякий случай напомним, что запись “A - B” является сокращением для “forall (x : A), B” для любой переменной x, не входящей в A и в B. Например, тип cons мог бы быть записан следующим образом:
cons : forall (X:Type), forall (hd : X), forall (tl : List X), List Xили, более компактно:
cons : forall (X : Type) (hd : X) (tl : List X), List XСм. calculus of constructions. Примеры функциональных языков с зависимыми типами, поддерживающих подобными конструкции — coq, agda.
В этом случае запись через квантор всеобщности оказывается более содержательной, чем запись через стрелку, поскольку имя переменной, связываемой квантором, используется для передачи названия соответствующего поля в конструкторе, даже если эта переменная нигде не используется в части выражения под квантором. Со структурной точки зрения все эти записи типа cons эквивалентны.
Как мы видим, для сериализации значения типа List X, получающегося в результате применения комбинатора cons X:Type hd:X tl:(List X) = List X, нам нужно:
В первом пункте единственный вопрос — от какой именно строки следует вычислять crc32. Предлагается брать строку cons X:Type hd:X tl:List X = List X, без завершающей точки с запятой и без всех скобок (замкнутые выражения-типы однозначно восстанавливаются по префиксной записи их конструкции).
В последнем пункте мы рекурсивно решаем все ту же проблему сериализации значения типа List X; будем считать ее решенной по предположению индукции по построению сериализуемого значения. Третий пункт также будем считать понятным (индукция по построению типа сериализуемого значения).
Остается описать, каким образом передаются (сериализуются) типы, т.е. значения типа Type. На настоящий момент типы в TL-схемах появляются только как необязательные параметры конструкторов и потому никогда не сериализуются явно, а их значения выводятся из заранее известного типа сериализуемого значения.
Для полноты опишем, как можно было бы явно сериализовывать типы (значения типа Type), однако нужно помнить, что на практике это знание пока не пригодится. См. статью сериализация типов.
Выше было сказано, что у любого конструктора можно выделить любое подмножество (из первых нескольких) параметров как необязательные (заключив их объявления в фигурные скобки), на самом деле сейчас это не совсем так. Во-первых, эти необязательные параметры могут быть только типа Type либо # (натуральные числа). Во-вторых, необязательные параметры должны обязательно участвовать в типе результата, в противном случае не получится определить их значения.
Отметим, что @constr-id означает ‘полную форму’ конструктора (в которой все необязательные параметры становятся обязательными), а constr-id означает его сокращенную форму (без необязательных аргументов). Если необязательных аргументов нет, эти две формы совпадают. Сейчас полные формы конструкторов никогда не используются.
Есть небольшая проблема: если мы хотим сериализовать значение голого типа %pair string int или %pair string Y (который обычно обозначаетcя в TL просто как pair, хотя предпочтительнее форма %Pair), мы не можем одновременно использовать и полный конструктор @pair, и частичный pair, поскольку имя конструктора не будет сериализовано. Поэтому следует различать голые типы %@pair (сериализуется тип X, тип Y, значение x:X, значение y:Y) и %pair (сериализуются только x:X и y:Y, типы X и Y известны из контекста). На практике нам почти всегда нужен голый тип %pair, и это именно то, что обозначает pair в контексте типа в TL. Таким образом,
record name:string map:(List (pair int string)) = Record;будет сериализован примерно так, как хочется (сериализации элементов списка будут состоять из сериализации int‘а и сериализации string’а, без каких-либо дополнительных заголовков, типов, или имен комбинаторов). Кстати, при вычислении имени ‘record’ комбинатора record в приведенном выше примере будет вычисляться crc32 строки record name:string map:List pair int string = Record.
Отметим еще, что более точным описанием этого типа было бы
record name:string map:(List %(Pair int string)) = Record