Лекция 5.

ML

Введение в Функциональное программирование

Джон Харрисон

Университет Кембриджа

10 сентября 2008 г.

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Темы

От λ-исчисления к ML
Энергичное вычисление и его значимость
Семейство языков ML
Запускаем ML
Основы взаимодействия; выражения и объявления
Примеры

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

От λ-исчисления к ML

По ряду причин мы уже добавили некоторые примитивные

возможности в λ-исчисление, например:
Примитивную конструкцию let, чтобы полиморфная система
типов была более мощной.
Оператор рекурсии, чтобы восстановить полноту по Тьюрингу в
типизированном окружении.
Так будет продолжаться до тех пор, пока мы не построим ML.
Особенно интересно, что основные типы данных не реализованы в
виде λ-термов.
Например, преобразование 2 + 2 −→ 4 происходит благодаря
машинной арифметике, а не манипулированию нумералами Чёрча.
Такие дополнительные правила преобразования часто называют
δ-конверсиями.

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Проблема с нормальным порядком редукции

Мы уже сказали, что нормальный порядок редукции («вызов по
имени») является наилучшей редукционной стратегией, потому что
если хоть какая-то стратегия завершается, то эта тоже. Вспомните
пример когда эта стратегия завершается, а другие нет:

(λx. y ) ((λx. x x x) (λx. x x x))

−→ (λx. y ) ((λx. x x x) (λx. x x x) (λx. x x x))
−→ ···

Однако, встаёт вопрос эффективности:

(λx. x + x + x) (10 + 5)

Нормальный порядок редукции даст

(10 + 5) + (10 + 5) + (10 + 5)

Нам придётся три раза вычислять одно и тоже выражение! Было бы

эффективнее сначала вычислить аргумент 10 + 5.
Джон Харрисон Введение в Функциональное программирование
 Лекция 5. ML

Ленивое и энергичное вычисление

Такие повторения вычислений недопустимы на практике. Существует

два решения проблемы, которые делят мир функционального
программирования на части:
Ленивое вычисление выполняет нормальный порядок
редукции, но также использует хитрые способы совместного
использования выражений, сохраняя их в виде графа. При
таком способе выражения вычисляются только один раз и
только когда это понадобится.
Энергичное вычисление просто вычисляет сперва аргументы
(«аппликативный порядок редукции»), и сам программист
должен следить, чтобы не было зацикливаний.
В некотором роде ленивое вычисление элегантнее и мощнее. Однако,
его не так просто реализовать и связать с императивными
возможностями.

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Стратегия вычисления в ML

В ML реализовано энергичное вычисление. Однако, как мы увидим,

есть способы добиться многих преимуществ ленивых вычислений.
Правила вычислений следующие:
Константы вычисляются в самих себя.
Выражения под λ-абстракциями не вычисляются. В частности,
тут нет η-конверсии.
При вычислении комбинации s t сначала вычисляются оба s и
t. Потом, при условии что вычисление s дало λ-абстракцию,
производится самая внешняя β-конверсия, и процесс
повторяется.
Что бы правильно понимать работу ML, важно хорошо усвоить эти
правила вычислений.

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Примеры

(λx. (λy . y + y ) x)(2 + 2)

−→ (λx. (λy . y + y ) x)4
−→ (λy . y + y )4
−→ 4+4
−→ 8

((λfx. f x) (λy . y + y )) (2 + 2)
−→ ((λfx. f x) (λy . y + y )) 4
−→ (λx. (λy . y + y ) x) 4
−→ (λy . y + y ) 4
−→ 4+4

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Условное выражение
Из-за энергичного вычисления нам необходимо создать примитив –
условное выражение с собственной стратегией редукции. Если мы
попытаемся реализовать

if b then e1 else e2

как применение обычного тернарного оператора:

COND b e1 e2

то самые интересные случаи будут зациклены, так как все b, e1 и e2

вычисляются до того, как вычисленное значение b будет
использовано. Рассмотрим:

let rec fact(n) = if ISZERO n then 1

else n ∗ fact(PRE n)

Если мы хотим вычислить fact(0), то нам надо будет вычислить

fact(PRE 0), fact(PRE (PRE 0)) и так далее.
Джон Харрисон Введение в Функциональное программирование
 Лекция 5. ML

Новые примитивы

Из-за энергичного вычисления мы делаем два изменения.

Мы делаем условное выражение примитивом языка и изменяем
стандартную стратегию вычислений для него таким образом,
что сначала вычисляется булево выражение, а потом только
одна соответствующая ветвь.
Мы также немного поменяем правило редукции для оператора
рекурсии. Вместо:
Rec f −→ f (Rec f )
мы используем

Rec f −→ f (λx. Rec f x)

Благодаря этому мы избежим зацикливаний, так так ML не

будет вычислять выражения под λ-абстракцией.

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Семейство языков ML

ML это не один язык. Есть множество потомков первого ML,

который использовался как метаязык в Edinburgh LCF:
Standard ML и SML/NJ
CAML и Objective CAML
Edinburgh ML и Cambridge ML
Lazy ML
Мы будем использовать CAML Light, маленькую и быструю
реализацию языка CAML.
Мы будем использовать возможности, которые легко можно
перевести на другие диалекты ML и другие функциональные языки.

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Запускаем ML

Добавить описание централизованного онлайн доступа к OCaml.

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Взаимодействие с ML
Самый простой способ взаимодействия с ML — это использование
его в роли простого калькулятора.
#10 + 5 ; ;
− : i n t = 15

ML не только печатает результат, но также выводит тип выражения,

