Previous Up Next

Chapter 23  Универсальные типы

В предыдущей главе мы рассмотрели простую разновидность полиморфизма через let, имеющегося в ML. В этой главе мы изучаем более общую форму полиморфизма в рамках мощного исчисления, известного как Система F (System F).1

23.1  Мотивация

Как мы упомянули в §22.7, в простом типизированном лямбда-исчислении можно написать бесконечное число <<удваивающих>> функций:

doubleNat = λf:Nat -> Nat. λx:Nat. f (f x); doubleRcd = λf:{l:Bool} -> {l:Bool}. λx:{l:Bool}. f (f x); doubleFun = λf:(Nat -> Nat) -> (Nat -> Nat). λx:Nat -> Nat. f (f x);

Каждая из этих функций применима к своему типу аргумента, но их поведение одинаково (более того, текст функций, помимо аннотаций типа, тоже одинаков). Если нам нужно применять операции удвоения к различным типам аргументов внутри одной программы, нам придется написать отдельные определения doubleT для каждого T. Такое программирование путем копирования и вставки текста нарушает один из главных принципов разработки программ:

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

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

23.2  Разновидности полиморфизма

Системы типов, позволяющие использовать единый фрагмент кода с различными типами, известны под общим названием полиморфных (polymorphic) (поли = много, морф = форма). В современных языках встречается несколько разновидностей полиморфизма (приводимая здесь классификация основана на работах Стрейчи (Strachey, 1967), а также Карделли и Вегнера (Cardelli and Wegner, 1985)).

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

Наиболее мощной формой параметрического полиморфизма является импредикативный (impredicative) полиморфизм, или полиморфизм первого класса (first-class polymorphism). Именно он обсуждается в данной главе. На практике больше распространен полиморфизм в стиле ML (ML-style), то есть полиморфизм через let (let-polymorphism), ограниченный связываниями let верхнего уровня и запрещающий функции, в которых аргументами служат полиморфные значения. Взамен он предлагает удобную и естественную форму реконструкции типов (type reconstruction) (глава 22). Параметрический полиморфизм первого класса приобретает популярность в языках программирования. Он служит техническим основанием для мощной системы модулей в языках вроде ML (см. Harper and Stone, 2000).

Специализированный полиморфизм (ad-hoc polymorphism), напротив, позволяет полиморфному значению демонстрировать различное поведение при его <<рассмотрении>> относительно разных типов. Самый обычный пример специализированного полиморфизма — перегрузка (overloading), когда один и тот же символ функции соответствует различным реализациям; компилятор (или система времени выполнения, в зависимости от того, идет ли речь о статическом (static) или динамическом (dynamic) разрешении перегрузки) выбирает подходящую реализацию для каждого случая применения функции, исходя из типов ее аргументов.

Обобщая перегрузку функций, мы получаем диспетчеризацию мультиметодов (multi-method), как в CLOS (Bobrow et al., 1988, Kiczales et al., 1991) и Cecil (Chambers, 1992, Chambers and Leavens, 1994). Этот механизм был формализован в λ-&-исчислении Кастаньи, Гелли и Лонго (Castagna, Ghelli, and Longo, 1995; ср. Castagna, 1997).

Более мощная форма специализированного полиморфизма — интенсиональный полиморфизм (intensional polymorphism) (Harper and Morrisett, 1995, Crary, Weirich, and Morrisett, 1998), который допускает ограниченные вычисления над типами во время выполнения. Интенсиональный полиморфизм лежит в основе некоторых сложных методов оптимизации для полиморфных языков, в том числе бестеговой сборки мусора, <<распакованных>> аргументов функций, полиморфной сериализации, а также оптимизированных по памяти <<плоских>> структур данных.

Еще более мощные формы специализированного полиморфизма можно получить на основе конструкции typecase, которая позволяет осуществлять произвольное сопоставление информации о типах с образцом во время выполнения (Abadi, Cardelli, Pierce, and Rémy, 1995, Abadi, Cardelli, Pierce, and Plotkin, 1991b, Henglein, 1994, Leroy and Mauny, 1991, Thatte, 1990). Такие конструкции, как instanceof в Java, можно рассматривать как ограниченную разновидность typecase.

Полиморфизм через подтипы (subtype polymorphism) (глава 15) присваивает несколько типов одному терму с помощью правила включения и позволяет избирательно <<забывать>> часть информации о поведении терма.

Эти категории не являются взаимоисключающими: различные формы полиморфизма могут смешиваться в одном языке. Например, Standard ML поддерживает как параметрический полиморфизм, так и простую перегрузку встроенных арифметических операций, но не поддерживает подтипы, а Java содержит подтипы, перегрузку и простой специализированный полиморфизм (instanceof), но не содержит (на момент написания книги) параметрический полиморфизм. Существует несколько предложений по добавлению параметрического полиморфизма в Java; наиболее известен из них GJ (Bracha, Odersky, Stoutamire, and Wadler, 1998).

Использование термина <<полиморфизм>> без уточнений приводит к некоторой путанице при общении различных программистских сообществ. Среди функциональных программистов (т. е. тех, кто использует или проектирует языки вроде ML, Haskell и т. п.), он почти всегда означает параметрический полиморфизм. Среди программистов, работающих с объектно-ориентированными языками, он, напротив, почти всегда означает полиморфизм через подтипы, а параметрический полиморфизм обозначается термином обобщенные функции (generics).

23.3  Система F

Система, которую мы изучаем в этой главе, известна под названием Системы F (System F). Ее впервые открыл Жан-Ив Жирар (Girard, 1972) в контексте теории доказательств в логике. Несколько позже систему типов с практически той же выразительной мощностью независимо построил специалист по информатике Джон Рейнольдс (Reynolds, 1974), который назвал ее полиморфным лямбда-исчислением (polymorphic lambda-calculus). Эта система активно используется как исследовательский инструмент для работ по основаниям полиморфизма, а также послужила базой для многочисленных проектов языков программирования. Иногда ее также называют лямбда-исчислением второго порядка (second-order lambda calculus), поскольку по соотношению Карри-Говарда (Curry-Howard correspondence) она аналогична интуиционистской логике второго порядка, в которой разрешена квантификация не только по отдельным объектам [термам], но и по предикатам [типам].

