John Harrison - Введение в функциональное программирование (1108517), страница 4
Текст из файла (страница 4)
Такое подобие помогает избегать дублирования и увеличивает элегантность.51.2. ПланГлава 1. Введениемы выбрали другой подход – мы начнём с λ-исчисления, и покажем как оно можетбыть использовано в роли теоретической основы функциональных языков. Такойподход обладает тем достоинством, что он хорошо соответствует реальной историиразработки функциональных языков.Следовательно, сначала мы введём λ-исчисление, и покажем как оно,первоначально предназначенное на роль формальной логической основыматематики, превратилось в полноценный язык программирования. Затем мыобсудим, зачем мы хотим добавить типы в λ-исчисление, и покажем, как добитьсятребуемого. Это приведёт нас к языку ML, который по существу являетсяоптимизированной реализацией типизированного λ-исчисления с определённойстратегией вычисления выражений. Мы рассмотрим практические основыфункционального программирования на ML, обсудим полиморфизм и понятиенаиболее общего типа данных.
Затем мы перейдём к более сложным темам, такимкак исключения и императивные возможности ML. В заключение, мы приведёмнесколько реальных примеров, которые, как мы надеемся, подтвердят мощь ML.Дополнительная литератураМножество книг о «функциональном программировании» включают в себяобщее введение и описание отличий от императивного программирования —просмотрите несколько и выберите ту, которая вам нравится. Например, Henson (1987) предлагает хорошее вводное обсуждение и содержит такую же смесьтеории и практики, как и в этом тексте. Детальная и спорная пропагандафункционального стиля программирования приведена в работе создателя FORTRANДжона Бэкуса Backus (1978).
Работа Gordon (1994) обсуждает проблемы введенияввода-вывода в функциональные языки, а также приводит некоторые решения.Читатели, заинтересовавшиеся денотационной семантикой для императивных ифункциональных языков, могут прочитать Winskel (1993).6Глава 2λ-исчислениеλ-исчисление основывается на так называемой ‘λ-нотации’ для обозначенияфункций. В неформальной математике, когда кто-то хочет сослаться на функцию,то обычно сначала дает этой функции произвольное имя, а затем использует его,например:Предположим, что f : R → R определена выражением:(f (x) =0if x = 022x sin(1/x ) if x 6= 0Тогда f 0 (x) не интегрируема по Лебегу в пределах [0, 1].Большинство языков программирования, например C, в этом отношении похожи:мы можем определить функции только давая им имена. Например, для того, чтобыиспользовать функцию successor (которая добавляет 1 к своим аргументам) несамым простым способом (например, используя указатель на нее), то хотя она иявляется очень простой, но все равно нам нужно назвать ее используя определениефункции, такое как:int suc ( int n ) {return n + 1 ;}В математике или программировании это кажется нормальным, и в общем случае,работает достаточно хорошо.
Однако, это может стать неудобным, когда начинаютиспользоваться функции высшего порядка (функции, которые манипулируютдругими функциями). В любом случае, если мы хотим рассматривать функциинаравне с другими математическими объектами, то требование именования функцийбудет нелогичным. При обсуждении арифметического выражения, построенного изболее простых выражений, мы просто записываем подвыражения не давая им имен.Представим, что если бы мы всегда работали с арифметическими выражениямитаким способом:Определим x и y, так что x = 2 и y = 4. Тогда xx = y.λ-нотация позволяет записывать функции практически тем же способом, чтои остальные виды математических объектов. Существует общепринятая нотация,72.1.
Преимущества лямбда-нотацииГлава 2. Лямбда-исчислениекоторая иногда использовалась в математике для этих целей, хотя обычно онаиспользуется как часть определения временного имени. Мы можем записатьx 7→ t[x]для обозначения функции, отображающей любой аргумент x в некотороепроизвольное выражение t[x], которое обычно, но не обязательно, содержит x (иногдаполезно “отбросить” аргумент). Однако, мы должны использовать другую нотацию,разработанную Church (1941):λx. t[x]которое должно читаться точно также, как и предыдущее выражение.
Например,λx. x является функцией отображения (????? identity function), которая простовозвращает переданный аргумент, в то время как λx. x2 является функциейвозведения в квадрат.Выбор символа λ является произвольным, и не несет никакой смысловойнагрузки. (Можно часто видеть, особенно во французских текстах, альтернативнуюнотацию [x] t[x].) Вероятно, что она возникла во время сложного процессаэволюции. В начале, в известной книге Principia Mathematica (Whitehead and Russell 1910) использовалась ‘hat’-нотация t[x̂] для функции от x производящей t[x].Чёрч (Church) изменил его на x̂. t[x], но поскольку наборщики текстов не моглипоместить значок ‘hat’ (крыша) над x, то оно появилось как ∧x.
t[x], которое затемтрансформировалось в λx. t[x] в руках других наборщиков.2.1Преимущества λ-нотацииИспользуя λ-нотацию мы можем прояснить некоторые неточности, внесенныенеформальной математической нотацией. Например, часто говорят о ‘f (x)’,используя контекст для определения того, что мы рассматриваем – саму функцию f ,или результат ее применения к конкретному x.
Дополнительной пользой будет то,что λ-нотация дает нам возможности анализа почти всей математической нотации.Если мы начнем с переменных и констант, и построим выражение используя лишь λабстракцию и применение функций к аргументом, то мы сможем представлять оченьсложные математические выражения.Мы будем использовать общепринятую нотацию f (x) для операции примененияфункции f к аргументу x, за тем исключением, что в традиционной λ-нотации,скобки могут быть опущены, что позволяет нам записывать это выражение ввиде f x. По причинам, которые станут понятны в процессе чтения следующегопараграфа, мы считаем, что применение функции ассоциативно слева, т.е. f x yозначает (f (x))(y).
В качестве сокращенной записи для λx. λy. t[x, y] мы будемиспользовать λx y. t[x, y], и т.д. Мы также предполагаем, что область λ-абстракциираспространяется вправо, насколько это возможно. Например„ λx. x y означаетλx. (x y), а не (λx. x) y.На первый взгляд нам необходимо введение специальной нотации для функцийнескольких аргументов.
Однако существует способ перевода таких функцийна обычную λ-нотацию. Этот способ называется каррированием (currying), поимени математика-логикаCurry (1930). (В действительности, этот способ уже8Глава 2. Лямбда-исчисление2.1. Преимущества лямбда-нотациииспользовался и Frege (1893), и Schönfinkel (1924), но легко понять, почемусоответствующие применения не получили общественного призвания.) Идеязаключается в использовании выражений, вида λx y. x + y. Это выражение можетрассматриваться как функция R → (R → R), так что можно сказать, что оно является‘функцией высшего порядка (higher order function)’ или ‘функционалом (functional)’,поскольку при применении к другой функции, она производит другую функцию,которая получает второй аргумент.
На самом деле, она получает аргументы поочереди, по одному, а не все сразу. Например, рассмотрим:(λx y. x + y) 1 2 = (λy. 1 + y) 2 = 1 + 2Заметьте, что в λ-нотации, применение функции считается лево-ассоциативнойоперацией, поскольку каррирование используется очень часто.λ-нотация в частности полезна в обеспечении унифицированной обработкисвязанных переменных. В математике переменные обычно выражают зависимостьнекоторого выражения от значения этой переменной; например, значение x2 + 2зависит от значения x. В таком контексте, мы будем говорить, что переменнаяявляется свободной.
Однако, существуют другие ситуации, где переменная простоиспользуется в качестве обозначения, а не показывает зависимость от значения. Вкачестве примеров можно рассмотреть переменную m в выраженииnXm=1m=n(n + 1)2и переменную y в выраженииZ x2y + a dy = x2 + ax0В логике, квантификаторы ∀x. P [x] (‘для всех x, P [x]’) и ∃x.
P [x] (‘существуеттакой x так что P [x]’) являются дополнительными примерами, а в теории множеств,мы имеем абстрактные множества, наподобие {x | P [x]}, а также индексированныеобъединения и пересечения. В таких случаях говорят, что переменная должнабыть связанной (bound). В определенных подвыражениях она является свободной,но в полном выражении, она связана операцией связывания переменных, такойкак сложение. Часть, находящаяся ‘внутри’ этой операции связывания переменныхназывается областью видимости (scope) связанной переменной.Аналогичная ситуация возникает в большинстве языков программирования, покрайней мере, в произошедших от Algol 60. Переменные имеют определеннуюобласти видимости, а формальные аргументы процедур и функций, являютсясвязанными переменными, например, n в определении на языке C функцииsuccessor, данном выше.
Кто-то может рассматривать объявления переменныхкак операцию связывания для вложенных объектов соответствующих переменных.Между прочим, заметьте, что область видимости переменной должна быть отделенаот ее времени жизни. В функции rand языка C, которую мы привели в введении,переменная n имеет ограниченную область видимости, но сохраняет свое значение,даже за пределами данного блока кода.Мы можем свободно изменить имя связанной переменной, без изменения смыславыражения. Например,92.1. Преимущества лямбда-нотацииZ xГлава 2.
Лямбда-исчисление2z + a dz = x2 + ax0Аналогичным образом, при использовании λ-нотации выражения λx. E[x] иλy. E[y] являются эквивалентными; это называется альфа-эквивалентностью, апроцесс преобразования между такими парами, называется альфа-конверсией.Мы должны добавить оговорку, что y не является свободной переменной ввыражении E[x], иначе значение выражения изменится, например, как вZ x2a + a da 6= x2 + ax0Также возможно использовать в одном выражении одинаковые имена длясвободных и связанных переменных; хотя это может сбивать с толку, но стехнической точки зрения это не является неоднозначным, напримерZ x2x + a dx = x2 + ax0В действительности, обычная нотация Лейбница для производных имеет то же самоесвойство, например, в:d 2x = 2xdxx используется и как связанная переменная ля того, чтобы показать, чтодифференцирование производится относительно x, и как свободная переменная,чтобы показать где будет происходить окончательное вычисление производной.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
