Пирс Б. Типы в языках программирования

Подождите немного. Документ загружается.

Глава 7

Реализация лямбда-исчисления на ML

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

на интерпретаторе для арифметических выражений из Главы 4, а также на подходе к связыванию

переменных и к подстановке из Главы 6.

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

вода на OCaml определений из предыдущих глав. Как и в Главе 4, мы демонстрируем только базовые

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

детали.

7.1. Термы и контексты

Тип данных, представляющий абстрактные синтаксические деревья для термов, можно получить

путем прямого перевода Определения 6.1.2:

type term =

TmVar of int

| TmAbs of term

| TmApp of term * term

Представлением переменной является число — это индекс де Брауна. Представление абстракции содер-

жит только терм для тела абстракции. Применение содержит два терма, один из которых применяется

к другому.

Определение, которое реально используется в нашем интерпретаторе, впрочем, содержит несколько

больше информации. Во-первых, как и раньше, полезно каждый терм снабдить элементом типа info,

где записано, из какой позиции в файле терм был считан, чтобы программы распечатки ошибок могли

направить пользователя (или даже пользовательский текстовый редактор, автоматически) к точному

месту, где произошла ошибка.

type term =

TmVar of info * int

| TmAbs of info * term

| TmApp of info * term * term

Во-вторых, для целей отладки, полезно хранить в каждой вершине-переменной дполнительное число,

для проверки целостности. Соглашение будет такое: в этом втором числовом поле всегда содержится

полная длина контекста, где встретилась эта переменная.

type term =

TmVar of info * int * int

| TmAbs of info * term

| TmApp of info * term * term

В основном в этой главе обсуждается чистое бестиповое лямбда-исчисление (Рис. 5.3). Соответствующий интерпре-

татор называется untyped. Интерпретатор fulluntyped включает расширения, а именно поддержку чисел и булевских

значений.

72 7.1. Термы и контексты

Каждый раз при распечатке переменной мы будем проверять, что это число совпадает с реальной

длиной контекста, где мы находимся; если это не так, значит, где-то мы забыли добавить операцию

сдвига.

Последнее улучшение тоже относится к распечатке. Несмотря на то, что внутри термы представля-

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

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

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

однако проделывать это совсем наивным образом не стоит (скажем, порождая для всех переменных

совершенно новые имена), поскольку тогда имена связанных переменных в печатаемых термах будет

никак не связан с именами из исходной программы. Можно справиться с этой трудностью, если хранить

при каждой абстракции строку-подсказку об имени связанной переменной.

type term =

TmVar of info * int * int

| TmAbs of info * st ring * term

| TmApp of info * term * term

Основная работа с термами (в частности, подстановка) ничего интересного с этими строками проде-

лывать не будет: они просто переносятся в результат в исходной форме, безо всякой заботы о совпа-

дении имен, захвате переменных, и т. д. Когда программе распечатки требуется породить новое имя

для связанной переменной, она сначала пытается использовать подсказку; если окажется, что это имя

противоречит какому-либо имени, уже используемому в текущем контексте, процедура распечатки пы-

тается породить похожее имя, добавляя штрихи, пока, в конце концов, не найдется имя, которое в

текущем контексте никто не использовал. Такое правило обеспечивает, что напечатанный терм будет

всегда очень похож на то, чего ожидает пользователь, с точностью до нескольких штрихов.

Сама процедура печати выглядит так:

let rec printt m ctx t = match t with

TmAbs ( fi ,x , t1 ) ->

let ( ctx ’,x ’) = p i c k f r e s h n a m e ctx x in

pr " ( lambda ␣"; pr x ’; pr ". ␣ "; printt m ctx ’ t1 ; pr ")"

| TmApp ( fi , t1 , t2 ) ->

pr " ( "; printtm ctx t1 ; pr " ␣"; pr inttm ctx t2 ; pr ")"

| TmVar ( fi , x ,n) ->

if ctxlength ctx = n then

pr ( i n d e x2name fi ctx x)

else

pr " [ bad ␣ index ]"

В ней используется тип данных context,

type contex t = ( string * binding ) list

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

вания совершенно тривиальны

type bindin g = NameB ind

и не несут никакой дополнительной информации. Однако позднее (в Главе 10) мы введем другие вари-

анты в определение типа binding, и они будут отслеживать сведения о типе, связанном с переменной,

