John Harrison - Введение в функциональное программирование (1108517), страница 17
Текст из файла (страница 17)
Однако, это не работает:#I’ = I;;Uncaught exception: Invalid_argument "equal: functional value"В общем случае запрещено сравнивать функции, хотя в нескольких специальныхслучаях, когда равенство функций очевидно, выдаётся true.60Глава 5. Знакомство с ML5.8.
Равенство функций#let f x = x + 1;;f : int -> int = <fun>#let g x = x + 1;;g : int -> int = <fun>#f = f;;- : bool = true#f = g;;Uncaught exception: Invalid_argument "equal: functional value"#let h = g;;h : int -> int = <fun>#h = f;;Uncaught exception: Invalid_argument "equal: functional value"#h = g;;- : bool = trueПочему существуют эти ограничения? Разве в ML функции не равноправныс другими разновидностями данных? Да, но к сожалению, (экстенсиональное)равенство функций в общем случае невычислимо. Это следует из различныхклассических результатов теории алгоритмов, таких как неразрешимость проблемыостанова и теорема Райса.7 Приведём конкретный пример, демонстрирующийэту неразрешимость.
На данный момент для функции, определённой ниже, таки не установлено, завершается ли её вычисление для произвольного аргумента.Предположение, что данная функция вычислима всюду, известно как гипотезаКоллатца (Collatz conjecture):8#let rec collatz n =if n <= 1 then 0else if even(n) then collatz(n / 2)else collatz(3 * n + 1);;collatz : int -> int = <fun>С другой стороны, очевидно, что в случае завершения вычислений их результатомвсегда будет 0. Теперь рассмотрим следующую тривиальную функцию:#let f (x:int) = 0;;f : int -> int = <fun>Решив уравнение collatz = f, компьютер подтвердил бы гипотезу Коллатца.Похожие примеры также легко построить на основе других математических задач,решение которых пока не найдено.Процедура контроля типов может быть расширена таким образом, что позволитвыявлять без выполнения программы попытки сравнения как элементарныхобъектов-функций, так и объектов-агрегатов, в состав которых входят объектыфункции.
Типы данных, в которые не входят подвыражения типа функция, известныкак сравнимые типы, поскольку всегда возможно проверить объекты таких типов7Вы увидите доказательства в курсе теории алгоритмов. Теорема Райса — чрезвычайно сильныйвывод о неразрешимости, которая утверждает, что любое нетривиальное свойство функции,соответствующее программе, невычислимо из её текста. Отличной книгой по теории алгоритмовявляется Davis, Sigal, and Weyuker (1994).8Хороший обзор этой проблемы и попыток её решнения приведены в Lagarias (1985).
Строгоговоря, мы должны использовать целые числа неограниченной разрядности, а не машиннуюарифметику. Позже мы увидим как это сделать.615.8. Равенство функцийГлава 5. Знакомство с MLна равенство. В то же время, это делает систему типов более сложной. Однако,сторонники такого подхода придерживаются мнения, что статическая проверкатипов должна быть настолько полной, насколько это возможно.Дополнительная литератураМногие книги о функциональном программировании содержат информацию пообщим для всех функциональных языков аспектам, которые мы тоже обсуждали,например, по стратегии вычислений. Хорошее элементарное введение в CAMLLight и функциональное программирование можно найти в Mauny (1995).
Paulson(1991) также является хорошей книгой, хотя основывается на Standard ML.Примеры1. Предположим, что ‘функция-условие’, определённая ite(b,x,y) = if b thenx else y является единственной функцией, которая может работать саргументами типа bool. Существует ли способ написать функцию факториала?2. Докажите при помощи правил типизации, приведённых в предыдущей главе,что комбинатор S имеет в точности тот тип, который выводит для него ML.3. Напишите простую рекурсивную функцию возведения в степень целых чисел,т.е. вычисляющую xn для n ≥ 0. Напишите на ML пару функций, изэквивалентности которых следовала бы справедливость Великой теоремыФерма: не существует целых чисел x, y, z и натурального числа n > 2 таких,что xn + y n = z n , за исключением тривиального случая, когда x = 0 или y = 0.62Глава 6Более подробно о MLВ этой главе мы закрепим предыдущие примеры, более точно определивсинтаксис и основные возможности ML, а затем перейдём к рассмотрению некоторыхдополнительных возможностей, таких как рекурсивные типы.
Но начнём обсуждениявзаимодействия с системой.До сих пор мы печатали команды в интерпретатор, получая от него результат.Однако, это не лучший способ писать нетривиальные программы. Обычно вамследует записывать все выражения и объявления в файл. После этого повторноеиспользование кода обеспечивается операцией «вырезать и вставить».
Эта операцияможет быть выполнена с помощью X Window System и схожих систем, илив редакторе типа Emacs. Такой подход, однако, становится утомительным инеэффективным для больших программ. Вместо этого вы можете использоватьфункцию include для непосредственного чтения из файла. Например, если файлmyprog.ml содержит:l e t pythag x y z =x ∗ x + y ∗ y = z ∗ z ;;pythag 3 4 5 ; ;pythag 5 12 1 3 ; ;pythag 1 2 3 ; ;то введя в интерпретатор include "myprog.ml";; вы получите:#includepythag :- : bool- : bool- : bool- : unit"myprog.ml";;int -> int -> int -> bool = <fun>= true= true= false= ()То есть, вывод системы ML получился такой же, как если бы вы печаталисодержимое файла в консоль. Последняя строка вывода – это результат вычислениясамого выражения includeВ больших программах часто полезно включать комментарии.
В ML онизаписываются между символами (* и *), например:636.1. Основные типы данных и операцииГлава 6. Более подробно о ML(∗ −−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−− ∗)(∗ This f u n c t i o n t e s t s i f ( x , y , z ) i s a Pythagorean t r i p l e ∗)(∗ −−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−− ∗)l e t pythag x y z =x ∗ x + y ∗ y = z ∗ z ;;(∗ comments ∗) pythag (∗ can ∗) 3 (∗ go ∗) 4 (∗ a l m o s t ∗) 5 (∗ anywhere ∗)(∗ and (∗ can (∗ be (∗ n e s t e d ∗) q u i t e ∗) a r b i t r a r i l y ∗) ∗) ; ;6.1Основные типы данных и операцииML представляет несколько встроенных примитивных типов.
Из них, с помощьюконструкторов типов, могут быть построены составные типы. Пока мы будемиспользовать только конструктор функциональных типов -> и конструктордекартового произведения типов *. В своё время мы рассмотрим и другиеконструкторы, а также узнаем как определять новые типы и конструкторы типов.Примитивные типы, которые интересуют нас, это:• Тип unit, можно называть его процедурным. Это одноэлементный тип,единственный элемент которого записывается как (). Очевидно, использованиетипа unit не передаёт какой-либо информации, так что он часто используетсякак возвращаемый тип императивно записанных «функций», результаткоторых не значение вычислений, а какой-либо побочный эффект.
Например,таких как include. Он так же может использоваться как тип функции,используемой для приостановки вычислений.• Тип bool. Двухэлементный тип булевых значений (значений истинности).Элементы этого типа: true и false.• Тип int. Содержит конечное подмножество отрицательных и неотрицательныхчисел.
Обычно значения варьируются от −230 (−1073741824) до 230 − 1(1073741823). 1 Элементы записываются обычным способом, например: 0, 32,-25.• Тип string содержит строки (т.е. конечные последовательности) символов.Они записываются и печатаются в двойных кавычках, вот так: "hello". Длязаписи специальных символов используется экранирование в стиле языка С.Например, " - запись двойной кавычки, \n - символ перевода строки.Значения, такие как (), false, 7 и "caml", в смысле лямбда - исчислениярассматриваются как константы. Другие константы соответствуют операциямна основных типах. Некоторые из них, из соображений привычности, могутбыть записаны как инфиксные.
Для операций определено понятие приоритета,1На самом деле, в машинной арифметике значения ещё более ограничены, поскольку одинбит используется сборщиком мусора (см. определения). Далее мы увидим, как использоватьальтернативный тип целых с неограниченной точностью.64Глава 6. Более подробно о ML6.1. Основные типы данных и операциипоэтому выражения группируются так, как ожидается. Например, мы пишемx + y вместо + x y, и x < 2 * y + z вместо < x (+ (* 2 y) z).
Логическийоператор not выделяется тем, что имеет особое правило разбора, для него невыполняется обычное правило ассоциативности слева: not not p означает not(not p). Функцию, определённую пользователем, можно задать как инфиксную, спомощью директивы #infix. Например, вот определение функции, выполняющейкомпозицию функций:#l e t s u c c e s s o r x = x + 1 ; ;s u c c e s s o r : i n t −> i n t = <fun>#l e t o f g = fun x −> f ( g x ) ; ;o : ( ’ a −> ’ b ) −> ( ’ c −> ’ a ) −> ’ c −> ’ b = <fun>#l e t add3 = o s u c c e s s o r ( o s u c c e s s o r s u c c e s s o r ) ; ;add3 : i n t −> i n t = <fun>#add3 0 ; ;− : int = 3##i n f i x "o " ; ;#l e t add3 ’ = s u c c e s s o r o s u c c e s s o r o s u c c e s s o r ; ;add3 ’ : i n t −> i n t = <fun>#add3 ’ 0 ; ;− : int = 3В ML нет возможностей задавать приоритет для инфиксных операций,определённых пользователем, а также определять неинфиксные операции какправоассоциативные.
Также запомните, что неявная операция «аппликацияфункции» имеет приоритет выше, чем у любой другой бинарной операции, такчто successor 1 * 2 разбирается как (successor 1) * 2. Если хотите использоватьфункцию с особым статусом как обычную константу, вам потребуется prefix:#o successor successor;;Toplevel input:>o successor successor;;>^Syntax error.#prefix o successor successor;;- : int -> int = <fun>#(prefix o) successor successor;;- : int -> int = <fun>Разобравшись с этими деталями синтаксиса, давайте рассмотрим список операцийна основных типах. Унарные операции:Оператор ТипЗначениеint -> intЧисленное отрицаниеnotbool -> bool Логическое отрицаниеи бинарные операции, в порядке убывания приоритета:656.1. Основные типы данных и операцииОператорmod*/+^=<><<=>>=&orГлава 6.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
