John Harrison - Введение в функциональное программирование (1108517), страница 16
Текст из файла (страница 16)
Система может сделать это, поскольку знает типвстроенного оператора сложения +. С другой стороны, если для выражения не можетбыть определён тип, то система отвергнет его и постарается выдать сообщение о том,почему произошла ошибка. В сложных случаях сообщения об ошибках достаточнотяжело понять.#1 + true;;Toplevel input:>let it = 1 + true;;>^^^^This expression has type bool,but is used with type int.Поскольку ML является функциональным языком, то выражения могут иметьфункциональный тип.
Для λ-абстракций λx. t[x] ML предоставляет следующийсинтаксис — fun x -> t[x]. Например, мы можем определить функцию вычисленияцелого числа, следующего за данным:#fun x -> x + 1;;- : int -> int = <fun>Как и в предыдущем примере, тип выражения (сейчас это int -> int),выводится и выдаётся на экран. Однако сама функция не печатается; системалишь выдаёт <fun>. Это сделано потому, что внутреннее представление функцийне слишком читабельно.4 Функции применяются к следующим за ними аргументам,так же как и в λ-исчислении. Например:#(fun x -> x + 1) 4;;- : int = 5Подобно λ-исчислению, применение функции левоассоциативно, так что выможете определять каррированные функции, используя то же самое соглашение посокращению повторяющихся λ-абстракций (т.е., fun-й).
Например, все следующиевыражения эквивалентны:#((fun x -> (fun y -> x + y)) 1) 2;;- : int = 3#(fun x -> fun y -> x + y) 1 2;;- : int = 3#(fun x y -> x + y) 1 2;;- : int = 34CAML не хранит их как синтаксические деревья, а компилирует в байт-код.56Глава 5. Знакомство с ML5.65.6. Связывания и объявленияСвязывания и объявленияВводить большое выражение целиком утомительно, гораздо удобнее будетвоспользоватся let для связывания осмысленных подвыражений с именами. Этоможет быть сделано следующим образом:#let successor = fun x -> x + 1 insuccessor(successor(successor 0));;- : int = 3Для связывания функций существует более элегантная конструкция:#let successor x = x + 1 insuccessor(successor(successor 0));;- : int = 3в том числе для рекурсивных определений, дополненных ключевым словом rec:#let rec fact n = if n = 0 then 1else n * fact(n - 1) infact 6;;- : int = 720Используя and, мы можем сделать несколько связываний одновременно иопределить взаимно рекурсивные функции.
Вот пример двух простых, хотя и сильнонеэффективных, функций, которые определяют, является ли натуральное числочётным или нечётным:#let rec even n = if n = 0 then true else odd (n - 1)and odd n = if n = 0 then false else even (n - 1);;even : int -> bool = <fun>odd : int -> bool = <fun>#even 12;;- : bool = true#odd 14;;- : bool = falseВ действительности, любое связывание может быть сделано отдельно от егоприменения. ML помнит набор связанных переменных, и пользователь можетпополнять данный набор интерактивно.
Просто уберите in и завершите выражениедвойной точкой с запятой:#let successor = fun x -> x + 1;;successor : int -> int = <fun>После этого объявления, любое последующее выражение может использоватьфункцию successor, например:#successor 11;;- : int = 12575.6. Связывания и объявленияГлава 5. Знакомство с MLЗаметьте, что мы не делаем присваивания значений переменным. Каждоесвязывание выполняется только раз, когда система анализирует введённые данные;оно не может быть повторено или изменено. Оно может быть перезаписано новымопределением с тем же именем, но это не присваивание, в своём обычном значении,поскольку последовательность событий связана только с процессом компиляции,а не с динамикой выполнения программы. Конечно, отходя от интерактивногополучения ответа от системы, мы можем полностью заменить все двойные точкис запятой, записанные после объявлений, на in и вычислить всё сразу.
С этой точкизрения видно, что переписывание объявления в действительности соответствуетопределению новой локальной переменной, которая скрывает предыдущую, всоответствии с обычными правилами λ-исчисления. Например:#let x = 1;;x : int = 1#let y = 2;;y : int = 2#let x = 3;;x : int = 3#x + y;;- : int = 5является тем же самым, что и:#let x = 1 inlet y = 2 inlet x = 3 inx + y;;- : int = 5Обязательно заметьте, что следуя λ-исчислению, связывание переменныхявляется статическим, например, первое связывание x используется до того, какбудет сделано новое связывание, и любое его использование до нового определенияне будет затронуто этим определением.
Например:#let x = 1;;x : int = 1#let f w = w + x;;f : int -> int = <fun>#let x = 2;;x : int = 2#f 0;;- : int = 1Первые версии LISP, однако, использовали динамическое связывание, когдапереопределение переменной также распространялось на предыдущие использованияэтой переменной, так что аналогичная последовательность команд должнабудет вернуть число 2. В действительности это считалось ошибкой, но скоропрограммисты начали использовать эту возможность.
Как следствие, когданекоторая низкоуровневая функция изменялась, то изменения распространялись навсе её применения в других функциях без необходимости перекомпиляции. Такаявозможность продолжала существовать долгое время во многих диалектах LISP, нов конечном счёте победила идея, что статическое связывание лучше. В Common LISPпо умолчанию используется статическое связывание, но динамическое также можноразрешить, если необходимо, используя ключевое слово special.58Глава 5. Знакомство с ML5.75.7. Полиморфные функцииПолиморфные функцииМы можем определять полиморфные функции, например, тождественноеотображение:#let I = fun x -> x;;I : ’a -> ’a = <fun>Внешнее представление в ASCII-кодировке типовых переменных α, β, .
. . в MLимеет вид ’a, ’b, . . . Пример использования полиморфной функции с разнымитипами:#I true;;- : bool = true#I 1;;- : int = 1#I I I I 12;;- : int = 12В данном примере все вхождения I имеют различные типы и интуитивносоответствуют разным функциям. Очередным этапом будет определение всехбазовых комбинаторов:#let I x = x;;I : ’a -> ’a = <fun>#let K x y = x;;K : ’a -> ’b -> ’a = <fun>#let S f g x = (f x) (g x);;S : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun>Заметьте, что система сама следит за типами, несмотря на то, что в последнемслучае они были довольно сложными. Теперь, вспомним, что I = S K K; давайтепопробуем сделать это на ML:5#let I’ = S K K;;I’ : ’_a -> ’_a = <fun>Выражение имеет правильный тип6 и может быть легко проверено на конкретныхслучаях, например:#I’ 3 = 3;;- : bool = trueВ приведённых примерах полиморфных функций система очень быстро выводитнаиболее общий тип для каждого выражения, и этот тип достаточно прост.
Такобычно и происходит на практике, но существуют патологические случаи, например,следующий пример, приведённый в Mairson (1990). Тип этого выражения выводитсяоколо 10 секунд и занимает более 4000 строк на 80-символьном терминале.5Отметим, что без учёта типов, S K A = I верно для любого A. Однако, читатель может сампопробовать, например, S K S и убедиться, что его тип является менее общим, чем ожидалось.6Игнорируйте подчёркивания.
Это связано с типизацией императивных конструкций, которыемы обсудим позже.595.8. Равенство функцийlet pairl e t x1 =l e t x2 =l e t x3 =l e t x4 =l e t x5 =x5 ( fun zГлава 5. Знакомство с MLx y = fun z −> z x y infun y −> p a i r y y infun y −> x1 ( x1 y ) infun y −> x2 ( x2 y ) infun y −> x3 ( x3 y ) infun y −> x4 ( x4 y ) in−> z ) ; ;Мы уже упоминали, что программисты на ML никогда не задают типы. Этоправда в том смысле, что транслятор ML сам назначит выражению наиболее общийтип. Однако, иногда бывает полезно ограничить вывод типа. Подобная мера незаставит работать код, который до этого не работал, но может использоваться какдокументация для понимания его предназначения; также возможно использоватьболее короткие синонимы для сложных типов. Ограничение типа может быть заданов ML путём добавления аннотации типа после некоторого выражения. Аннотациитипов состоят из двоеточия, за которым указан тип.
Обычно расположениеаннотаций не имеет значения; если они есть, то они заставляют использоватьсоответствующие ограничения. Например, вот несколько альтернативных вариантовявного назначения тождественной функции типа int -> int:#let I (x:int) = x;;I : int -> int = <fun>#let I x = (x:int);;I : int -> int = <fun>#let (I:int->int) = fun x -> x;;I : int -> int = <fun>#let I = fun (x:int) -> x;;I : int -> int = <fun>#let I = ((fun x -> x):int->int);;I : int -> int = <fun>5.8Равенство функцийВместо проверки эквивалентности функций, таких как I и I 0 , сравнениемрезультатов их применения к конкретным аргументам, например 3, можетпоказаться, что мы можем разрешить данный вопрос путём сравнения самихфункций.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