Определение Системы F является естественным расширением λ, простого типизированного лямбда-исчисления. В λ лямбда-абстракция служит для абстрагирования термов из термов, а с помощью применения вместо абстрагированных частей подставляются значения. Поскольку теперь нам понадобился механизм для абстрагирования типов из термов, а также для последующего заполнения абстракций, мы вводим новую форму абстракции, которую мы записываем в виде λX.t, параметром которой служит тип, и новую форму применения, t [T], в которой аргументом служит выражение типа. Мы называем эти новые абстракции абстракциями типа (type abstractions), а новую конструкцию применения — применением (type application) или конкретизацией типа (type instantiation).

Когда при вычислении абстракция типа сочетается с применением типа, получается редекс, в точности как в λ. Мы добавляем в систему правило редукции:

  (λX.t12) [T2] → [X ↦ T2]t12

аналогичное обыкновенному правилу редукции для термов-абстракций и термов-применений:

  (λx:T11.t12) v2 → [x ↦ v2]t12

Например, при применении полиморфной функции тождества (identity function)

id = λX. λx:X. x;

к типу Nat в выражении id [Nat] результатом будет [XNat](λx:X.x), т. е. λx:Nat.x, функция тождества на натуральных числах.

Наконец, мы должны указать тип полиморфной абстракции. Такие типы, как NatNat, используются для описания обыкновенных функций вроде λx:Nat.x; теперь для описания полиморфных функций вроде id нам нужен другой вид <<функционального типа>>, областью определения которого служат типы. Заметим, что для каждого типа-аргумента T, к которому применяется id, она возвращает функцию вида TT; то есть, тип результата id зависит от конкретного типа, передаваемого ей в качестве аргумента. Чтобы отразить эту зависимость, мы записываем тип id как X.XX. Правила типизации для полиморфных абстракции и применения аналогичны правилам для абстракции и применения на уровне термов.

  
Γ, X ⊢ t2 : T2
Γ ⊢ λX.t2 : X.T2
  
Γ ⊢ t1 : X.T12
Γ ⊢ t1 [T2] : [XT2]T12

Обратите внимание, что мы включаем типовую переменную X в контекст, используемый в подвыводе для t. Продолжает действовать соглашение (4), согласно которому имена переменных (термовых или типовых) должны быть выбраны так, чтобы отличаться от уже связанных в Γ, а переменные, связанные лямбдами, можно при необходимости переименовывать, чтобы выполнить это условие. (В некоторых вариантах изложения Системы F это условие новизны задается как явное дополнительное условие в правиле T-TAbs, а не встраивается в правила построения контекстов, как у нас.) Пока что единственная роль типовых переменных в контекстах заключается в отслеживании областей видимости и защите от повторного добавления одной и той же типовой переменной в контекст. В последующих главах мы будем снабжать типовые переменные различной информацией, например, ограничениями (bounds) (глава 26) или видами (kinds) (глава 29).

На рис. 23.1 приведено полное определение полиморфного лямбда-исчисления, и выделены его отличия от λ. Как обычно, здесь определяется только чистое исчисление, без конструкторов типов вроде записей, без базовых типов вроде Nat и Bool и без расширений термового языка вроде let и fix. Эти дополнительные конструкции можно без труда добавить в чистую систему, и в последующих примерах мы будем их часто использовать.


На основе λ (9.1)



Синтаксис
t::= термы:
x переменная
λx:T.t абстракция
t t применение
λX.t абстракция типа
t [T] применение типа
 
v::= значения:
λx:T.t значение-абстракция
λX.t значение-абстракция типа
 
T::= типы:
X типовая переменная
TT тип функций
X.T универсальный тип
 
Γ::= контексты:
пустой контекст
Γ,x:T связывание термовой переменной
Γ,X связывание типовой переменной
Вычислениеtttt
        
t1 → t1
t1 t2 → t1 t2
        
t2 → t2
v1 t2 → v1 t2
        
(λx:T11.t12) v2 → [x ↦ v2]t12
        
t1 → t1
t1 [T2] → t1 [T2]
 
         (λX.t12) [T2] → [XT2]t12  

ТипизацияΓ ⊢ t : TΓ ⊢ t : T

          
x : T ∈ Γ
Γ ⊢ x : T
        
Γ, x:T1 ⊢ t2:T2
Γ ⊢ λx:T1.t2 : T1 T2
        
Γ ⊢ t1 : T11 T12           Γ ⊢ t2 : T11
Γ ⊢ t1 t2 : T12
        
Γ, X ⊢ t2 : T2
Γ ⊢ λX.t2 : X.T2
 
        
Γ ⊢ t1 : X.T12
Γ ⊢ t1 [T2] : [XT2]X.T12
 



Figure 23.1: Полиморфное лямбда-исчисление (Система F)


23.4  Примеры

Приведем несколько примеров программирования с использованием полиморфизма. Начнем, для разминки, с нескольких небольших, но постепенно усложняющихся примеров, которые иллюстрируют выразительные возможности Системы F. Затем кратко рассмотрим основные идеи <<обыкновенного>> полиморфного программирования со списками, деревьями и т. п. В последних двух разделах вводятся типизированные варианты кодирования по Чёрчу для простых алгебраических типов — булевских значений, чисел и списков. (Само кодирование рассматривалось в главе 5 для бестипового лямбда-исчисления.) Несмотря на то, что эти варианты кодирования не имеют особой практической ценности — для этих важных элементов языка проще создать хороший код, если они встроены как примитивы, — они служат замечательными примерами, на которых можно продемонстрировать как тонкости, так и выразительную силу Системы F. В главе 24 мы увидим некоторые другие приложения полиморфизма в области модульного программирования (modular programming) и абстрактных типов данных (АТД).

Разминка

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

id = λX. λx:X. x; |> id : ∀X. X -> X

и конкретизировать ее так, чтобы получить любую необходимую функцию тождества:

id [Nat]; |> <fun> : Nat -> Nat id [Nat] 0; |> 0 : Nat

Более полезным примером может служить полиморфная функция удвоения:

double = λX. λf:X -> X. λa:X. f (f a); |> double : ∀X. (X -> X) -> X -> X

Абстракция по типу X позволяет получать функции удвоения для конкретных типов, применяя функцию double к различным аргументам-типам:

doubleNat = double [Nat]; |> doubleNat : (Nat -> Nat) -> Nat -> Nat doubleNatArrowNat = double [Nat -> Nat]; |> doubleNatArrowNat : ((Nat -> Nat) -> Nat -> Nat) -> (Nat -> Nat) -> Nat -> Nat