и другую подобную информацию.

Процедура распечатки зависит также от нескольких низкоуровневых функций: pr выдает строку в

стандартный поток вывода; ctxlength возвращает длину контекста; index2name находит строковое имя

переменной по ее индексу. Самая интересная из этих функций, pickfreshname, принимает контекст ctx

и имя-подсказку x, находит имя x’, похожее на x и не встречающееся в ctx, добавляет x’ к контексту

ctx, получая при этом новый контекст ctx’, и возвращает пару, состоящую из x’ и ctx’.

Настоящая процедура печати в интерпретаторе untyped с веб-сайта книги выглядит несколько слож-

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

печатать скобки, следуя соглашению, что применение право-ассоциативно, а тела абстракций простира-

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

rev. 104

7.2. Сдвиг и подстановка 73

модуля красивой печати (OCaml-овской библиотеки Format), который принимает решения о переводах

строк и отступах.

7.2. Сдвиг и подстановка

Определение сдвига (6.2.1) переводится на OCaml чуть ли не посимвольно.

let termShift d t =

let rec walk c t = match t with

TmVar ( fi ,x ,n ) -> if x >= c then TmVar ( fi , x+d ,n + d )

else TmVar (fi ,x ,n+d )

| TmAbs ( fi , x , t1 ) -> TmAbs (fi , x , walk (c +1) t1 )

| TmApp ( fi , t1 , t2 ) -> TmApp ( fi , walk c t1 , walk c t2 )

in walk 0 t

Внутренний сдвиг

t здесь представлен вызовом внутренней функции walk c t. Поскольку d не

меняется, нет нужды передавать ее в каждый вызов walk: когда нам это требуется в варианте с пе-

ременной внутри walk, мы просто используем внешнее связывание d. Сдвиг верхнего уровня

представляется выражением termShift d t. (Заметим, что сама функция termShift не помечена как

рекурсивная, поскольку единственное, что она делает — вызывает один раз walk.)

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

let termSubst j s t =

let rec walk c t = match t with

TmVar ( fi ,x ,n ) -> if x=j + c then term S h ift c s else TmVar (fi ,x , n)

| TmAbs ( fi , x , t1 ) -> TmAbs (fi , x , walk (c +1) t1 )

| TmApp ( fi , t1 , t2 ) -> TmApp ( fi , walk c t1 , walk c t2 )

in walk 0 t

Подстановка j s t терма s вместо переменной с номером j в терме t записывается здесь как

termSubst j s t. Единственное отличие от исходного определения подстановки состоит в том, что

весь сдвиг s мы производим сразу, в ветви TmVar, вместо того, чтобы сдвигать s на единицу каждый

раз, когда проходим через связывание. При этом получается, что аргумент j во всех вызовах walk один

и тот же, и мы можем опустить его во внутреннем определении.

Читатель может заметить, что определения termShift и termSubst весьма похожи, и отличаются

только действием, производимым, когда процесс достигает переменной. Интерпретатор untyped, до-

ступный на веб-сайте книги, использует эту похожесть и выражает как сдвиг, так и подстановку в

качестве частных случаев более общей функции tmmap. Принимая терм t и функцию onvar, onmap

выдает терм той же формы, что t, только каждая переменная заменяется результатом вызова onvar

от этой переменной. Такой трюк в более крупных исчислениях избавляет нас от довольно большого

количества повторений; подробности можно найти в §25.2.

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

— правило бета-редукции. Как мы уже замечали, это правило на самом деле проводит несколько опе-

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

результат сдвигается на единицу вниз, чтобы отразить исчезновение использованной связанной пере-

менной. Следующее определение описывает эту последовательность действий:

let t e r m S u b s t T o p s t =

ter m S hift ( -1) ( t ermSubst 0 ( termS h ift 1 s) t)

7.3. Вычисление

Как и в Главе 4, функция вычисления зависит от вспомогательного предиката isval:

let rec isval ctx t = match t with

TmAbs (_ ,_ ,_ ) -> true

| _ -> false

rev. 104

74 7.4. Дополнительные замечания

Функция одношагового вычисления прямо кодирует правила вычисления, но при этом, помимо терма,

принимает дополнительным аргументом контекст ctx. В нашей теперешней функции eval1 этот кон-

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

обращаться.

