John Harrison - Введение в функциональное программирование (1108517), страница 19
Текст из файла (страница 19)
В действительности, разрешается ослабить это свойствопутём неуказания некоторых образцов, хотя при этом ML выдаст предупреждение:#fun (inr b) -> b;;Toplevel input:>fun (inr b) -> b;;>^^^^^^^^^^^^^^^^Warning: this matching is not exhaustive.- : (’a, ’b) sum -> ’b = <fun>Если эта функция применяется к чему-то вида inl x, то она не будет работать:#let f = fun (inr b) -> b;;Toplevel input:>let f = fun (inr b) -> b;;>^^^^^^^^^^^^^^^^Warning: this matching is not exhaustive.f : (’a, ’b) sum -> ’b = <fun>#f (inl 3);;Uncaught exception: Match_failure ("", 452, 468)Хотя логические значения и встроены в ML, они эффективно определяютсятривиальным использованием рекурсивного типа, часто называемого (типперечисление) enumerated type, где конструкторы не получают аргументов:#type bool = false | true;;В самом деле, разрешается определять выражения путём сопоставления систинным значением.
Следующие два выражения полностью эквивалентны:#if 4 < 3 then 1 else 0;;- : int = 0#(fun true -> 1 | false -> 0) (4 < 3);;- : int = 0Однако, сопоставление с образцом не ограничивается определением элементоврекурсивных типов, хотя в частности это очень удобно. Например, мы можемопределить функцию, которая сообщает нам является ли число нулём, следующимобразом:716.3. Определения типовГлава 6. Более подробно о ML#fun 0 -> true | n -> false;;- : int -> bool = <fun>#(fun 0 -> true | n -> false) 0;;- : bool = true#(fun 0 -> true | n -> false) 1;;- : bool = falseВ этом случае, мы не имеем взаимсной исключительности образцов, поскольку0 соответствует обоим образцам.
Образцы сопостовляются по порядку, один задругим, и используется первый соответствующий. Заметьте, что пока соответствияне являются взаимно исключающими, нет гарантии, что каждое выражениесодержит математическое уравнение. Например, в предыдущем примере, функцияне возвращает false для любого n, так что второе выражение не универсально.Заметьте, что только конструкторы могут использоваться в вышеприведённыхвыражениях как компоненты образцов. Обычные константы будут рассматриватьсякак новые переменные, связанные внутри образца.
Например, рассмотримследующий код:#let true_1 = true;;true_1 : bool = true#let false_1 = false;;false_1 : bool = false#(fun true_1 -> 1 | false_1 -> 0) (4 < 3);;Toplevel input:>(fun true_1 -> 1 | false_1 -> 0) (4 < 3);;>^^^^^^^Warning: this matching case is unused.- : int = 1В общем, элемент-модуль (unit element) (), истинные значения, целые числа,строковые константы и операция образования пар (infix comma) имеют статусконструкторов, также как и другие конструктора из предопределённых рекурсивныхтипов. Когда они встречаются в образце, соответствующее значение должноиметь соответствующий тип.
Все другие идентификаторы соответствуют любомувыражению и становятся связанными в процессе обработки.Также как и ???varstructs в λ-выражениях, существуют другие способывыполнения сопоставления с образцом. Вместо создания функции с помощьюсопоставления с образцом, и применения её к выражению, мы можем выполнятьсопоставление с образцом напрямую используя следующую конструкцию:match expression with pattern1 −>E1 | · · · | patternn −>EnПростейшей альтернативой этому является использованиеlet pattern = expressionно в этом случае разрешено использование лишь одного образца.72Глава 6.
Более подробно о ML6.3.26.3. Определения типовРекурсивные типыПредыдущие примеры были бессодержательны в том смысле, что мы неопределяли тип через самое себя. В качестве более интересного примера давайтеобъявим тип списков 3 элементов типа ’a.#type (’a)list = Nil | Cons of ’a * (’a)list;;Type list defined.Проверим типы конструкторов:#Nil;;- : ’a list = Nil#Cons;;- : ’a * ’a list -> ’a list = <fun>Конструктор Nil, не принимающий никаких аргументов, просто создаётнекоторый объект типа (’a)list, который рассматривается как пустой список.Другой конструктор Cons принимает аргументы типа ’a и (’a)list, а возвращаетновый список, который образован из предыдущего добавлением в начало первогоэлемента.
Например:#Nil;;- : ’a list = Nil#Cons(1,Nil);;- : int list = Cons (1, Nil)#Cons(1,Cons(2,Nil));;- : int list = Cons (1, Cons (2, Nil))#Cons(1,Cons(2,Cons(3,Nil)));;- : int list = Cons (1, Cons (2, Cons (3, Nil)))Поскольку значение конструктора инъективно зависит от аргументов, легкопонять, что все значения, которые мы рассматривали как списки [], [1], [1; 2]и [1; 2; 3], различны, а списки различной длины будут иметь различный тип.Фактически, ML уже имеет тип list, точно такой, как только что был определён.Единственная разница в синтаксисе: пустой список записывается как [], арекурсивный конструктор :: – инфиксный.
Следовательно, все упомянутые спискив действительности записываются:#[];;- : ’a list = []#1::[];;- : int list = [1]#1::2::[];;- : int list = [1; 2]#1::2::3::[];;- : int list = [1; 2; 3]Списки выводятся в удобном виде, это же справедливо и для ввода. Тем не менее,следует помнить, что это синтаксический сахар, а списки можно выражать и явно,в терминах конструкторов. Например, мы можем, используя сравнение по образцу,определить функции, принимающие начало и хвост списка.3конечных упорядоченных последовательностей736.3.
Определения типовГлава 6. Более подробно о ML#let hd (h::t) = h;;Toplevel input:>let hd (h::t) = h;;>^^^^^^^^^^^^^Warning: this matching is not exhaustive.hd : ’a list -> ’a = <fun>#let tl (h::t) = t;;Toplevel input:>let tl (h::t) = t;;>^^^^^^^^^^^^^Warning: this matching is not exhaustive.tl : ’a list -> ’a list = <fun>Компилятор предупреждает нас, что применение этих функций к пустым спискамприведёт к ошибкам.
Посмотрим на них в действии:#hd [1;2;3];;- : int = 1#tl [1;2;3];;- : int list = [2; 3]#hd [];;Uncaught exception: Match_failureОбратите внимание, следующее определение hd не является корректным. Вдействительности, функция принимает в качестве аргумента список ровно из двухаргументов, а на списках отличной длины не определена:#let hd [x;y] = x;;Toplevel input:>let hd [x;y] = x;;>^^^^^^^^^^^^Warning: this matching is not exhaustive.hd : ’a list -> ’a = <fun>#hd [5;6];;- : int = 5#hd [5;6;7];;Uncaught exception: Match_failureСравнение по образцу может комбинироваться с рекурсией. Например, вотфункция, возвращающая длину списка:#let rec length =fun [] -> 0| (h::t) -> 1 + length t;;length : ’a list -> int = <fun>#length [];;- : int = 0#length [5;3;1];;- : int = 3В качестве альтернативы можно задать её с помощью функций hd и tl:#let rec length l =if l = [] then 0else 1 + length(tl l);;Последний стиль задания функции весьма распространён во многих языках,особенно в LISP, но непосредственное сравнение по образцу часто бывает болееэлегантно.74Глава 6.
Более подробно о ML6.3.36.3. Определения типовДревовидные структурыЧасто бывает полезно представлять части рекурсивных типов в виде дерева срекурсивными конструкторами в узлах, и остальными типами данных в качествелистьев. Рекурсивность просто говорит о том как дерево образуется из отдельныхподдеревьев. В случае списков «деревья» более вытянутые и односторонние.
Так,список [1;2;3;4] представляется в следующем виде:@@@1@@@@2@@@3@@4[]Рекурсивные типы, допускающие построение более сбалансированных деревьев,задаются также просто, например:#type (’a)btree = Leaf of ’a| Branch of (’a)btree * (’a)btree;;В общем, может быть несколько различных рекурсивных конструкторов, сразличным числом потомков. Это даёт очень простой способ представлениясинтаксических деревьев для языков программирования (и других формальныхязыков).
Например, вот тип для представления арифметических выражений,построенных из целых чисел, операций сложения и умножения.#type expression = Integer of int| Sum of expression * expression| Product of expression * expression;;А вот рекурсивная функция для вычисления таких выражений:#let rec eval =fun (Integer i) -> i| (Sum(e1,e2)) -> eval e1 + eval e2| (Product(e1,e2)) -> eval e1 * eval e2;;eval : expression -> int = <fun>#eval (Product(Sum(Integer 1,Integer 2),Integer 5));;- : int = 15Подобные абстрактные синтаксические деревья могут быть весьма успешнымпредставлением данных, допускающим всевозможные манипуляции над ними. Так,часто первое действие компиляторов заключается в переводе, согласно правиламсинтаксического разбора, текста на входе в «абстрактное синтаксическое дерево».Обратите внимание, что при этом условности, вроде приоритета или использованияскобок, уже не требуются.
Как только мы достигаем уровня абстрактного синтаксиса,756.3. Определения типовГлава 6. Более подробно о MLвсё выражается явно за счёт структуры дерева. Мы будем использовать подобнуютехнику при написании ML версий формальных правил лямбда-исчисления. Начнёмс типа, используемого для представления лямбда-термов.#type term = Var of string| Const of string| Comb of term * term| Abs of string * term;;Type term defined.Обратите внимание, вместо двух термов Abs принимает имя переменной и терм.Это сделано для запрещения некорректных термов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