Конкретизировав функцию double аргументом-типом, её можно применить к конкретной функции и аргументу, имеющим соответствующие типы:

double [Nat] (λx:Nat. succ(succ(x))) 3; |> 7 : Nat

Вот пример похитрее: полиморфное самоприменение. Напомним, что в простом типизированном лямбда-исчислении невозможно присвоить тип терму λx. x x (упражнение 2). А вот в Системе F этот терм оказывается типизируем, если придать x полиморфный тип и должным образом его конкретизировать:

selfApp = λx:∀X.X -> X. x [∀X.X -> X] x; |> selfApp : (∀X. X -> X) -> (∀X. X -> X)

В качестве (чуть) более полезного примера самоприменения можно применить к себе самой функцию double и получить полиморфную функцию учетверения:

quadruple = λX. double [X -> X] (double [X]); |> quadruple : ∀X. (X -> X) -> X -> X
Упражнение 1   [★ ↛]: Используя правила по рис. 23.1, убедитесь в том, что вышеприведенные термы на самом деле имеют типы, которые указаны в примерах.

Полиморфные списки

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

|> nil : ∀X. List X cons : ∀X. X -> List X -> List X isnil : ∀X. List X -> Bool head : ∀X. List X -> X tail : ∀X. List X -> List X

Когда мы впервые ввели списки в §11.12, мы позволили применять элементарные операции к спискам с элементами любого типа через <<специализированные>> правила вывода, созданные специально для списков. Теперь мы можем приписать этим операциям полиморфные типы, выражающие в точности те же самые ограничения — то есть, списки больше не надо <<вплавлять>> в базовый язык; их можно просто рассматривать как библиотеку, содержащую несколько констант, имеющих определенные полиморфные типы. То же самое верно для типа Ref и элементарных операций над ссылочными ячейками из главы 13, а также для многих других структур данных и управления.

С помощью этих примитивов мы можем определять собственные полиморфные операции над списками. Вот, например, полиморфная функция map, которая принимает функцию, переводящую X в Y, и список X-ов, и возвращает список Y-ов.

map = λX. λY. λf: X -> Y. (fix (λm: (List X) -> (List Y). λl: List X. if isnil [X] l then nil [Y] else cons [Y] (f (head [X] l)) (m (tail [X] l)))); |> map : ∀X. ∀Y. (X -> Y) -> List X -> List Y l = cons [Nat] 4 (cons [Nat] 3 (cons [Nat] 2 (nil [Nat]))); |> l : List Nat head [Nat] (map [Nat] [Nat] (λx:Nat. succ x) l); |> 5 : Nat
Упражнение 2   [★ ↛]: Убедитесь в том, что map действительно имеет указанный тип.
Упражнение 3   [Рекомендуется, ★★]: Используя в качестве образца map, напишите полиморфную функцию обращения списка
reverse : X. List X -> List X
Это упражнение лучше всего выполнять в интерактивном режиме. Запустите интерпретатор fullomega и скопируйте содержимое файла test.f из каталога fullomega в начало своего исходного файла. (В этом файле содержатся определения конструктора List и соответствующих операций. Эти определения требуют мощных возможностей абстракции Системы Fω, описанных в главе 29. Для работы с этим упражнением не обязательно в точности понимать, как они работают.)
Упражнение 4   [★★ ↛]: Напишите простую полиморфную функцию сортировки
sort : X. (X -> X -> Bool) -> (List X) -> List X
в которой первым аргументом служит функция сравнения для элементов типа X.

Кодирование по Чёрчу

В §5.2 мы видели, что многие элементарные значения данных, такие как булевские значения, числа и списки, могут быть закодированы в виде функций в чистом бестиповом лямбда-исчислении. В этом разделе мы покажем, как то же самое кодирование по Чёрчу (Church encoding) можно произвести в Системе F. Читатель может при желании освежить свое понимание кодирования по Чёрчу, перечитав §5.2.

Кодирование по Чёрчу интересно по двум причинам. Во-первых, оно служит хорошим упражнением, развивающим понимание абстракции и применения типов. Во-вторых, оно показывает, что, как и чистое бестиповое лямбда-исчисление, Система F является вычислительно весьма богатым языком в том смысле, что чистая система способна выразить широкий спектр структур данных и управления. Следовательно, если мы разработаем полноценный язык программирования, в основе которого лежит Система F, то все эти структуры можно добавить в него как примитивы (из соображений эффективности, а также для того, чтобы снабдить их более удобным конкретным синтаксисом), не нарушив при этом основные свойства базового языка. Разумеется, для всех интересных высокоуровневых языковых конструкций это не так. Например, добавление ссылок (references) в Систему F, как мы это сделали для λ в главе 13, влечет за собой существенное изменение фундаментальной вычислительной природы исчисления.

Начнем с Чёрчевых булевских значений. Напомним, что в бестиповом лямбда-исчислении мы представляли булевские константы true и false в виде лямбда-термов tru и fls:

tru = λt. λf. t; fls = λt. λf. f;

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

CBool = ∀X.X -> X -> X

Термы tru и fls в Системе F получаются добавлением соответствующих аннотаций типа к вышеприведенным бестиповым версиям:

tru = λX. λt:X. λf:X. t; |> tru : CBool fls = λX. λt:X. λf:X. f; |> fls : CBool

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

not = λb:CBool. λX. λt:X. λf:X. b [X] f t; |> not : CBool -> CBool
Упражнение 5   [Рекомендуется, ★]: Напишите терм, принимающий два аргумента типа CBool и возвращающий их конъюнкцию (оператор and).

Аналогично можно обращаться и с числами. Числа Чёрча (Church numerals), введенные в §5.2, кодируют натуральное число n в виде функции, которая принимает два аргумента, s и z, и n раз применяет s к z:

c0 = λs. λz. z; c1 = λs. λz. s z; c2 = λs. λz. s (s z); c3 = λs. λz. s (s (s z));

Понятно, что аргумент z должен иметь тот же тип, что и область определения s, и что результат s должен снова иметь тот же самый тип. Это приводит нас к следующему типу чисел Чёрча для Системы F:

CNat = ∀X. (X -> X) -> X -> X;

Элементы этого типа получаются путем добавления соответствующих аннотаций к бестиповым числам Чёрча:

c0 = λX. λs:X -> X. λz:X. z; |> c0 : CNat c1 = λX. λs:X -> X. λz:X. s z; |> c1 : CNat c2 = λX. λs:X -> X. λz:X. s (s z); |> c2 : CNat