let rec eval1 ctx t = match t with

TmApp ( fi , TmAbs (_ ,x , t12 ) , v2 ) when isval ctx v2 ->

termSubstTop v2 t12

| TmApp ( fi , v1 , t2 ) when isval ctx v1 ->

let t2 ’ = eval1 ctx t2 in

TmApp ( fi , v1 , t2 ’)

| TmApp ( fi , t1 , t2 ) ->

let t1 ’ = eval1 ctx t1 in

TmApp ( fi , t1 ’, t2 )

| _ ->

raise NoRuleApplies

Функция многошагового вычисления такая же, как раньше, за исключением аргумента ctx:

let rec eval ctx t =

try let t ’ = eval1 ctx t

in eval ctx t ’

with N o R u l e A p p l ie s -> t

Упражнение 7.3.1 Рекомендуется, : Измените реализацию, чтобы она использовала стиль

вычисления с «большим шагом», введенный в Упражнении 3.5.17.

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

Реализация подстановок, представленная в этой главе, хотя и достаточна для целей нашей кни-

ги, но далека от идеала. В частности, правило бета-редукции в нашем интерпретаторе «энергично»

подставляет значение аргумента вместо связанной переменной в теле процедуры. Интерпретаторы (и

компиляторы) функциональных языков, где оптимизируется скорость, а не простота чтения кода, ис-

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

информацию о связи между именем переменной и значением аргумента во вспомогательной структуре

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

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

если рассматривать окружение как своего рода явную подстановку — т. е., перевести механизм подста-

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

вычислитель, а не внешней операцией на термах. Явные подстановки появились в исследовании Абади,

Карделли, Куриена и Леви (Abadi, Cardelli, Curien and L´evy 1991a) и стали с тех пор активной областью

исследований.

Если Вы что-то реализовали в

программе, это еще не значит,

что Вы это поняли.

Брайан Кантвелл Смит

rev. 104

Часть II

Простые типы

Глава 8

Типизированные арифметические

выражения

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

вали основные инструменты для точного описания синтаксиса и вычислений. Теперь мы возвращаемся

к этому языку и дополняем его статическими типами. Подобно Главе 3, сама по себе система типов

совершенно тривиальна, однако она поможет нам познакомиться с понятиями, которые затем будут

использоваться на протяжении всей книги.

8.1. Типы

Напомним синтаксис арифметических выражений:

t ::= термы:

true константа «истина»

false константа «ложь»

if t then t else t условное выражение

0 константа «ноль»

succ t следующее число

pred t предыдущее число

iszero t проверка на ноль

В Главе 3 мы видели, что при вычислении терма может либо получиться значение. . .

v ::= . . . значения:

true константа «истина»

false константа «ложь»

nv числовое значение

nv ::= . . . числовые значения:

0 константа ноль

succ nv значение-последователь

либо вычисление может на каком-то шаге зайти в тупик, наткнувшись на терм вроде pred false, к

которому не применимы никакие правила.

Тупиковые термы соответствуют бессмысленным или ошибочным программам. Следовательно, по-

лезно было бы уметь определять, не вычисляя сам терм, что его вычисление наверняка не попадет

в тупик. Для этого нам придется отличать термы, чье значение будет числовым (поскольку только

эти термы должны использоваться как аргументы pred, succ и iszero) от тех, чье значение будет бу-

левским (поскольку только эти термы должны служить условием в условном выражении). Для такой

классификации термов мы вводим два типа, Nat и Bool. На протяжении всей книги метапеременные S,

Система, изучаемая в этой главе — типизированное исчисление булевских значений и чисел (Рис. 8.2). Соответству-

ющий интерпретатор на OCaml называется tyarith.

78 8.2. Отношение типизации

B (типизированное) Расширяет B (3.1)

Новые синтаксические формы:

T ::= типы:

Bool тип булевских значений

Новые правила типизации: t : T

true : Bool

(T-True)

false : Bool

(T-False)

: Bool t

: T t

: T

if t

then t

else t

: T

(T-If)

Рис. 8.1. Правила типизации для булевских значений (B).

BN (типизированное) Расширяет NB (3.2) и 8.1

Новые синтаксические формы:

T ::= . . . типы:

Nat тип натуральных чисел

Новые правила типизации: t : T

0 : Nat

(T-Zero)

: Nat

succ t

