Функциональное программирование. Основы (Файлы для подготовки к экзамену), страница 6

Будем использовать буквы α и β для типовых переменных, а σи τ — для произвольных типов. Теперь можно определить понятие замены типовой переменной в некотором типе на другой тип. Это в точностианалогично подстановке на уровне термов, и мы будем использовать туже нотацию. Например:(σ → bool)[σ := (σ → τ )] = (σ → τ ) → boolФормальное определение гораздо проще, чем для термов, поскольку намнет нужды беспокоится о связываниях переменных. В то же время удобно расширить его параллельными подстановками:αi [α1 := τ1 , . . .

, αk := τk ] = τiβ[α1 := τ1 , . . . , αk := τk ] = β, если αi 6= β для 1 ≤ i ≤ kCon (σ1 , . . . , σn )[θ] = Con (σ1 [θ], . . . , σn [θ])Для простоты, мы рассматриваем типовые константы как 0-арныеконструкторы, т. е. считаем, что int задается как int (). Имея определение подстановки, мы можем определить, что тип σ является более30общим, чем тип σ 0 и записывать этот факт как σ σ 0 . Это отношениевыполняется тогда и только тогда, когда существует набор подстановокθ такой, что σ 0 = σθ. Например:αα→αα → boolβ→αα→α6αβ→β(β → β) → boolα→β(β → β) → βТеперь можно сформулировать теорему:Теорема 4.

Каждый типизируемый терм имеет некоторый основнойтип, т. е. если T :: τ , то существует некоторый σ, такой что T :: σи для любого σ 0 , если T :: σ 0 , то σ σ 0 .Основной тип является единственным с точностью до переименований типовых переменных. Мы не будем приводить доказательство теоремы: оно не сложно, но довольно длинно. Важно понять, что доказательство конструктивно: оно дает конкретную процедуру для поиска основного типа. Эта процедура известна как алгоритм Хиндли–Милнера.

Всереализации языков программирования Haskell, ML и других, включаютв себя вариант этого алгоритма, так что выражения в них могут бытьсопоставлены их основному типу либо отвергнуты как нетипизируемые.6.3Сильная нормализацияВспомним наш пример терма без нормальной формы:(λx.y) ((λx.x x x) (λx.x x x))→ (λx.y) ((λx.x x x) (λx.x x x) (λx.x x x))→ (λx.y) ((λx.x x x) (λx.x x x) (λx.x x x) (λx.x x x))→ ...В типизированном лямбда-исчислении такого не может случиться, поскольку существует следующая теорема о сильной нормализации:Теорема 5.

Каждый типизируемый терм имеет нормальную формуи каждая возможная последовательность редукций, начинающаяся стипизируемого терма, завершается.31На первый взгляд, это хорошо — функциональная программа, соблюдающая дисциплину типизации может быть вычислена любым образом,и она всегда завершится в единственной нормальной форме (единственность следует из теоремы Черча–Россера, которая выполняется и длятипизированного лямбда-исчисления). Однако возможность писать незавершающиеся программы существенна для полноты по Тьюрингу, такчто мы больше не можем определять все вычислимые функции и дажевсе полные функции.Поскольку все определяемые функции полны, мы не можем делатьпроизвольные рекурсивные определения. Действительно, обычный комбинатор неподвижной точки должен быть нетипизируем; Y , λf.(λx.f (x x)) (λx.f (x x))не является правильно типизируемым выражением, поскольку он применяет x сам к себе и x связан.

Чтобы вернуть полноту по Тьюрингу,мы просто добавляем способ определения произвольных рекурсивныхфункций, которые являются правильно типизированными. Мы вводимполиморфный оператор рекурсии для всех типов вида:Rec :: ((σ → τ ) → (σ → τ )) → σ → τТакже вводится дополнительное правило редукции: для любого F ::(σ → τ ) → (σ → τ ) имеемRec F → F (Rec F )Теперь будем считать, что рекурсивные определения функций интерпретируются с использованием этих операторов рекурсии.7Отложенные вычисленияМы уже обсуждали, что с теоретической точки зрения, нормальныйпорядок редукции выражений наиболее предпочтителен, поскольку еслилюбая стратегия завершается, завершится и она. Такая стратегия известна и в традиционных языках программирования (в Алголе 60 ееназывают вызовом по имени, по таким же правилам «вызываются» параметризованные макроопределения в языке Си.) Однако с практическойточки зрения такая стратегия имеет существенные недостатки.

Для примера рассмотрим выражение(λx.x + x + x) (10 + 5)Нормальная редукция сводит это выражение к следующему:(10 + 5) + (10 + 5) + (10 + 5)32Таким образом, необходимо трижды вычислять значение одного и тогоже выражения. На практике это, разумеется, недопустимо. Существуютдва основных решения этой проблемы и они разделяют мир функционального программирования на два лагеря.В первом подходе отказываются от нормальной стратегии и вычисляют аргументы функций до того, как передать их значения в функцию.Это — обычная практика в таких языках, как Си, Паскаль и т.