Типизированная функция-последователь для чисел Чёрча определяется так:

csucc = λn:CNat. λX. λs:X -> X. λz:X. s (n [X] s z); |> csucc : CNat -> CNat

То есть, csucc возвращает элемент типа CNat, который, получая s и z, n раз применяет s к z (путем вызова n с аргументами s и z), а затем применяет s еще раз. Подобным образом можно определить и другие арифметические операции. Например, сложение можно определить либо через csucc:

cplus = λm:CNat. λn:CNat. m [CNat] csucc n; |> cplus : CNat -> CNat -> CNat

либо более прямым образом:

cplus = λm:CNat. λn:CNat. λX. λs:X -> X. λz:X. m [X] s (n [X] s z); |> cplus : CNat -> CNat -> CNat

Если в нашем языке присутствуют также числа в виде примитивов (рис. 8.2), то мы можем преобразовывать числа Чёрча в обыкновенные с помощью следующей функции:

cnat2nat = λm:CNat. m [Nat] (λx:Nat. succ(x)) 0; |> cnat2nat : CNat -> Nat

Она позволяет убедиться в том, что наши операции над числами Чёрча действительно вычисляют требуемые арифметические функции:

cnat2nat (cplus (csucc c0) (csucc (csucc c0))); |> 3 : Nat
Упражнение 6   [Рекомендуется, ★★]: Напишите функцию iszero, которая будет возвращать tru, будучи применена к числу Чёрча c0, и fls в противном случае.
Упражнение 7   [★★ ↛]: Убедитесь в том, что термы
ctimes = λm:CNat. λn:CNat. λX. λs:X -> X. n [X] (m [X] s); |> ctimes : CNat -> CNat -> CNat cexp = λm:CNat. λn:CNat. λX. n [X -> X] (m [X]); |> cexp: CNat -> CNat -> CNat
имеют указанные типы. Неформально объясните, как они реализуют арифметическое умножение и возведение в степень.
Упражнение 8   [Рекомендуется, ★★]: Покажите, что тип
PairNat = X. (CNat -> CNat -> X) -> X;
можно использовать для представления пар чисел, написав функции
pairNat : CNat -> CNat -> PairNat; fstNat : PairNat -> CNat; sndNat : PairNat -> CNat;
для построения элемента этого типа из пары чисел, а также для доступа к первой и второй компоненте такой пары.
Упражнение 9   [Рекомендуется, ★★★]: С помощью функций, определенных в упр. 8, напишите функцию pred, вычисляющую предшественник числа Чёрча (и возвращающую 0, если 0 подан на вход). Подсказка: основная идея приведена в примере из §5.2. Определите функцию f : PairNatPairNat, которая переводит пару (i,j) в (i+1, i) — то есть, отбрасывает второй компонент своего аргумента, копирует первый компонент во второй, и увеличивает первый. Тогда n применений f к начальной паре (0,0) дадут нам пару (n, n−1), откуда мы можем получить предшественника n, взяв второй компонент.
Упражнение 10   [★★★]: Вот еще один способ получить предшественник числа Чёрча. Пусть k обозначает бестиповый лямбда-терм λx. λy. x, а i обозначает λx. x. Бестиповый лямбда-терм
vpred = λn. λs. λz. n (λp. λq. q (p s)) (k z) i
(из статьи Барендрегта (Barendregt, 1992), со ссылкой на Й. Вельманса) вычисляет предшественник данного бестипового числа Чёрча. Покажите, что этот терм можно типизировать в Системе F, добавляя по необходимости абстракции и применения типов, а также помечая связанные переменные в бестиповом терме соответствующими типами. Дополнительные очки наберет тот, кто объяснит, как этот терм действует!

Кодирование списков

В качестве последнего примера распространим кодирование чисел по Чёрчу на случай списков. Этот пример демонстрирует изящество и мощь Системы F, поскольку показывает, что все примеры программ из предыдущего подраздела, касающиеся полиморфной обработки списков, выразимы в чистом языке. (Удобства ради, мы порождаем рекурсивные функции общего вида через конструкцию fix, однако в сущности, те же построения могут работать и без нее. См. упражнения 11 и 12.)

В упражнении 8 мы убедились, что в бестиповом лямбда-исчислении списки можно представить при помощи приемов, очень близких тем, которые используются при кодировании натуральных чисел. В сущности, число в единичной записи подобно списку из некоторых элементов, точная природа которых несущественна. Обобщая эту идею на элементы произвольного типа, мы получаем способ кодирования списков по Чёрчу, в котором список с элементами x, y и z представляется как функция, которая, получая функцию f и начальное значение v, вычисляет f x (f y (f z v)). В терминологии OCaml, список представляется в виде своей собственной функции fold_right.

Тип List X списков с элементами типа X определяется так:

List X = ∀R. (X -> R -> R) -> R -> R;

Значение nil в этом представлении записать несложно:1

nil = λX. (λR. λc:X -> R -> R. λn:R. n) as List X; |> nil : ∀X. List X

Операции cons и isnil также не представляют труда:

cons = λX. λhd:X. λtl:List X. (λR. λc:X -> R -> R. λn:R. c hd (tl [R] c n)) as List X; |> cons : ∀X. X -> List X -> List X isnil = λX. λl:List X. l [Bool] (λhd:X. λtl:Bool. false) true; |> isnil : ∀X. List X -> Bool

Операция head требует несколько больших усилий. Первая сложность состоит в вопросе, что делать с головой пустого списка. На этот вопрос мы можем ответить, вспомнив, что при наличии в языке оператора неподвижной точки общего вида с его помощью можно построить выражение любого типа. На самом деле, с помощью абстракции типов мы можем пойти еще дальше и написать единую обобщенную функцию, которая, получая тип X, выдает функцию из Unit в X, зацикливающуюся при применении к unit.

diverge = λX. λ_:Unit. fix (λx:X. x); |> diverge : ∀X. Unit -> X

Теперь мы можем использовать diverge[X] unit в качестве <<результата>> вычисления head [X] nil.

head = λX. λl:List X. l [X] (λhd:X. λtl:X. hd) (diverge [X] unit); |> head : ∀X. List X -> X

