John Harrison - Введение в функциональное программирование (1108517), страница 11
Текст из файла (страница 11)
Подобная интерпретация незадаёт никаких ограничений ни на способ вычисления выражений, ни даженаправление, в котором уравнения будут использоваться. Благодаря этому,функциональный подход к программированию часто называют декларативнымнаряду с логическим (примером последнего служит язык PROLOG).6 В рамкахтакого подхода программа не содержит явных инструкций, а лишь объявляетнекоторые свойства соответствующих понятий, оставляя подробности своеговыполнения компьютеру.В то же время, программа бесполезна или, по крайней мере, неоднозначна,если для неё не определены некоторые содержательные действия компьютера.Следовательно, требуется понимание того, что внешне полностью декларативнаяпрограмма должна быть выполнена неким определённым образом.
В самомделе, вычисление выражения начинается с раскрытия всех входящих в негоимён определений (т. е. уравнения интерпретируются слева направо), после чегопроизводится последовательность β-преобразований. Это значит, что несмотряна отсутствие процедурной информации в программе, неявно подразумеваетсяналичие некоторой конкретной стратегии выполнения. Таким образом, понятие«декларативности» относится в большей степени к восприятию программ человеком.Кроме того, должны существовать определённые правила, касающиеся стратегииредукции, поскольку выбор различных β-редексов, как мы знаем, может оказатьрешающее влияние на завершимость.
Как следствие, полностью определённый языкпрограммирования из лямбда-исчисления получается лишь тогда, когда мы зададимэту стратегию. В дальнейшем мы увидим, какие решения были приняты в ходепроектирования различных функциональных языков, но перед этим нам придётсяпрервать наше изложение и обсудить введение понятия типа.6По всей видимости, Лэндин предпочитал термин «денотационный».353.5. Дополнительная литератураГлава 3. Лямбда-исчисление как язык программирования3.5Дополнительная литератураМногие из упомянутых стандартных работ включают в себя подробный анализвопросов, затронутых в этом разделе.
В частности, в работе Gordon (1988) даётсястрогое доказательство Тьюринг-полноты лямбда-исчисления, а также того, чтозадача проверки существования нормальной формы терма (аналог «проблемыостанова» в лямбда-исчислении) алгоритмически неразрешим. Влияние лямбдаисчисления на полноценные языки программирования, а также на эволюциюфункциональных языков в частности обсуждается в работе Hudak (1989).Упражнения1. Дайте обоснование «обобщенного β-преобразования», т.
е. докажите, что(λ(x1 , . . . , xn ). t[x1 , . . . , xn ])(t1 , . . . , tn ) = t[t1 , . . . , tn ]42. Пусть f ◦ g = λx. f (g x). Приняв во внимание, что I = λx. x, докажите,что CURRY ◦ UNCURRY = I. Верно ли также, что UNCURRY ◦ CURRY = I?3. Какие арифметические операции соответствует заданным на множественумералов Чёрча функциям λn f x.
f (n f x) и λm n. n m?4. (Клоп) Докажите, что следующее выражение представляет собой комбинаторнеподвижной точки:££££££££££££££££££££££££££,где4£ = λabcdef ghijklmnopqstuvwxyzr. r(thisisaf ixedpointcombinator)5. Дайте рекурсивное определение операции вычитания натуральных чисел.6. Пусть задано следующее представление списков Mairson (1991):nilconsheadtailappendappend_listsmaplengthtackreversefilter===========λc n. nλx l c n. c x (l c n)λl. l(λx y. x) nilλl. snd (l(λx p. (cons x (fst p), fst p)) (nil, nil))λl1 l2 . l1 cons l2λL.
L append nilλf l. l (λx. cons (f x)) nilλl. l(λx. SUC)0λx l. l cons (cons x nil)λl. l tack nilλl test. l (λx. (test x)(cons x)(λy. y)) nilПочему автор этого представления Мэйрсон назвал его «списками Чёрча»?Каково назначение каждой из приведённых функций?36Глава 4ТипыТипы представляют собой удобное средство определения различныхразновидностей данных, наподобие логических и целочисленных значений либофункций. Благодаря типизации оказывается возможным гарантировать соблюдениеограничений, порождаемых этими различиями (например, что функция недолжна применяться к аргументам с неподходящими типами).
Что побуждаетнас ввести понятие типа в лямбда-исчисление и языки программирования наего основе? Основания для такого решения можно найти как в логике, так и впрограммировании.С точки зрения логики, требуется преодолеть парадокс Рассела, которыйпрепятствует попыткам построить непротиворечивое расширение лямбдаисчисления теорией множеств. Источником противоречий служит необычнаяциклическая природа используемого при этом приёма — применение функции ксамой себе. Более того, если бы даже и не требовалось избежать парадокса, всё равновозникает интуитивное ощущение неясности формальной системы, в рамках которойразрешены подобные действия. Безусловно, самоприменение таких функций, кактождественная функция (λx. x) и функция-константа (λx.
y), выглядит безобидно.В то же время, очевидна и потребность в более ясном описании того, какие именносемейства функций представимы в терминах лямбда-исчисления при условии, чтонам точно известны области определения и значений этих функций, а также то, чтомы их применяем лишь к аргументам, принадлежащим соответствующим областямопределения.
Введение Расселом типов в своей работе Principia Mathematica былопродиктовано приведёнными соображениями.Ещё одной причиной, которая побуждает нас подробно рассмотреть возможностьрасширения лямбда-исчисления понятием типа, является применение типизациив других языках программирования. Понятие типов данных встречается уже вязыке FORTRAN, в котором различаются целые числа и числа с плавающейточкой.
Причины появления типов в данном контексте не были связаны сизложенными ранее аргументами из области логики. Одной из таких причин была,очевидно, эффективность порождаемого компилятором кода. Наличие информациио допустимых способах использования той или иной переменной позволяет какгенерировать более эффективный код, так и рациональнее распределять память.Например, реализация адресной арифметики в духе языка C должна учитыватьразмер объектов, к которым происходит обращение.
Если p представляет собойуказатель на объект размером 4 байта, то выражение p + 1 при трансляции в37Глава 4. Типымашинный код на архитектурах с побайтовой адресацией памяти превращаетсяв p + 4. Предшественник C, язык BCPL, был бестиповым, и в нём не делалосьразличий между целыми числами и указателями. Как следствие, соответствующиемасштабирующие множители в каждой операции адресной арифметики задавалисьв программе явным образом, создавая тем самым существенные неудобства.Дальнейшее развитие привело к тому, что типизация, оставаясь важнымсредством повышения эффективности, стала приобретать всё большее значениекак инструмент ограниченной статической проверки корректности программ.Существенная доля ошибок, от очевидных опечаток до серьёзных концептуальныхпросчётов, проявляет себя нарушением правил типизации, благодаря чему этиошибки могут быть выявлены непосредственно в ходе компиляции без запускапрограммы на исполнение.
Более того, в ходе чтения исходных текстов типызачастую играют роль документации. Наконец, типы данных могут применятьсядля улучшения модульности программ и скрытия информации при помощи такихопределений различных структур данных, которые явно разделены на интерфейс иподробности реализации.В то же время некоторые программисты выступают против использованиятипов, полагая, что для их стиля программирования ограничения, накладываемыетипизацией, являются излишне утомительными. Как следствие, различается иуровень её поддержки языками программирования. Существуют бестиповые языки,как императивные (BCPL), так и функциональные (ISWIM, SASL и Erlang???).
Другие, подобно PL/I, имеют лишь слабую типизацию, которая допускаетнекоторые варианты совместного использования данных различных типов припомощи автоматических преобразований, реализуемых компилятором. Наконец,некоторые языки, такие как Lisp, осуществляют динамический контроль типовво время исполнения программы. Этот подход может, в принципе, существенноухудшить производительность, поскольку требует дополнительных вычислительныхресурсов, подобно тому, как это происходит с другим известным источникомнакладных расходов — проверкой корректности обращений к массивам.
Статическаяже типизация, напротив, может существенно снизить издержки.1На практике важность тех или иных ограничений типизации существеннозависит от характера решаемых задач и стиля программирования. Разработкасистемы типов, обеспечивающей как возможность содержательного статическогоконтроля, так и достаточный уровень гибкости, остаётся предметом активныхисследований. Типизация, реализованная в языке ML, представляет собой важноедостижение, поскольку в ней допускается полиморфизм, благодаря которому одна ита же функция может применяться к аргументам различных типов.
Такой подходсохраняет все выгоды сильной статической типизации, дополняя их некоторымивозможностями, присущими слабому или динамическому контролю типов2 . Болеетого, программист как правило не обязан указывать типы явно — транслятор MLспособен самостоятельно вывести наиболее общий тип каждого выражения, отвергаяте из них, которые не поддаются типизации. Роль полиморфизма в процессе выводатипов будет рассмотрена далее. Таким образом, несомненно, что система типовязыка ML делает его подходящим инструментом для широкого класса задач. Тем1Одним из направлений развития динамической типизации является её дополнение элементамистатической, что зачастую позволяет добиться сравнимой эффективности.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