: Nat

(T-Succ)

: Nat

pred t

: Nat

(T-Pred)

: Nat

iszero t

: Bool

(T-IsZero)

Рис. 8.2. Правила типизации для чисел (NB).

T, U и т. п. будут обозначать типы.

Утверждение «терм t имеет тип T» (или «t принадлежит типу T», или «t является элементом

T») означает, что t «очевидным образом» дает при вычислении значение нужного вида — при этом

под словами «очевидным образом» мы подразумеваем, что проверить это можно статически, не про-

изводя само вычисление t. Например, терм if true then false else true имеет тип Bool, а pred

(succ (pred (succ 0))) имеет тип Nat. Однако наш анализ типов будет консервативен, то есть будет

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

ли термы вроде if (iszero 0) then 0 else false, или даже if true then 0 else false какой-либо

тип, даже при том, что их вычисление на самом деле в тупик не заходит.

8.2. Отношение типизации

Отношение типизации для арифметических выражений, записываемое

«t : T», определяется на-

бором правил вывода, присваивающих термам типы. Эти правила перечислены на Рис. 8.1 и 8.2. Как

и в Главе 3, мы помещаем правила для булевских значений и для чисел на два различных рисунка,

поскольку впоследствии нам иногда будет нужно ссылаться на них по отдельности.

Правила T-True и T-False на Рис. 8.1 присваивают тип Bool булевским константам true и false.

Правило T-If присваивает тип условному выражению на основании типов его подвыражений: условие

должно при вычислении давать булевское значение, а t

и t

должны давать значения одного и того

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

if — тип ветвей then и else, и что тип этот может быть любым (либо Nat, либо Bool, либо, когда мы

доберемся до исчислений с более интересными наборами типов, любой другой тип).

Часто вместо : используется символ .

rev. 104

8.2. Отношение типизации 79

Правила для чисел на Рис. 8.2 имеют подобный же вид. T-Zero присваивает тип Nat константе 0.

T-Succ присваивает тип Nat выражению succ t

при условии, что t

имеет тип Nat. Точно так же,

T-Pred и T-IsZero говорят, что pred дает в результате Nat, если его аргумент имеет тип Nat, а iszero

дает Bool при аргументе типа Nat.

Определение 8.2.1 Формально, отношение типизации для арифметических выражений — это наи-

меньшее бинарное отношение между термами и типами, удовлетворяющее всем правилам с Рис. 8.1

и 8.2. Терм t типизируем, если существует тип T, такой, что t : T.

В рассуждениях о типизации мы часто будем делать утверждения вроде «Если терм вида succ t

имеет какой-нибудь тип, то это должен быть тип Nat». Следующая лемма дает нам набор утверждений

такого вида. Каждое из них немедленно следует из формы соответствующего правила типизации.

Лемма 8.2.2 Обращение отношения типизации :

1. Если true : R, то R Bool.

2. Если false : R, то R Bool.

3. Если if t

then t

else t

: R, то t

: Bool, t

: R и t

: R.

4. Если 0 : R, то R Nat.

5. Если succ t

: R, то R Nat и t

: Nat.

6. Если pred t

: R, то R Nat и t

: Nat.

7. Если iszero t

: R, то R Bool и t

: Nat.

Доказательство: Непосредственно следует из определения отношения типизации.

Лемму об обращении типизации часто называют леммой о порождении для отношения типизации,

поскольку она позволяет, имея верное утверждение о типе терма, понять, как можно породить дока-

зательство этого утверждения. Лемма об обращении немедленно приводит к рекурсивному алгоритму,

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

вычислить его тип (если таковой имеется), исходя из типов его подтермов. Мы подробно рассмотрим

это утверждение в Главе 9.

Упражнение 8.2.3 : Докажите, что у типизируемого терма все подтермы также типизируе-

мы.

В §3.5 мы познакомились с понятием деревьев вывода для вычислений. Подобным образом, дере-

во вывода типов представляет собой дерево, состоящее из экземпляров правил типизации. Каждая

пара t, T в отношении типизации основывается на дереве вывода типов с заключением t : T. Вот,

например, дерево вывода для утверждения типизации «if iszero 0 then 0 else pred 0 : Nat»:

0 : Nat

T-Zero

iszero 0 : Bool

T-IsZero

0 : Nat

T-Zero

0 : Nat