К сожалению, это определение — еще не вполне то, что нам нужно: функция не завершается никогда, даже будучи примененной к непустым спискам. Чтобы получить требуемое поведение, нужно несколько изменить функцию так, чтобы diverge [X] не получала свой аргумент типа Unit, выступая в качестве аргумента l. Ради этого мы убираем аргумент unit и соответствующим образом изменяем тип первого аргумента l:

head = λX. λl: List X. (l [Unit -> X] (λhd:X. λtl:Unit -> X. λ_:Unit. hd) (diverge [X])) unit; |> head : ∀X. List X -> X

То есть, l применяется к функции типа X(UnitX)(UnitX) и к базовому значению типа UnitX. В случае, когда l соответствует пустому списку, результатом будет diverge [X]; однако когда l соответствует непустому списку, результатом будет функция, которая принимает unit и возвращает головной элемент l. Результат l в конце применяется к unit, и таким образом извлекается настоящая голова списка, имеющая нужный нам тип (или, если нам не повезло, вычисление зацикливается). Таким образом, у head оказывается нужный нам тип.

В случае функции tail мы используем сокращение Pair X Y (обобщающее тип PairNat из Упражнения 8) и с его помощью строим кодирование по Чёрчу пар, у которых первый элемент имеет тип X, а второй — тип Y:

Pair X Y = ∀R. (X -> Y -> R) -> R;

Операции над парами являются простыми обобщениями вышеприведенных операций над типом PairNat:

|> pair : ∀X. ∀Y. X -> Y -> Pair X Y fst : ∀X. ∀Y. Pair X Y -> X snd : ∀X. ∀Y. Pair X Y -> Y

Теперь функция tail пишется так:

tail = λX. λl: List X. (fst [List X] [List X] ( l [Pair (List X) (List X)] (λhd: X. λtl: Pair (List X) (List X). pair [List X] [List X] (snd [List X] [List X] tl) (cons [X] hd (snd [List X] [List X] tl))) (pair [List X] [List X] (nil [X]) (nil [X])))); |> tail : ∀X. List X -> List X
Упражнение 11   [★★]: Строго говоря, в примерах из этого подраздела используется не чистая Система F, поскольку для порождения значения, <<возвращаемого>>, когда head применяется к пустому списку, мы использовали fix. Напишите альтернативную версию head, которая принимает дополнительный параметр и возвращает его (вместо зацикливания), если список на входе оказывается пустым.
Упражнение 12   [Рекомендуется, ★★★]: Напишите на языке чистой Системы F (без использования fix) функцию insert, имеющую тип
X. (X -> X -> Bool) -> List X -> X -> List X
которая принимает функцию сравнения, отсортированный список, и новый элемент. Она должна вставить элемент в список на подходящее ему место (т. е. вслед за всеми элементами, меньшими его самого). При помощи insert напишите функцию сортировки для списков на языке чистой Системы F.

23.5  Основные свойства

Фундаментальные свойства Системы F весьма близки к свойствам простого типизированного лямбда-исчисления. В частности, доказательства теорем о сохранении типов и о продвижении являются простыми расширениями доказательства тех же теорем из главы 9.

Теорема 1   [Сохранение]: Если Γ ⊢ t : T и tt’, то Γ ⊢ t’ : T.

Доказательство: Упражнение [Рекомендуется, ★★★].

Теорема 2   [Продвижение]: Если имеется замкнутый правильно типизированный терм t, то t либо является значением, либо существует некоторый терм t’ такой, что tt’.

Доказательство: Упражнение [Рекомендуется, ★★★].

Кроме того, Система F, подобно λ, обладает свойством нормализации (normalization) — вычисление всякой правильно типизированной программы завершается.2 В отличие от приведенных выше теорем о типовой безопасности, доказательство нормализации весьма сложно (в сущности, удивительно уже то, что это свойство вообще имеется, учитывая, что в чистом языке можно закодировать такие вещи, как функции сортировки (см. упражнение 12) без обращения к fix). Это доказательство, основанное на обобщении метода, представленного нами в главе 12, было одним из основных достижений докторской диссертации Жирара (Girard, 1972; см. также Girard, Lafont, and Taylor, 1989). С тех пор его метод доказательства был проанализирован и переработан многими другими исследователями (см. Gallier, 1990).

Теорема 3   [Нормализация]: Правильно типизированные термы Системы F являются нормализующими.

23.6  Стирание, типизируемость и реконструкция типов