д. Такой подход называют передачей по значению. При этом вычислениенекоторых выражений, завершающееся при нормальной стратегии, может привести к бесконечной последовательности редукций. Однако напрактике этих случаев можно легко избежать. Обычно такая стратегияпозволяет получать довольно эффективный машинный код. Также онапредпочтительна в случае гибридных языков, т. е. функциональных языков, содержащих императивные конструкции (присваивания, циклы и т.п.) Языки семейства ML придерживаются такого порядка вычислений.При другом подходе, использующемся в Haskell и некоторых других языках, нормальная стратегия редукций сохраняется.

Однако приэтом различные возникающие подвыражения разделяются и никогда невычисляются более одного раза. Во внутреннем представлении выражения становятся не деревьями, а направленными ациклическими графами.Такая дисциплина вызова называется ленивой или вызовом по необходимости, поскольку выражения вычисляются только тогда, когда ихзначения действительно необходимы для работы программы.Например, в языке Haskell можно сделать следующее определение:bottom = bottomСогласно этому определению, вычисление выражения bottom никогдане завершиться. Однако рассмотрим такую функцию:const1 x = 1Тогда значение выражения const1 bottom равно 1.

Поскольку функция const1 не нуждается в значении своего аргумента, он не вычисляется. Аналогичная ситуация и со следующим выражением:const1 (1/0)Значение этого выражения также равно 1. Деления на 0 не происходит,поскольку аргумент функции никогда не вычисляется.Преимуществом такого подхода является то, что он позволяет добиваться большей выразительности при записи функций. Платой за этоявляется сложность реализации и некоторое снижение эффективности.33Действительно, вместо того, чтобы непосредственно вычислить выражение, приходится сохранять информацию о том, как его вычислять.

Разумеется, если значение этого выражения не понадобилось в дальнейшихвычислениях, мы получаем некоторую экономию, однако в противномслучае непосредственное вычисление кажется предпочтительным. Оптимизирующие компиляторы языка Haskell во многих случаях могут самивыявить места программы, в которых можно обойтись без отложенныхвычислений.Конструкторы данных в Haskell также являются функциями (единственное отличие от «настоящих» функций заключается в том, что ихможно использовать в шаблонах при сопоставлении с образцом.) В сочетании с «ленивым» вызовом это позволяет определять бесконечныеструктуры данных. Например, следующее определение задает бесконечный список единиц:ones = 1 : onesБолее интересным примером служит бесконечный список целых чисел,начиная с числа n:numsFrom n = n : numsFrom (n+1)Термин «бесконечный» здесь — не преувеличение.

Определения, подобные приведенным, действительно задают потенциально бесконечныеструктуры данных. С ними можно работать так же, как и с конечными, например, получить (бесконечный) список квадратов натуральныхчисел:squares = map (^2) (numsFrom 1)Разумеется, в реальности мы работаем только с конечной частью нашего списка, однако использование отложенных вычислений позволяетотделить генерацию бесконечной структуры данных от выделения ее конечной части. Для наших примеров конечную часть списка можно выделить, например, с помощью функции take, которая по заданному числуn и списку возвращает первые n элементов этого списка.

Так, значениевыраженияtake 5 (numsFrom 1)равно [1,2,3,4,5], а результатом вычисленияtake 5 squares34будет [1,4,9,16,25]Представленный пример дает образец типичной структуры программы, использующейся в Haskell. Программа представляется в виде конструкции g (f input), где g и f — некоторые функции. Они выполняются вместе строго синхронно. f запускается только тогда, когда gпытается прочитать некоторый ввод, и выполняется ровно столько, чтобы предоставить данные, который пытается читать g.

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

Ленивые вычисления, возможно, наиболее мощный инструментдля модуляризации в наборе функционального программиста.Мы проиллюстрируем мощь ленивых вычислений, программируя некоторые численные алгоритмы. Прежде всего, рассмотрим алгоритм Ньютона–Рафсона для вычисления квадратного корня. Этот алгоритм вычисляет квадратный корень числа z, начиная с начального приближенияa0 . Он уточняет это значение на каждом последующем шаге, используяправило:an+1 = (an + z/an )/2Если приближения сходятся к√ некоторому пределу a, то a = (a +z/a)/2 , то есть a · a = z или a = z.Фактически сведение к пределу проходит быстро. Программа проводит проверку на точность (eps) и останавливается, когда два последовательных приближения отличаются меньше чем на eps.

При императивном подходе алгоритм обычно программируется следующим образом:x = a0;do{y = x;35x = (x + z/x) / 2;} while (abs(x-y) < eps)// теперь x = квадратному корню из zЭта программа неделима на обычных языках. Мы выразим её в более модульной форме, используя ленивые вычисления, и затем покажемнекоторые другие применения полученным частям.Так как алгоритм Ньютона–Рафсона вычисляет последовательностьприближений, естественно представить это в программе явно спискомприближений. Каждое приближение получено из предыдущего функциейnext z x = (x + z/x) / 2То есть (next z) — функция, отображающая каждое приближениев следующее. Обозначим эту функцию f, тогда последовательность приближений будет: [a0, f a0, f(f a0), f(f(f a0)),...] .