T-Zero

pred 0 : Nat

T-Pred

if iszero 0 then 0 else pred 0 : Nat

T-If

Иначе говоря, утверждения — это формальные высказывания о типах в программах, правила типи-

зации — это зависимости между утверждениями, а деревья вывода — это доказательства, построенные

с помощью правил типизации.

Теорема 8.2.4 Единственность типов : Всякий терм t имеет не более одного типа. То есть, если

t типизируем, то у него только один тип. Более того, есть только один способ вывести этот тип

с помощью правил Рис. 8.1 и 8.2.

Доказательство: Прямолинейная структурная индукция по t. В каждом варианте используется

соответствующее утверждение леммы обращения и предположение индукции.

rev. 104

80 8.3. Безопасность = продвижение + сохранение

В простой системе типов, с которой мы работаем в этй главе, у каждого терма только один тип (если

тип у него вообще есть), и для подтверждения этого всегда есть ровно одно дерево вывода. Позже —

скажем, когда мы доберемся до систем типов с наследованием в Главе 15, — оба этих свойства будут

ослаблены: один терм может иметь несколько типов, и в общем случае может быть несколько способов

доказать утверждение, что данный терм имеет данный тип.

Свойства отношения типизации часто будут доказываться при помощи индукции на деревьях вы-

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

вывода вычисления. Начиная со следующего раздела, мы встретим много примеров индукции на дере-

вьях вывода типов.

8.3. Безопасность = продвижение + сохранение

Самое главное свойство нашей системы типов, как и любой другой — безопасность (также назы-

ваеемая корректность): правильно типизированные термы «никогда не ломаются». Мы уже решили,

что значит для терма сломаться: это значит оказаться в «тупиковом состоянии» (Определение 3.5.15),

когда терм не является значением, но правила вычисления ничего не говорят о том, что делать с ним

дальше. Следовательно, мы хотим знать, что правильно типизированные термы никогда не оказыва-

ются в тупике. Мы доказываем это в два шага, традиционно называемые теоремами продвижения и

сохранения.

Продвижение: Правильно типизированный терм не может быть тупиковым (либо это

значение, либо он может проделать шаг в соответствии с правилами вычисления).

Сохранение: Если правильно типизированный терм проделывает шаг вычисления, полу-

чающийся терм также правильно типизирован.

Вместе эти два свойства гарантируют, что правильно типизированный терм никогда при вычислении

не попадет в тупик.

Для доказательства теоремы о продвижении удобно записать несколько утверждений о возможном

виде канонических форм типов Bool и Nat (т. е., правильно типизированных значениях этих типов).

Лемма 8.3.1 Канонические формы :

1. Если v — значение типа Bool, то v равен либо true, либо false.

2. Если v — значение типа Nat, то v является числовым значением согласно грамматике на

Рис. 3.2.

Доказательство: Часть (1): согласно грамматике на Рис. 3.1 и 3.2, значения в этом языке могут

иметь четыре формы: true, false, 0 и succ nv, где nv — числовое значение. Первые два варианта

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

по предположению, имеет тип Bool, а пункты 4 и 5 леммы об обращении говорят нам, что 0 и succ

nv могут иметь только тип Nat, а не Bool. Часть (2) доказывается так же.

Теорема 8.3.2 Продвижение : Допустим, t — правильно типизированный терм (то есть, t : T

для какого-то типа T). Тогда либо t является значением, либо существует некоторый t , такой,

что t t .

Доказательство: Индукция по дереву вывода t : T. Варианты T-True, T-False и T-Zero дают

требуемый результат немедленно, так как в этих случаях t — значение. В остальных случаях мы

рассуждаем так:

Вариант T-If: t if t

then t

else t

: Bool t

: T t

: T

Согласно предположению индукции, либо t

является значением, либо существует терм t

, такой,

Лозунг «безопасность — это продвижение плюс сохранение» (с использованием леммы о канонических формах) был

выдвинут Харпером; вариант того же лозунга был предложен Райтом и Феллейсеном (Wright and Felleisen 1994).

В большинстве рассматриваемых нами систем, вычисление сохраняет не только типизируемость, но и сам тип термов.

Однако в некоторых системах тип при вычислении может меняться. Например, в системах с наследованием типы могут

становиться меньше (более информативными) в процессе вычисления.

rev. 104