Как и в случае λ в §9.5, мы можем определить функцию стирания типов (type erasure), которая переводит термы Системы F в термы бестипового лямбда исчисления, отбрасывая аннотации типов (включая все абстракции типов и применения типов):

  erase(x)=x 
  erase(λx:T1.t2)=λx.erase(t2) 
  erase(t1 t2)=erase(t1)   erase(t2
  erase(λX.t2)=erase(t2
  erase(t1 [T2])=erase(t1)

Терм m бестипового лямбда-исчисления называется типизируемым (typable) в Системе F, если существует какой-либо правильно типизированный терм t, такой, что erase(t) = m. Задача реконструкции типов (type reconstruction) состоит в том, чтобы, имея бестиповый терм m, сказать, можем ли мы отыскать некоторый правильно типизированный терм, дающий при стирании m.

Реконструкция типов для Системы F была одной из самых долгоживущих нерешенных проблем в области исследований по языкам программирования. Вопрос оставался открытым с начала 70-х до тех пор, пока Уэллс не ответил на него отрицательно в начале 90-х годов.

Теорема 1   [Уэллс (Wells, 1994)]: Для данного замкнутого терма m в бестиповом лямбда-исчислении задача о существовании правильно типизированного терма t Системы F, такого, что erase(t) = m, неразрешима.

Известно, что не только реконструкция типов сама по себе, но и некоторые ее частичные формы в Системе F неразрешимы. Рассмотрим, например, следующее отношение <<частичного стирания>>, которое сохраняет все аннотации типов, кроме (возможно) аргументов к применениям типов. Заметим, что местоположение применений типов отмечается в частично стертых термах пустыми квадратными скобками.

  x  x
  
t2  t2
λx:T1. t2  λx:T1. t2
  
t1  t1           t2  t2
t1 t2  t1 t2
 
  
t2  t2
λX.t2  λX.t2
  
t1  t1
t1 [T2]  t1 [T2]
  
t1  t1
t1 [T2]  t1 []
 
Теорема 2   [Пфеннинг (Pfenning, 1993a)]: Для данного терма s задача о существовании правильно типизированного терма t Системы F, такого, что t s, неразрешима.

Основываясь на более ранних наблюдениях Бёма (Boehm, 1985, Boehm, 1989), Пфеннинг показал, что такая форма реконструкции типов столь же сложна, как унификация высших порядков, про которую уже было известно, что она неразрешима. Интересно, что этот отрицательный результат прямо привел к созданию полезного метода частичной реконструкции типов (Pfenning, 1988, Pfenning, 1993a), основанного на ранних работах Юэ по эффективным полуалгоритмам для унификации высших порядков (Huet, 1975). Среди дальнейших улучшений в этом направлении исследований — более тонкий алгоритм для решения ограничений высших порядков (Dowek, Hardin, Kirchner, and Pfenning, 1996), исключающий опасность незавершения алгоритма или порождения множественных решений. Использование родственных алгоритмов в таких языках, как LEAP (Pfenning and Lee, 1991), Elf (Pfenning, 1989) и FX (O’Toole and Gifford, 1989), показало, что на практике они ведут себя вполне прилично.

Другой подход к частичной реконструкции типов основан на сделанном Перри наблюдении о том, что экзистенциальные типы первого класса (см. главу 24) совместимы с используемым в ML механизмом datatype (Perry, 1990); эту идею дальше развили Лойфер и Одерский (Läufer, 1992, Läufer and Odersky, 1994). В сущности, конструкторы и деструкторы datatype можно рассматривать как явные аннотации типа, которые указывают места, где требуется упаковывать и распаковывать значения типов-непересекающихся объединений, где нужно сворачивать и разворачивать рекурсивные типы, а также, если добавлены экзистенциальные типы, где требуется вести их упаковку и распаковку. Реми (Rémy, 1994) удалось распространить эту идею на (импредикативные) универсальные типы первого класса. Недавнее предложение Одерского и Лойфера (Odersky and Läufer, 1996), которое развили далее Гарриг и Реми (Garrigue and Rémy, 1997), строит консервативное расширение реконструкции типов в стиле ML, позволяя программистам явно указывать типы аргументов функций, и эти аннотации (в отличие от выводимых автоматически) могут содержать универсальные кванторы. Таким образом, сужается разрыв между ML и более мощными импредикативными системами. Преимуществом этого семейства подходов является относительная простота и изящная интеграция с полиморфизмом языка ML.

Прагматический подход к частичной реконструкции типов для систем, одновременно включающих подтипы и импредикативный полиморфизм, называется локальным выводом типов (local type inference) (или локальной реконструкцией типов, local type reconstruction). Он был предложен Пирсом и Тёрнером (Pierce and Turner, 1998; см. также ???). Локальный вывод типов присутствует также в некоторых современных языковых проектах, включая GJ (Bracha, Odersky, Stoutamire, and Wadler, 1998) и Funnel (Odersky and Zenger, 2001). В последнем вводится более мощная форма вывода, которая называется окрашенным локальным выводом типов (colored local type inference) (Odersky, Zenger, and Zenger, 2001).

Более простой, но менее предсказуемый алгоритм жадного вывода типов (greedy type inference) был предложен Карделли (Cardelli, 1993); подобные алгоритмы также используются в программах проверки доказательств для теорий с зависимыми типами, например, Nuprl (Howe, 1988) и Lego (Pollack, 1990). Здесь идея состоит в том, что любая аннотация типа может быть опущена программистом: для каждого такого случая процедура синтаксического разбора порождает новую переменную унификации X. При проверке типов алгоритму проверки подтпирования можно задать вопрос, является ли некоторый тип S подтипом T, причем как S, так и T могут содержать переменные унификации. Проверка подтипирования ведется как обычно до тех пор, пока не возникает подцель вида X <: T или T <: X. В таком месте X конкретизируется типом T, и текущее ограничение удовлетворяется простейшим из возможных способов. Однако присваивание переменной X значения T может быть неоптимальным решением, и это может привести к дальнейшим неудачным проверкам подтипирования для типов, включающих X, при том что другой выбор мог бы привести к успеху. Однако использование этого алгоритма на практике в реализации Карделли и в ранней версии языка Pict (Pierce and Turner, 2000) показывает, что жадный выбор алгоритма почти всегда правилен. Однако в случаях, когда выбор оказывается неверным, поведение жадного алгоритма может быть совершенно непонятным для программиста и приводить к таинственным сообщениям об ошибках далеко от того места, где была сделана неоптимальная конкретизация.

Упражнение 3   [★★★★]: Из свойства нормализации следует, что бестиповый терм omega = (λx. x x) (λy. y y) не может быть типизирован в Системе F, поскольку редукция omega никогда не достигает нормальной формы. Однако можно получить и более прямое, <<комбинаторное>> доказательство этого утверждения, рассматривая только правила, определяющие отношение типизации.
  1. Назовем терм Системы F незащищенным (exposed), если это переменная, абстракция λx:T.t или применение t s (т. е., если терм не является абстракцией типа λX.t или применением типа t [S]).

    Покажем, что если терм t правильно типизирован (в некотором контексте) и erase(t) = m, то существует некоторый незащищенный терм s, такой, что erase(s) = m, и s правильно типизирован (возможно, в другом контексте).

  2. Будем использовать запись λAX.t, которая обозначает последовательность абстракций типа вида λX1...λXn.t. Аналогично, будем писать t [AA], обозначая таким образом вложенную последовательность применений типа ((t [A1])...[An-1]) [An] и AX.T для вложенной последовательности полиморфных типов X1...Xn.T. Следует учитывать, что эти последовательности могут быть пустыми. Например, если AX — пустая последовательность типовых переменных, то AX.T — просто T.

    Покажем, что если erase(t) = m и Γ ⊢ t : T, то существует некоторый терм s вида λX. (u [AA]) для некоторой последовательности типовых переменных AX, некоторой последовательности типов AA и некоторого незащищенного терма u, для которых erase(s) = m и Γ ⊢ s : T.

  3. Покажем, что если t — незащищенный терм типа T (в контексте Γ) и erase(t) = m n, то t имеет вид s u для некоторых термов s и u, таких, что erase(s) = m и erase(u) = n, и при этом Γ ⊢ s : UT и Γ ⊢ u : U.
  4. Допустим, что x:T ∈ Γ. Покажем, что если Γ ⊢ u : U и erase(u) = x x, то либо
    1. T = ∀AX.Xi, где XiAX, либо
    2. T = ∀AX1AX2.T1T2, где [AX1AX2A]T1 = [AX1B](AZ.T1T2) для некоторых последовательностей типов AA и AB, таких, что |AA| = |AX1 AX2| и |AB| = |AX1|.
  5. Покажем, что, если erase(s) = λx.m и Γ ⊢ s : S, то S имеет вид AX.S1S2 для некоторых AX, S1 и S2.
  6. Определяем самый левый лист (leftmost leaf) типа T:
          leftmost-leaf(X)=X 
          leftmost-leaf(ST)=leftmost-leaf(S
          leftmost-leaf(X.S)=leftmost-leaf(S). 
        
    Покажем, что, если [AX1 AX2AA](AY.T1) = [AX1AB](AZ.(AY.T1)T2), то должно выполняться leftmost-leaf(T1) = Xi для некоторого XiAX1 AX2.
  7. Покажем, что терм omega не типизируем в Системе F.

23.7  Стирание и порядок вычислений

Операционная семантика Системы F, определенная на рис. 23.1 — это семантика с передачей типов (type-passing semantics): когда полиморфная функция принимает аргумент-тип, он действительно подставляется в тело функции. Реализация Системы F в главе 25 именно так и поступает.

В более практическом интерпретаторе или компиляторе для языка программирования, основанного на Системе F, такая манипуляция типами во время исполнения может приводить к существенным затратам. Более того, нетрудно заметить, что аннотации типов не играют никакой существенной роли во время исполнения, в том смысле, что при исполнении не принимается никаких решений на основе типов: можно взять правильно типизированную программу, произвольным образом переписать ее аннотации типов, и получить новую программу, которая ведёт себя точно так же. Поэтому многие полиморфные языки основаны на семантике со стиранием типов (type-erasure semantics), в которой после завершения фазы проверки типов вся типовая информация уничтожается, и уже получившиеся бестиповые термы интерпретируются либо компилируются в машинный код.3

Однако в полноценном языке программирования, в котором есть конструкции с побочными эффектами вроде изменяемых ячеек памяти или исключений, функция стирания типов требует более тщательного определения, чем функция полного стирания из §23.6. Например, если мы дополним Систему F примитивом error для сигнализации об ошибках (§14.1), то терм

let f = (λX.error) in 0;

дает при вычислении 0, поскольку λX.error — синтаксическое значение, и терм error в его теле не подлежит исполнению. Однако, получаемый при стирании терм

let f = error in 0;

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

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

  erasev(x)=x 
  erasev(λx:T1.t2)=λx.erasev(t2) 
  erasev(t1 t2)=erasev(t1)   erasev(t2
  erasev(λX.t2)=λ_ . erasev(t2
  erasev(t1 [T2])=erasev(t1)   dummyv

где dummyv — некоторое произвольное бестиповое значение, например, unit.5 Корректность новой функции стирания подтверждается наблюдением о том, что она может проводиться в любом порядке относительно бестипового вычисления.

Теорема 2   Если erasev(t) = u, то либо (1) как t, так и u являются нормальными формами относительно своих собственных отношений вычисления, либо (2) tt’, а uu’, причем erasev(t’) = u’.

23.8  Варианты Системы F

Благодаря своему изяществу и мощи Система F занимает центральное место в теоретических исследованиях полиморфизма. Однако в разработке языков часто считается, что потеря реконструкции типов — слишком дорогая цена за гибкость, которая так редко используется в полную меру. Отсюда возникают несколько различных вариантов подмножеств Системы F, для которых задача реконструкции более решаема.

Самое известное из них — полиморфизм через let в стиле ML (§22.7), которое иногда также называется пренекс-полиморфизм (prenex-polymorphism), поскольку его можно рассматривать как вариант Системы F, в котором типовые переменные имеют областью определения только типы без кванторов (монотипы, monotypes), а типы с кванторами (политипы, polytypes, или схемы типов, types schemas) не могут оказаться слева от стрелок. Особая роль конструкции let в ML затрудняет формальное выражение этого соответствия; подробности можно найти в Jim, 1995.

Еще одно хорошо изученное ограничение Системы F — полиморфизм ранга 2 (rank-2 polymorphism), введенный Леивантом (Leivant, 1983) и подробно исследованный многими другими (см. ???). Тип называется типом ранга 2, если при его изображении в виде дерева никакой путь от его корня к квантору ∀ не проходит слева от более чем двух стрелок. Например, (X.XX)Nat имеет ранг 2, а также NatNat и Nat(X.XX)NatNat. Однако, ((X.XX)Nat)Nat типом ранга 2 не является. В системе ранга 2 все типы должны быть ранга 2. Эта система несколько более мощная, чем пренексный (ML) вариант, в том смысле, что она способна присвоить типы большему количеству лямбда-термов.

Кфури и Тюрин (Kfoury and Tiuryn, 1990) доказали, что вычислительная сложность реконструкции типов для варианта Системы F ранга 2 равна сложности ML-фрагмента (т. е., DExptime-полна). Кфури и Уэллс (Kfoury and Wells, 1999) построили первый правильный алгоритм реконструкции типов для системы ранга 2 и показали, что задача реконструкции типов для рангов 3 и выше Системы F неразрешима.

Ограничение ранга 2 может применяться и к другим мощным конструкторам типов помимо кванторов. Например, типы-пересечения (intersection types) (см. §15.7) можно ограничить рангом 2, если запретить типы, в которых оператор пересечения находится слева более чем от двух стрелок (Kfoury, Mairson, Turbak, and Wells, 1999). Варианты ранга 2 Системы F и системы типов первого порядка с пересечениями тесно связаны. Действительно, Джим (Jim, 1995) показал, что они могут присваивать типы в точности одним и тем же термам.

23.9  Параметричность

Вспомним, как в §23.4 мы определили тип CBool булевских значений, закодированных по Чёрчу:

CBool = ∀X.X -> X -> X;

и константы tru и fls:

tru = λX. λt:X. λf:X. t; |> tru : CBool fls = λX. λt:X. λf:X. f; |> fls : CBool

Имея тип CBool, определения термов tru и fls можно выписать почти механически, просто глядя на структуру типа. Поскольку CBool начинается с квантора ∀, любое его значение будет абстракцией типа, так что tru и fls обязаны начинаться с λX. Далее, поскольку тело CBool является функциональным типом XXX, каждое значение этого типа должно принимать два аргумента типа X — т. е. тела tru и fls обязаны начинаться с λt:X. λf:X. Наконец, поскольку результирующий тип CBool — опять же, X, каждое значение типа CBool должно возвращать элемент типа X. Но поскольку X — параметр, единственные значения этого типа, которые мы в состоянии вернуть — это связанные переменные t и f; никаких других способов получить или создать значение этого типа у нас нет. Другими словами, tru и fls, в сущности, исчерпывают собой тип CBool. Строго говоря, CBool содержит некоторые другие термы, такие как (λb:CBool.b) tru, но интуитивно ясно, что каждый из них ведет себя либо как tru, либо как fls.

Это наблюдение является простым следствием мощного принципа параметричности (parametricity), который формализует единообразное поведение полиморфных программ. Параметричность была введена Рейнольдсом (Reynolds, 1974, Reynolds, 1983). В дальнейшем ее исследовали, наряду с родственными понятиями, Рейнольдс (Reynolds, 1984, Reynolds and Plotkin, 1993), Бейнбридж и др. (Bainbridge, Freyd, Scedrov, and Scott, 1990), Ма (Ma, 1992), Митчелл (Mitchell, 1986), Митчелл и Майер (Mitchell and Meyer, 1985), Хасегава (Hasegawa, 1991), Питтс (Pitts, 1987, Pitts, 1989, Pitts, 2000), Абади, Карделли, Куриен и Плоткин (Abadi, Cardelli, and Curien, 1993, Plotkin and Abadi, 1993, Plotkin, Abadi, and Cardelli, 1994), Уодлер (Wadler, 1989, Wadler, 2001) и другие. Описание основ можно найти у Уодлера (Wadler, 1989).

23.10  Импредикативность

Полиморфизм Системы F часто называют импредикативным (impredicative). В общем случае, определение (множества, типа и т. п.) называют <<импредикативным>>, если оно использует квантор, переменная которого может иметь значением сам определяемый объект. Например, в Системе F типовая переменная X в типе T = X.XX может иметь своим значением любой тип, включая и сам T (так что, например, можно конкретизировать тип T типом T и получить функцию из T в T). С другой стороны, полиморфизм в стиле ML часто называют предикативным (predicative) или слоистымstratified, поскольку значения типовых переменных ограничены монотипами, а те не содержат кванторов.

Термины <<предикативный>> и <<импредикативный>> происходят из логики. Куайн (Quine, 1987) проясняет их историю:

В переписке с Анри Пуанкаре …Рассел предложил приписать парадокс [Рассела] тому, что он назвал заблуждением порочного круга. <<Заблуждение>> состояло в том, что класс определялся условием принадлежности, которое прямо или косвенно ссылалось на набор классов, среди которых находился и сам определяемый класс. Например, условие принадлежности, лежащее в основе парадокса Рассела, — отсутствие самовключения: x не является членом x. Парадокс происходит оттого, что переменной x в условии принадлежности разрешено быть, среди прочего, тем самым классом, который определяется условием принадлежности. Рассел и Пуанкаре стали называть такое условие принадлежности импредикативным, и дисквалифицировали его в качестве средства указания класса. Таким образом, парадоксы теории множеств, Расселовский и другие, были лишены силы […].

Откуда же берутся термины <<предикативный>> и <<импредикативный>>? Рассел называет отброшенной банальностью о классах и условиях принадлежности к ним утверждение о том, что всякий предикат определяет класс; затем он приспосабливается к отказу от этой банальности, отказывая в звании предиката таким условиям принадлежности, которые более не рассматриваются как определяющие классы. Таким образом, определение <<предикативный>> не относилось ни к конкретному иерархическому подходу, ни к метафоре последовательного построения; это было просто конкретное предложение Рассела и Пуанкаре о том, какие условия принадлежности можно считать продуктивными при образовании классов, или <<предикативными>>. Однако вскоре ситуация перевернулась с ног на голову. Сегодня предикативная теория множеств — это конструктивная теория, а импредикативное определение понимается именно так, как объяснено в предыдущем абзаце, независимо от того, какие условия принадлежности мы предпочитаем рассматривать как определяющие классы.

23.11  Дополнительные замечания

Дополнительную библиографию по Системе F можно найти во вводной статье Рейнольдса (Reynolds, 1990) и в его же <<Теориях языков программирования>> (<<Theories of Programming Languages>>, Reynolds, 1998b).


1
На протяжении большей части этой главы изучается чистая Система F (рис. 23.1); в примерах из §23.4 используются расширения этой системы различными уже известными нам конструкциями. Соответствующая реализация на OCaml называется fullpoly. (Примеры с использованием пар и списков требуют интерпретатора fullomega.)
1
Аннотация as помогает программе проверки типов вывести тип nil в читаемом виде. Как мы видели в §11.4, все программы проверки типов из этой книги перед печатью типа проводят простую операцию <<схлопывания>> сокращений. Однако функция схлопывания недостаточно умна, чтобы справиться с такими <<параметрическими сокращениями>>, как List.
2
На самом деле, варианты Системы F с менее строгой операционной семантикой на основе полной бета-редукции обладают свойством сильной нормализации (strong normalization): гарантируется завершение любого пути нормализации, начинающегося с правильно типизированного терма.
3
В некоторых языках реализация с передачей типов диктуется наличием конструкций вроде приведения типов (casts) (§15.5). Как правило, высокопроизводительные реализации этих языков пытаются во время выполнения сохранять лишь минимальные остатки информации о типах, например, передавая типы только в полиморфные функции, в которых они действительно могут быть использованы.
4
Это связано с уже встречавшейся нам проблемой некорректного взаимодействия ссылок с полиморфизмом через let в стиле ML из §22.7. Обобщение (generalization) тела let в том примере здесь соответствует явной абстракции типа.
Упражнение 1   [★★]: Переведите опасный пример со с. ?? на язык Системы F с добавлением ссылок (рис. 13.1).
5
В отличие от этого решения, ограничение на значения (value restriction), введенное нами в §22.7 для сохранения корректности реконструкции типов в стиле ML при наличии побочных эффектов, стирает абстракции типов: обобщение типовой переменной, в сущности, противоположно стиранию абстракции типа. Корректность обеспечивается потому, что такие обобщения оказываются разрешены только там, где выводимая абстракция типа была бы непосредственно вложена в абстракцию терма или другой конструктор синтаксического значения, поскольку и то, и другое также останавливает вычисление.

Previous Up Next