John Harrison - Введение в функциональное программирование (1108517), страница 18
Текст из файла (страница 18)
Более подробно о MLТипint -> int -> intint -> int -> intint -> int -> intint -> int -> intint -> int -> intstring -> string -> string’a -> ’a -> bool’a -> ’a -> bool’a -> ’a -> bool’a -> ’a -> bool’a -> ’a -> bool’a -> ’a -> boolbool -> bool -> boolbool -> bool -> boolЗначениеВзятие модуляПроизведениеЦелочисленное делениеСложениеВычитаниеСклейка строкРавенствоНеравенствоМеньше чемМеньше или равноБольше чемБольше или равноЛогическое «и»Логическое «или»Например, x > 0 & x < 1 парсится как & (> x 0) (< x 1).
Заметьте, что всесравнения, не только по равенству, полиморфны. Они не только соответствующимобразом упорядочивают числа и строчки, но также и остальные примитивные, исоставные типы. Однако, они не применимы к функциям.Две логические операции & и or имеют особую стратегию вычисления.
Всущности, их можно рассматривать как синонимы условных выражений:4p & q = if p then q else false4p or q = if p then true else qСледовательно, операция «and» вычисляет первый аргумент, и только если егозначение true, вычисляет следующий. Напротив, «or» вычисляет первый аргумент,и только если это false, вычисляет второй.Выражения в ML строятся из констант и переменных; любой идентификатор,не связанный на текущий момент выполнения программы, рассматривается какпеременная.
Объявления связывают значения выражений с именами, при этом всостав выражений могут входить другие объявления. Следовательно, синтаксическиеклассы выражений и объявлений взаимно рекурсивны. Мы можем выразить этоследующей БНФ - грамматикой.2expression ::=||||||variableconstantexpression expressionexpression inf ix expressionnot expressionif expression then expression else expressionfun pattern → expression2Мы отбросили многие конструкции, которые нами не будут использоваться.
За подробностямиобращайтесь к руководству по CAML.66Глава 6. Более подробно о MLdeclarationlet_bindingslet_bindingpatternvariables||::=|::=|::=::=::=|6.2. Дальнейшие примеры(expression)declaration in expressionlet let_bindingslet rec let_bindingslet_bindinglet_binding and let_bindingspattern = expressionvariablesvariablevariable variablesПозже мы более подробно обсудим синтаксический класс pattern. До сих пормы имели дело только с variable или variable variable · · · variable. В первом случаемы просто связываем выражение с именем, тогда как во втором, для объявленияфункций, используется специальный синтаксический сахар.
Аргументы функциизаписываются после имени функции, слева от знака равенства. Например, вотобъявление функции, add4, которая может использоваться для прибавления 4 к еёаргументу:#let add4 x =let y = successor x inlet z = let w = successor y insuccessor w insuccessor z;;add4 : int -> int = <fun>#add4 1;;- : int = 5Представляется полезным разбор этого объявления в соответствии с приведённойвыше грамматикой.6.2Дальнейшие примерыНе сложно задать рекурсивную функцию, принимающую в качестве аргументовцелочисленное n и функцию f , а возвращающую f n , т.е. f ◦ · · · ◦ f (n раз):#let rec funpow n f x =if n = 0 then xelse funpow (n - 1) f (f x);;funpow : int -> (’a -> ’a) -> ’a -> ’a = <fun>В действительности, небольшое размышление показывает, что функция funpowпринимает машинное целое n и возвращает нумерал (число) Чёрча,соответствующее n.
Поскольку функции не выводятся на печать, мы не можем вдействительности посмотреть на лямбда-выражение, представляющее число Чёрча:#funpow 6;;- : (’_a -> ’_a) -> ’_a -> ’_a = <fun>676.2. Дальнейшие примерыГлава 6. Более подробно о MLТакже просто задаётся функция обратная к funpow, которая принимает числоЧёрча и возвращает машинное целое:#let defrock n = n (fun x -> x + 1) 0;;defrock : ((int -> int) -> int -> ’a) -> ’a = <fun>#defrock(funpow 32);;- : int = 32Мы можем проверить некоторые из арифметических операций на числах Чёрча:#let add m n f x = m f (n f x);;add : (’a -> ’b -> ’c) -> (’a -> ’d -> ’b) -> ’a -> ’d -> ’c = <fun>#let mul m n f x = m (n f) x;;mul : (’a -> ’b -> ’c) -> (’d -> ’a) -> ’d -> ’b -> ’c = <fun>#let exp m n f x = n m f x;;exp : ’a -> (’a -> ’b -> ’c -> ’d) -> ’b -> ’c -> ’d = <fun>#let test bop x y = defrock (bop (funpow x) (funpow y));;test :(((’a -> ’a) -> ’a -> ’a) ->((’b -> ’b) -> ’b -> ’b) -> (int -> int) -> int -> ’c) ->int -> int -> ’c = <fun>#test add 2 10;;- : int = 12#test mul 2 10;;- : int = 20#test exp 2 10;;- : int = 1024Примеры выше, очевидно, не являются самым эффективным способомвыполнения арифметических операций.
Далее, ML не имеет функции для возведенияв степень, но её легко задать по рекурсии:#let rec exp x n =if n = 0 then 1else x * exp x (n - 1);;exp : int -> int -> int = <fun>Это решение выполняет n произведений для вычисления xn . Более эффективныйспособ использует тот факт, что x2n = (xn )2 и x2n+1 = x(xn )2 :#let square x = x * x;;square : int -> int = <fun>#let rec exp x n =if n = 0 then 1else if n mod 2 = 0 then square(exp x (n / 2))else x * square(exp x (n / 2));;exp : int -> int -> int = <fun>#infix "exp";;#2 exp 10;;- : int = 1024#2 exp 20;;- : int = 1048576Другая классическая операция на натуральных числах - нахождение ихнаибольшего общего делителя при помощи алгоритма Евклида:68Глава 6. Более подробно о ML6.3.
Определения типов#let rec gcd x y =if y = 0 then x else gcd y (x mod y);;gcd : int -> int -> int = <fun>#gcd 100 52;;- : int = 4#gcd 7 159;;- : int = 1#gcd 24 60;;- : int = 12Мы использовали оператор рекурсии Rec при объяснении рекурсивныхопределений. Действительно, давайте определим его:#let rec Rec f = f(fun x -> Rec f x);;Rec : ((’a -> ’b) -> ’a -> ’b) -> ’a -> ’b = <fun>#let fact = Rec (fun f n -> if n = 0 then 1 else n * f(n - 1));;fact : int -> int = <fun>#fact 3;;it : int = 6Обратите внимание на необходимость анонимной функции, в противном случаевыражение Rec f уходит в бесконечную последовательность рекурсивных вызовов,прежде чем функция будет применена к своему аргументу:#let rec Rec f = f(Rec f);;Rec : (’a -> ’a) -> ’a = <fun>#let fact = Rec (fun f n -> if n = 0 then 1 else n * f(n - 1));;Uncaught exception: Out_of_memory6.3Определения типовМы уже говорили о том, что ML имеет возможности для объявления новыхконструкторов типов, так что сложные типы данных могут быть построены набазе существующих.
В действительности, ML позволяет создавать типы не толькоиз существующих типов, но и из самих сложных типов данных. Такие типыназываются рекурсивными. Они объявляются с помощью ключевого слова type, закоторым выражение, описывающее как тип создаётся из существующих типов и себя.Мы покажем это на нескольких примерах. Первым примером будет определениетипа sum, которые должен соответствовать несвязному объединению (t) двухсуществующих типов.#type (’a,’b)sum = inl of ’a | inr of ’b;;Type sum defined.Грубо говоря, объект типа (’a,’b)sum является либо чем-то типа ’a, либо чемто типа ’b. Однако, говоря более формально, все эти объекты имеют разные типы.Объявление типа, также определяет так называемые конструкторы inl и inr.
Этофункции, которые получают объекты с типами компонентов, и встраивают ?????inject их в новый тип. Мы действительно можем видеть их типы в ML и применять ихк объектам:696.3. Определения типовГлава 6. Более подробно о ML#inl;;- : ’a -> (’a, ’b) sum = <fun>#inr;;- : ’a -> (’b, ’a) sum = <fun>#inl 5;;- : (int, ’a) sum = inl 5#inr false;;- : (’a, bool) sum = inr falseМы можем показать данную ситуацию с помощью следующей диаграммы. Приналичии двух существующих типов α и β, тип (α, β)sum создаётся из точныхотдельных копий α и β, и два конструктора отображаются на соответствующиекопии:(α, β)sumαβXXXXX inlXXXXXXXXz: inrЭто аналогично использованию union в языке C, но в ML копии типовкомпонентов хранятся отдельно и кто-то всегда знает, к какому из этих элементовотносится объединение.
В противоположность этому, в C типы компонентовпересекаются и программист отвечает за корректность работы с ними.6.3.1Сопоставление с образцомКонструкторы в таком определении имеют три очень важных качества:• Они полные (????exhaustive), т.е., каждый элемент нового типа может бытьполучен через inl x для некоторого x или через inr y для некоторого y. Такчто, новый тип не содержит ничего, кроме копий типов компонент.• Они являются инъективными, т.е. тест на равенство inl x = inl y даётистинный результат, если, и только если x = y, и аналогичным образом, дляinr. Так что, новый тип содержит точную копию типа каждого компонента,без идентификации любого из элементов.• Они индивидуальны, т.е.
их диапазоны несвязны. Это означает, что впредыдущем примере inl x = inr y будет ложным, независимо от того, чемявляются x и y. Так что, копия типа каждого компонента в новом типе,хранится независимо.Второе и третье свойство конструкторов выравнивает (???justify) нашеиспользование сопоставления с образцом. Это выполняется за счёт использованияболее общих varstructs ???? как аргументов в lambda-выражениях, например:70Глава 6. Более подробно о ML6.3. Определения типов#fun (inl n) -> n > 6| (inr b) -> b;;- : (int, bool) sum -> bool = <fun>Эта функция имеет свойство (достаточно натуральное), что когда она применяетсяк inl n она возвращает n > 6, а когда она применяется к inr b, то она возвращаетb.
Это происходит в соответствии со вторым и третьим свойствами конструкторов,что даёт нам хорошо определённую функцию. Поскольку конструкторы являютсяинъективными, мы можем точно восстановить n из inl n и b из inr b. Посколькуконструкторы индивидуальны, мы знаем, что два выражения не могут быть взаимнонеконсистетны, поскольку никакое значение не соответствует обоим образцам.В добавление к этому, поскольку кострукторы являются полными (??? exhaustive), мы знаем, что каждое значение будет подпадать под один из образцов, так чтофункция определена везде.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