в данном случае int. Если ML не может назначить тип выражению,
то оно отвергается.
#1 + t r u e ; ;
Toplevel input :
>l e t i t = 1 + t r u e ; ;
> ^^^^
T h i s e x p r e s s i o n h a s type b o o l ,
b u t i s u s e d with type i n t .

ML знает тип встроенного оператора +, и именно поэтому он может

вывести тип этого выражения.
Джон Харрисон Введение в Функциональное программирование
 Лекция 5. ML

Используем функции (1)

Поскольку ML является функциональным языком, то выражения

могут иметь функциональный тип. Синтаксис ML для обозначения
λ-абстракции λx. t[x] выглядит как fun x -> t[x]. Например мы
можем определить функцию вычисления целого числа, следующего
за данным:
#fun x −> x + 1 ; ;
− : i n t −> i n t = <fun>

Опять же, тип выражения, в этот раз int -> int, был выведен и
показан. Однако сама функция не была показана; система просто
написала <fun>.
Функции применяются к соседним аргументам, как в λ-исчислении:
#(fun x −> x + 1 ) 4 ; ;
− : int = 5

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Используем функции (2)

ML использует синтаксис подобный принятому в λ-исчислении для

каррированных функций от нескольких аргументов.
#(fun x −> fun y −> x + y ) 1 2 ; ;
− : int = 3
#(fun x y −> x + y ) 1 2 ; ;
− : int = 3
#fun x y −> x + y ; ;
− : i n t −> i n t −> i n t = <fun>

Первые две строчки полностью эквивалентны варианту со всеми

скобками:
#(( fun x −> ( fun y −> x + y ) ) 1 ) 2 ; ;
− : int = 3

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Let связывания
Не обязательно вычислять всё выражение за раз. Можно
использовать let связывания:
#l e t s u c c e s s o r = fun x −> x + 1 i n
successor ( successor ( successor 0));;
− : int = 3

Когда связываются функции, можно использовать более элегантную

конструкцию:
#l e t s u c c e s s o r x = x + 1 i n
successor ( successor ( successor 0));;
− : int = 3

Связывания функций могут быть рекурсивными, только добавьте

ключевое слово rec:
#l e t r e c f a c t n = i f n = 0 then 1
e l s e n ∗ f a c t ( n − 1) in
fact 6;;
− : i n t = 720
Джон Харрисон Введение в Функциональное программирование
 Лекция 5. ML

Объявления

В действительности, набор связываний можно пополнять

интерактивно. Просто уберите in и завершите выражение:
#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 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>

Таким образом можно создать набор объявлений функций, которые

позже могут быть использованы в процессе работы.
#s u c c e s s o r 6 ; ;
− : int = 7

Замечание: это не тоже самое что и присвоение переменных!

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Полиморфные функции
Мы можем определять полиморфные функции, такие как оператор
тождественного отображения:
#l e t I = fun x −> x ; ;
I : ’ a −> ’ a = <fun>

ML печатает типовые переменные как ’a, ’b и т.д. Предполагается,

что они являются ASCII представлением для α, β и т.д. Теперь мы
можем использовать тождество с разными типами:
#I true ; ;
− : bool = true
#I 1;;
− : int = 1
#I I I I 12;;
− : i n t = 12

В последнем выражении все вхождения I имеют различные типы и

интуитивно соответствуют разным функциям.
Джон Харрисон Введение в Функциональное программирование
 Лекция 5. ML

Комбинаторы
Вообще, давайте определим все комбинаторы:
#l e t I x = x ; ;
I : ’ a −> ’ a = <fun>
#l e t K x y = x ; ;
K : ’ a −> ’ b −> ’ a = <fun>
#l e t S f g x = ( f x ) (g x ) ; ;
S : ( ’ a −> ’ b −> ’ c ) −>
( ’ a −> ’ b ) −> ’ a −> ’ c = <fun>

Заметим, что система сама следит за типами. Вспомним, что

I = S K K ; давайте попробуем это в ML:
#l e t I ’ x = S K K x ; ;
I ’ : ’ a −> ’ a = <fun>

У него правильный тип, и похоже это работает:

#I ’ 3 = 3 ; ;
− : bool = true

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Равенство функций

Почему бы нам просто не сравнить два варианта оператора

тождества? Вот почему:
#I ’ = I ; ;
Uncaught e x c e p t i o n : I n v a l i d _ a r g u m e n t
" equal : ␣ functional ␣ value "

В общем случае запрещено сравнивать функции на равенство.

Почему? Разве в ML функции не являются объектами высшего
порядка?
Да, но к сожалению, (экстенсиональное) равенство функций
невычислимо. Это следствие из теоремы Райса, или просто из
неразрешимости проблемы останова.
Некоторые версии ML отличают функции от остальных «сравнимых
типов» и фильтруют такие случаи во время проверки типов.

Джон Харрисон Введение в Функциональное программирование

 Лекция 5. ML

Отклонения в проверке типов

Во всех наших примерах система очень быстро выводит наиболее

общий тип для каждого выражения и тип получается простым. Так
обычно и бывает на практике, но бывают и патологические случаи,
например следующий вариант, приведённый в Майерсоне:
let pair x y = fun z −> z x y i n
l e t x1 = fun y −> p a i r y y i n
l e t x2 = fun y −> x1 ( x1 y ) i n
l e t x3 = fun y −> x2 ( x2 y ) i n
l e t x4 = fun y −> x3 ( x3 y ) i n
l e t x5 = fun y −> x4 ( x4 y ) i n
x5 ( fun z −> z ) ; ;

Чтобы вычислить тип этого выражения потребуется порядка 10

секунд, а печать займёт свыше 4000 строк на 80-символьном
терминале.
Не пробуйте дома.

Джон Харрисон Введение в Функциональное программирование