shortly about different ML implementations

>> i hears it used in practice somewhere… but alice definetely needs
>> updating to modern realities and closing bugs.
>> yes, could be worse… and, yes, it’s interesting environment.
> So what implementation of SML would you recommend?

as others already sayed, it depends on your needs.
i’m not expert … but can remember some on all ML versions
(not CAML, it has somewhere different target audience).

hmm, seems i know many… seven!… implementations, besides alice…
looks like with ML you definetely NOT vendor-locked, like with gnat or
evergrowing ghc…

0) so, alice… it’s bytecoded implementation and purposely always will be such (one of project targets is code migration). so it somewhere slow (but has jit) and more or less portable. as i remember, it have some problems with OSes which «not linux» (like xBSD). base sml language in it is greatly extended with parallel and distributed features, with constraint programming (sometimes it very useful), etc. all of that features is not so well-founded and narrow as in smlsharp case.
this implementation is general and «powerful», of course. but you not always need power, sometimes predictability and reliability is preferred. including one solution you deny other solutions. formally verified standards (Standard ML 97) is good… i hear rumors — alice developer now worked in google and making v8 javascript… meanwhile, javascript is bad language, it can’t grow.

1) smlnj. the so named «standard implementation of ML». i use it some, it’s average. it oriented to dynamic, explorating, interactive use. memory images can be stored to file and runned on other computer with same runtime version (or can be packed with runtime forming independent, somewhere big, executable). but smlnj is not for binaries. it’s big, elaborated, interactive environment for small-to-medium programs.
memory consumption is moderate. generates average native code in-memory (MLRISC backend) and so has slower compiling time than mosml, and also has somewhere bigger memory consumption, but faster resulting run times (on par with mlkit). smlnj is not intended for really big heaps.

2) mlton. optimizing compiler. i say it «optimising whole picture, not small peepholes», optimising-at-large. it do less optimisations-in-small than gcc, i think, but apply optimisations-in-big more thoroughly (some peepholes rests unoptimized, sse not used etc). supports parallelism (threads), as is polyml, but in somewhere different way. resulting binaries is self-contained and relatively small (what not used is not included).
…one BIG problem with it — it’s a real memory and processor hog, and always will be. mlton can easy eat gigabytes of memory because of «whole-programness» (that mean including all used libraries) and multiple passes of optimisation transformations in memory. and because of that, it sometimes just can’t be used on old desktops or netbooks. i recommend you setup zswap (packed swapfile) in your linux box for mlton.
peoples recommends to use mlton for compiling release binaries only. some game developers or crossdevelopers use it as such wunderwaffe. but there is one possible trap in «use for final release only». «whole-program»-ness somewhere changes semantic for some SML constructs (like scope for definitions). this can be good (you get efficient functors for free!) or bad. it depends… be warned.

3) polyml. compact interactive system. two files, easily distributed with application. has parallelism. i think internally looks like smlnj (generate native code in-memory), but codegen is smaller and simpler. moderate sequential performance, but people say it has good parallel scalability. it’s main application is isabelle theorem prover. i do not know if polyml GC is parallelized now (that somewhere limited speedup on 4-6 in applications other than symbolic computations with small shared state), but it is actively supported.

UPD: polyml gc is parallelized in last versions so speedup is not so limited anymore. with parallelized gc ML possibly will be faster than haskell. haskell always will have bigger number of sequential parts in runtime (because of it’s lazy-by-default semantic). and so haskell’s speedup will always be more limited than ML’s.
Meanwhile, polyml (in line with mlton and smlsharp), is one of three more or less actively developed ML implementations.

4) mlkit. simple native batch compiler (MLRISC-based codegenerator, as in smlnj). backend optimiser in this compiler is simple and gives moderate quality. sure it not so good in optimisations as mlton, but it more predictable. and has smaller runtime. really great things in this compiler is:
a) region-based memory allocation (compiler optimise some or all work for gc, depending on program, which make it possible to implement realtime and system programs).
i think regions will be very useful if someone tries to implement barrier-based parallel ML in style of JoCaml. possible speedup will be better, i think.
b) separate module compilation! this is really good thing for incremental big project development by several programmers. memory consumption is also much smaller than mlton’s.
try to use it in the middle of development, before releasing with mlton.
…it’s bad, bad that this compiler somewhere forgetted and leaved in shadows ((

UPD: forgive me for some misinformation. MlKit has it’s own, simpler, backend, not MLRISC.
too bad… it supports i386 and hp-pa native targets only. and KAM bytecode generation.maybe somebody wants to bolt MLRISC to mlkit? with some tweaking of runtime this gives to mlkit posibility of running on amd64…

5) moscow ml. simple bytecode interpreter on old caml (wich was before ocaml) runtime. fast compiles, slow runtimes (bytecode, without jit). compact. have separate module compilation!
as i hear, have some problems with float numbers (because tagging?). some admins use it as scripting language and for building small web interfaces. in the past, some peoples use it for theorem provers.
small memory consumption is main goodie of this implementation.

6) hamlet. interpreter of full ml written in ml. useful in teaching and experimenting with language, can be in one big sml file. slow, of course. compile it with mlton.

7) smlsharp. interesting ml native-code (x86 only… that’s bad) compiler. roots of project grows from mlkit as i think (it not related with dotNet and C-sharp) but i not sure.
It’s characteristics is like of mlkit. have good c interoperability. Somewhere polished in fresh, release version. Developers say it has parallelized gc now.
It’s ml language is extended with some enterprise-y constructions like records and such. and, unlike alice, this extensions was _formally verified_ (meanwhile, i personally do not like oop and stupid inheritance, but managers like it). Developed by japan government-founded project, they tries to get language, useful for normal commercial development and specially targeted at low maintenance costs (like Ada was). i ask developers if it will have jvm codegen in future (for more «enterpriseness» which it targets). they reply — «maybe». interesting project, i will look with one eye at it future…

resulting runtime performance grade from fast to slow:
1) mlton (on par with c or even faster)
2) mlkit, smlsharp, smlnj (acceptable, 1.5-2 times from c)
3) polyml (more or less acceptable, 2-3 times from c, but i also hear rumors that _in symbolic computations_ and with big heaps polyml sometimes is very good).
4) alice (i think, somewhere between poly and mosml)
5) mosml (5-10 from c, it’s normal for bytecode)
6) hamlet (slow, you bet)


existentialtype in russian

(transl.note. In the search for «perfect modularity» i found blog of R.H. It was very interesting and fundamental reading so i make translation of this know-what-is-essential-not-what-marketed-now style blog to russian language. I do it for my own and noncommercial use. I was trying all what i can to mimic author speech style and mindset. And also do some (somewhere maybe too long, sorry) clarifying comments on my undestandings of these ideas. Beware, reader!)) If in doubt please consult original blog, because i’m not a professional translator or writer. I’m just hobbyist CS article’s reader))

Note to author. Dear Robert Harper, i e-mail to you a copy of my (Natarov Vladislav Igorevich from Novosibirsk, Russia) hobby translation as i finish it. Do with it ALL what you wish, i.e. attach_to_blog orelse proofread andalso publish orelse send_to_trash andalso forget)) This is least what i can do to pay happy occasion of hearing of some fundamental truths you sayed… )

Перевод блога профессора Роберта Харпера

Экзистенциональный тип (Типы вокруг нас)

  1. О блоге
  2. Приступаем
  3. 15-150: Курс функционального программирования
  4. Обучение новичков функциональному программированию
  5. Не упоминайте о равенстве!
  6. Булевская слепота
  7. Что такое функциональный язык?
  8. Языки и Машины
  9. Параллелизм не значит согласованность
  10. Динамические языки это статические языки
  11. Собака которая не лает
  12. Святая Троица
  13. Функции это значения
  14. Постоянство Памяти
  15. Дохлый пес
  16. Модули важнее всего
  17. Некоторые мысли по преподаванию ФП
  18. Вопрос Ленивости
  19. Само собой в МЛ есть монады!
  20. Семестр завершен
  21. Многомерная теория типов
  22. Трансформации как строгие группоиды
  23. Типы и ячейки
  24. Сердечный приступ
  25. Слова имеют значение
  26. Прозрачность ссылок

О блоге

Меня зовут Роберт Харпер, я один из профессоров факультета компьютерных наук университета Карнеги-Меллона. Я работаю на этом факультете с 1988 года. Основным направлением моих исследований является применение конструктивной теории типов к проектированию и реализации языков программирования а так-же к разработке систем механизации математических преобразований. Полагаю, я более всего известен благодаря своему участию в разработке и реализации языка Стандартный МЛ, введению логического фреймворка ЛФ, а так-же благодаря разработке концепции сертифицирующего компилятора управляемого типами и построенного вокруг типизированных внутренних языков.
Я так-же руководил исследовательскими проектами на темы — компьютерных сетей, научных вычислений, проектирования и семантики языков программирования, грид-вычислений, параллельных научных вычислений, автоматизированной мета-теории для языков программирования, и по теории типов. Я активно участвую в обучении как студентов так и аспирантов. В последнее время я возглавляю группу, занятую пересмотром вводного курса по программированию (прим.перев. 15-150?), который преподается в настоящее время. Мною были написаны (в том числе в соавторстве) несколько книг, включая «Определение Стандартного МЛ», «Программирование на Стандартном МЛ» и, наконец, напоследок «Практические основы языков программирования» (черновик последней доступен в интернете в настоящее время).
Я являюсь членом ACM (АссоциацииВычислительнойТехники), удостоен награды Аллена Ньюэлла за совершенство в исследованиях, а так-же награды Герберта Саймона за совершенство в преподавании, был среди удостоенных награды ACM PLDI «наиболее ключевая статья даже десять лет спустя» и среди IEEE LICS «проверка временем» (за статью, остающуюся важной 12 лет после публикации).

Стандартное предупреждение: Мнения, выраженные здесь и далее, являются личными мнениями автора, и не должны представляться как выражение мнения Университета Карнеги-Меллона, Национального Научного Общества, либо любого другого агенства или организации.


Я собираюсь использовать этот блог для публикации размышлений и стимулирования дискуссии на тему преподавания вводного курса программирования.

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

15-150: Курс функционального программирования

Целью данного курса является введение в теорию и практику функционального программирования (ФП). Ключевым признаком ФП является акцент на обработку путем оценки (прим.перев. выражений в математическом смысле). Традиционное различение программ и данных, типичное для императивного программирования (ИП; ПП — процедурное программирование), заменяется упором на классификацию выражений по типам, которые характеризуют их поведение. Типы включают знакомые числовые (фиксированной и произвольной точности), кортежи и записи(структуры), классифицированные значения (объекты), индуктивные типы наподобие деревьев, функции с заданными аркументами и результатами, а так-же команды, такие как ввод и вывод. Выполнение императивных программ обобщено до оценки хорошо типизированных выражений путем мягкого расширения математических навыков до практики программирования.

Преимущества ФП значительны:

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

Кроме того, ФП обобщает ИП, трактуя команды как формы данных, которые могут быть выполнены ради своих эффектов на среде, в которой они присутствуют. После завершения данного курса, студенты приобретут владение базовыми техниками функционального программирования, включая проектирование программ путем использования типов, разработки программ с использованием техник математической верификации, а так-же эксплуатации параллелизма в приложениях.

Предварительное требование: знакомство с курсом 21-127 «Концепции математики», либо разрешение инструктора.
Студентам потребуется некоторая базовая математическая подготовка, такая как способность провести доказательство методом математической индукции, для того что-бы рассуждать о корректности программ.

Успешное завершение данного курса необходимо и достаточно для поступления на 15-210 «Структуры данных и алгоритмы», который тоже будет строиться на функциональной модели вычислений для того чтобы проработать современную трактовку параллельных алгоритмов для широкого диапазона абстрактных типов.

Обучение новичков функциональному программированию

В этом семестре Дэн Ликата и я совместно преподаем новый курс функционального программирования для первокурсников собирающихся специализироваться на программировании. Этот курс является частью новой вводной программы обучения программированию в УКМ (Университет Карнеги-Меллона, CMU), которая включает в себя так-же новый курс по императивному программированию, созданный Фрэнком Пфеннингом, и готовящийся новый курс по структурам данных и алгоритмам, который будет представлен Гаем Блеллохом этой осенью.

Функциональный и императивный курсы независимы друг от друга, и оба требуются для нового курса структур данных. Оба курса уделяют особое внимание техникам верификации (в основном это инварианты состояния для императивного программирования и структурная индукция для функционального программирования). Новый курс структур данных делает упор на параллельные алгоритмы как наиболее общий случай, и уделяет равное внимание как хранимым так и эфемерным (прим.перев. так называют традиционные процедурные, временные, существующие только в памяти и недолго) структурам данных. Это достигается путем использования выразительного функционального языка (Стандартный МЛ) который содержит механизмы обработки как путем оценки так и изменения (императивно), а так-же поддерживает модульность и абстракцию данных.

Объектно-ориентированное программирование исключено полностью из вводной программы, поскольку оно одновременно и анти-модульно и анти-параллельно по самой своей природе, а потому не годится для современной учебной программы обучения программированию. Предлагаемый новый курс обьектно-ориентированной методологии проектирования будет предложен на втором курсе для тех студентов, которые захотят изучить этот предмет.

Обновление: ревизия программы обучения старших курсов, на которую я тут намекаю, описана в отчете «Вводное обучение программированию в УКМ: Преспективы с точки зрения декана» написанной Рэндалом Е. Брайант, Клаусом Сатнер, Марком Дж. Стелик. Данный отчет обобщает рекомендации специального комитета факультета, отчитывающегося перед факультетом и деканом Школы компьютерных наук.

Не упоминайте о равенстве!

Одна вещь, которой я научился, преподавая программирование, это — то что я выбираю не говорить не менее важно чем то что я выбираю рассказать, по определенной теме. Требуется много усилий в некоторых случаях что-бы научить себя избегать некоторый путь мышления, который, как показала практика, приводит только к ошибкам и заблуждениям студентов. Классическим примером является досадный вопрос равенства, который является источником проблем для судентов и порождает самые разные заблуждения. Мой совет: не упоминайте равенство!

Позвольте мне разъяснить подробнее. Прежде всего, в примитивных языках, таких как Си, нет ни мотивации, ни возможности избежать равенства. Все данные первого порядка, все типы выражений допускают определение равенства за константное время.
Равенство целых не представляет никаких проблем (прим.перев. вообще-то могут быть тонкости знаковое/беззнаковое и разные форматы представления с разными областями значений), однако часто пренебрегают тем что есть (согласно стандарту IEEE) два различных смысла равенства вещественных чисел с плавающей запятой, один из которых не рефлексивен а другой не транзитивен; выберите свою отраву. Указатели должны быть сравнимы не только на равенство, но так-же сравнимы с NULL, что бы это ни значило. (Это, как Тони Хоар сам сказал, «ошибка на миллиард долларов», огромный источник всех привнесенных глюков в языках программирования.) Хотя все это требует некоторой возни, никто не считает что равенство является проблемой в таких языках. Сравнительно говоря, оно и правда не проблема.

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

Так что, если вы соберетесь поднять вопрос равенства, вы вляпаетесь в большие неприятности.
Однако есть альтернатива: просто скажите «нет» равенству. Точнее говоря, не говорите вообще ничего, не вспоминайте о равенстве совсем. Избегая его, вы получите и другой бонус, а именно — сможете избегать Булевских величин (следующий большой источник всяческих привнесенных глюков в языках программирования) полностью, и хорошо если вам это удастся. Я отвлекался от этого обсуждения чтоб написать в другую тему. Теперь, чтоб лишить сил пустую болтовню, позвольте мне сказать что в конце концов вам придется ввести равенство, поскольку оно иногда необходимо, но только на поздней, гораздо более поздней стадии, когда студенты безопасно минуют многие реальные препятствия к тому, чтоб научиться писать хороший, чистый код. Не стоит так-же скатывать бревна им под ноги, вместо этого позвольте им тратить свое время на серьезные вещи.

Многие случаи применения равенства лучше заменить сравнением с образцами. Если у вас есть индуктивно определенный тип, наподобие

datatype nat = Z | S of nat

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

fun plus x y = case x of
Z => y
| S(x’) => S(plus x’ y)

Многие студенты вместо этого пишут:

fun plus x y = if x=Z
then y
else S (plus (pred x) y)

используя pred, определенный до этого, и делают это даже если вы не заикались о равенстве! (Удивительно, чему только не «научатся» дети на улице.) Заметьте! Это не только требует введения дополнительной функции для определения предшествующего числа, но так-же бедный студент лишает себя одного из наиболее ценных инструментов в своем репертуаре, проверки на полноту в механизме сравнения с образцами. (Имеется так-же более тонкая и неприятная вещь — определение pred должно само проверять на Z, в то время как мы знаем, что x не может быть Z в месте вызова pred. Я вернусь к этому вопросу позже, когда будем обсуждать неразбериху между булевскими величинами и логическими предположениями.)

Но что если вы программируете используя машинные целые? Например, как нам определить факториал над типом int в МЛ? Основной прием это использовать концепцию упорядоченного типа которая предоставляется в библиотеке Стандартного МЛ. Это приводит к следующему:

fun fact x = case compare (x, 0) of
LSS => raise Undefined
| EQL => 1
| GTR => x * fact (x-1)

Заметим, что тут все еще нужно находить предшествующее число, однако мы можем избавиться и от этого, затратив чуть больше усилий:

datatype TRI = Neg of int | Zero | Pos of int

fun tri x = case compare (x,0) of
LSS => Neg (x+1)
| EQL => Zero
| GTR => Pos (x-1)

fun fact x = case tri x of
Neg _ => raise Undefined
| Zero => 1
| Pos of x’ => x * fact x’

Рассматриваемое само по себе, это смотрится тяжеловесно, однако на практике все сводится к вопросу проектирования правильных интерфейсов, с которыми далее будет работа, и использованию их к своей выгоде.

Применение тех-же принципов к селекторным типам ясно показывает почему «анализ null-указателей» такая глупая идея. Предположим что переменная x имеет тип t option для некоторого типа t. Вместо того что-бы писать

if x=NONE then raise NullPtrException else …

при котором не-NONE статус x не распространяется в else-ветку, взамен этого мы пишем более чистый селектор образцов

case x of
NONE => raise NullPtrException
| SOME x’ => …

в котором второе предложение x’ имеет тип t а не t option, и потому ни при каких условиях не может быть NONE!

Булевская слепота

Ненавижу булевские величины! Но разве не все в конце концов «просто биты»? Разве компьютеры не построены из триггеров? И разве триггеры не просто логические связки? Как только возможно для программиста ненавидеть булевские величины?

Фритц Хенглейн недавно сказал мне что мир теоретического программирования разделен на два лагеря, которые я назову логиками (занимающимися языками и семантиками) и комбинаторщиками (занимающимися алгоритмами и вычислительной сложностью). Логики обожают доказывать что программы работают правильно, комбинаторщики любят подсчитывать за сколько шагов программа «делает правильно». Причем, забавно, логики ненавидят булевские величины, и любят абстракции, такие как деревья или потоки, в то время как комбинаторщики обожают биты и ненавидят абстракцию! (Или по крайней мере так часто кажется; простите мне мою риторику.)

Моя точка зрения такова. Булевские величины это всего лишь один, исключительно (или, возможно, двоично) занудный, тип данных. Булево значение b, оно либо истина, либо ложь; более ничего. Булевское не несет в себе никакой информации кроме своего значения, в этом и затык. Как Конор МакБрайд это сформулировал, что-бы использовать булевское значение, вам потребуется знать еще его происхождение так чтоб вы могли знать что оно означает.

Булевские величины почти все время (в программистской литературе и книгах) путают с пропозициями, которые выражают логические утверждения или делают заявления.

Для утверждения p быть истинным значит что у него есть доказательство; это такая доступная, разумная аргументация на тему того почему p имеет место. Для утверждения p быть ложным значит что у него есть опровержение; обычно это контрпример показывающий почему p не имеет места быть.

Разница здесь очень тонка. Решение о том что утверждение p истинно это не то-же самое что говорить что p равно истине, так же и решение о том что p ложно это не то-же самое что сказать что p равно ложь! Фактически, не имеет даже смысла задавать вопрос, равно ли p истине, поскольку первое есть пропозиция (утверждение), в то время как второе есть булевское (значение данных); они разных типов.

В классической математике, где о вычислимости не беспокоятся, возможно путать понятия булевских и пропозиций, так что в том мире есть только два утверждения, истинное и ложное. И роль доказательства лишь показать что имеющееся утверждение есть один из этих двух случаев, равно одному из них. Все это хорошо и замечательно, при условии что вас не интересует само вычисление того, истинно нечто или ложно. Как только вас это заинтересует, вам придется ухватить разницу между общим утверждением, чья истинность может не быть определена, и булевской величиной, которая всегда может быть вычислена так или иначе. Однако затем, как упоминалось ранее, мы должны будем связать ее с утверждением, формулирующим, что эта булева величина означает, специфицирующим ее происхождение. Как только мы сделаем это, мы обнаружим что булевские величины не имеют специального статуса, и в любом случае обычно плохой выбор в качестве структуры данных, поскольку приводят к состоянию, которое Дэн Ликата называет булевской слепотой.

Хорошим примером будет тест на равенство, e=e’, для булевских величин. Как мы обсуждали ранее, такая казалось бы невинная функция привносит серьезные усложнения, в частности в абстрактных языках с богатой системой типов. Она так-же демонстрирует стандартную путаницу между утверждением и булевской величиной. Как предполагает ее тип, операция проверки на равенство есть функция, которая возвращает истину или ложь в соответствии с тем, равны ее аргументы или нет (в смысле, определяемом типом этих аргументов). Хотя нотация провоцирует путаницу, выражение e=e’ не есть утверждение гласящее что e и e’ равны! Вместо этого оно есть структура данных, имеющая одну из двух форм, либо истинную либо ложную. Тест на равенство это функция, имеющая такое свойство что если она возвращает истину то ее аргументы равны (связанное логическое утверждение равенства истинно), а если она возвращает ложь то ее аргументы не равны (связанное логическое утверждение равенства ложно), и кроме того, данная функция непременно возвращает либо истину либо ложь для всех входных данных. Кажется сначала что это разница в волосок, но это не так! Для дельнейшего рассмотрения, прежде всего заметим, что тест на равенство может быть записан в другом синтаксисе, возможно e==e’ или (equal? e e’) или в любом количестве других нотаций. Эте делает очевидным, надеюсь, что отношение между функцией и связанным логическим утверждением должно быть явно выражено некоторыми другими способами; функция и утверждение — разные вещи. Более интересно, что та-же функциональность может быть выражена разными способами. Например, для частично-упорядоченных типов мы можем записать e<=e' andalso e'<=e или что-то вроде этого, удовлетворяя той-же спецификации, что и наша невинная маленькая функция "знак равенства". Связь между функцией и утверждением тут слабее, и так-же она будет слабее у многочисленных других вариаций которые вы можете накрутить для себя сами.

А что такого плохого в том что-бы устраивать такую путаницу? Возможно, наибольший ущерб в том, что запутывается фундаментальное отличие, и это несет за собой самые разные виды плохих последствий. Например, студент может разумно спросить, почему равенство не определено на функциях? В конце концов, в доказательстве, проведенном мною недавно, я давал тщательную аргументацию методом структурной индукции что две функции равны. А теперь я говорю обратное и утверждаю что равенство не определено над функциями! Ради Бога, о чем я вообще разговариваю? Так вот, если вы привлечете соответствующее отличие, у вас не будет вопроса. Конечно, имеется хорошо определенная концепция математического равенства двух функций;оно, в общем случае, требует доказательства. Однако не существует хорошо определенной вычислимой функции, которая возвращает истину если две функции (над целыми числами, скажем) равны, или возвращает ложь в противном случае. Таким образом, хотя «=» : (int->int)*(int->int) -> prop выражает равенство, однако «=» : (int->int)->(int->int)->bool все-же не способна удовлетворить только что данной предыдущей спецификации. Либо, глядя с другой стороны, вы не можете проверять равенство пропозиций! (И хорошо что нет.)

Другой ущерб от путаницы это состояние Булевской слепоты, упоминавшееся ранее.
Предположим, что я вычисляю выражение e=e’ что-бы проверить равны ли e и e’. У меня в руке один бит. Бит сам по себе не имеет внутреннего смысла; я должен связать происхождение с этим битом что-бы дать ему смысл.
«Этот бит будучи истинным означает что e и e’ равны, поскольку этот вот другой бит будучи ложным означает что некоторые два других выражения не равны.» Отслеживание такой информации ( или попытки восстановить ее используя любое количество технологий анализа программного кода ) представляет собой известную трудность. Единственная вещь, которую вы можете сделать с битом, это провести по нему ветвление, и очень скоро вы потеряетесь в чаще if-then-else-ов и потеряете представление что есть что.
Немного поразвивайте программу, и вскоре вы потеряете из виду берега и обнаружите себя находящимся в поиске своего любимого SAT-решателя что-бы определить, какого … тут вообще твориться.

Однако это лишь еще один пример привнесенных глюков! Проблемой является вычисление бита прежде всего остального. Как только вы это сделали, вы ослепили себя, уменьшив доступную себе информацию до бита, а затем пытаетесь восстановить эту информацию позже, вспоминая происхождение этого бита. Характерный пример был рассмотрен в моей статье по равенству:

fun plus x y = if x=Z
then y
else S(plus (pred x) y)

Здесь мы разрушаем информацию, которую мы имеем об x, до одного бита, затем делаем ветвление по нему, затем нам приходится восстанавливать информацию которую мы потеряли чтоб оправдять вызов pred, которая типично не может восстановить тот факт что ее аргумент ненулевой и ей приходится самой это проверять чтоб быть уверенной. Что за бардак!

Вместо этого мы должны написать

fun plus x y = case x of
Z => y
| S(x’) => S(plus x’ y)

Нет нужды в булевских величинах да и код стал получше! В частности, мы получаем предшествующее значение мимоходом, и у нас нет нужды отслеживать происхождение никаких битов.

В качестве упражнения, убедите себя что весь бизнес «анализа null-указателей», бессмысленен, по тем-же самым причинам! Есть мало вещей в мире, более глупых чем код, который сравнивает указатель на равенство с null, затем делает ветвление по результату проверки, затем обнаруживает что ему нужен SAT-решатель или Проверяльщик моделей чтоб распространить происхождение булевской величины которая прежде всего просто не должна была вычисляться!

Что такое функциональный язык?

В предыдущем сообщении я упоминал что разрабатываю новый курс по функциональному программированию для студентов-первокурсников. Моментальный вопрос, который никто из вас не задал, звучит так — «что вы имеете ввиду под функциональным программированием?».

Хороший вопрос! Теперь, если только у меня будет блестящий ответ, я буду считать себя в хорошей форме.

Говоря социально, первая проблема которая мне встретится это фундаментальное непонимание насчет термина «функциональное программирование». Большинство людей полагают, что это обозначает идеологическую позицию, которая представляет собой оппозицию к тому что все остальные думают и делают. Таким образом, в мозгу типичного коллеги, когда я говорю о функциональном программировании, она слышит «ненормальная религиозная доктрина» и «знает» инстинктивно что надо игнорировать ее.

В то время как то что я подразумеваю под функциональным программированием включает все то что все прочие делают, как частный случай. Вконце концов, как читателям этого блога несомненно известно, нет лучшего императивного языка чем функциональный язык! Фактически, я часто говорю, что Хаскелл является лучшим в мире императивным языком программирования; при этом я лишь наполовину (а то и меньше) шучу.

Выходит, если функциональное программирование включает императивное программирование, то о чем я вообще тогда разговариваю когда продвигаю функциональное программирование для обучения первокурсников? И почему, к тому-же, у нас еще имеется курс императивного программирования? Очень хорошие вопросы. Я не уверен что у меня есть полностью обоснованные ответы, однако это всего лишь блог, где я могу просто вывесить свои мнения (прим.перев. вывесить без обоснования. тут, как легко понять, автор подкалывает любителей вести блоги а не писать статьи, не особо заботящихся об обосновании того что они пишут. экономя усилия для себя они перекладывают заботу о фильтрации мусора снова и снова на каждого из десятков тысяч своих читателей).

Если бы все зависело только от меня, у нас бы был лишь один вводный курс, возможно длительностью два семестра, по программированию, который бы, конечно, уделял внимание как функциональным так и императивным техникам, все в пределах одного языка.

Лично мне кажется что этот путь был бы правильный, подготавливал бы студентов для всех дальнейших курсов нашей программы обучения, а так-же для работы там, в «реальном мире». Не все верят мне ( иногда я и сам себе не верю ), поэтому мы пришли к компромиссу. В то время как это конечно звучит полностью замечательно и глобально, обучать как императивному так и функциональному программированию, реальность такова что мы обучаем лишь старым и новым методам программирования. Важна не столько сама императивная часть, скорее ее моральная устарелость. Считается важным (и, по честному, я могу видеть ценность этого аргумента) чтоб студенты учили «старые способы» поскольку именно так устроено сейчас большинство остального мира. Так что нам приходится использовать язык, который неправильно определен (допускает программы не имеющие никакого смысла в терминах самого языка), который принуждает к последовательному а не параллельному мышлению, который требует ручного выделения памяти, который приносит самые разные виды сложностей, наподобие null-указателей, но без которых вообще можно было обойтись. А затем нам приходится учить о вещах называющихся «тулсы» которые помогают нам разгрести бардак который мы-же и создали. Тулсы, которые делают вещи типа излечения от Булевской слепоты или проверяют на ошибки в работе с null-указателями. Вообще говоря, эти тулсы-средства полностью восхитительны, и так-же поражают воображение как первые станки, печатающие по способу горячего литья, или паровые локомотивы.

Так что такое тогда функциональный язык? Я не придумал ничего лучшего, кроме как перечислить некие критерии, которые важны для того, чем я занимаюсь; языки которые удовлетворяют этим критериям, обычно называются функциональными языками, поэтому так-же буду называть их и я.

  1. Язык должен иметь хорошо определенную семантику, выраженную в терминах программ, которые мы пишем, а не в терминах того как они «компилированы» на некую гипотетическую аппаратно-программную платформу. Я хочу быть способен рассуждать о коде который я пишу, а не о том коде который пишет компилятор (прим.перев. это важный момент — наличие простой абстрактной точки отсчета для рассуждений. так-же обратите внимание что баги в современных компиляторах, особенно в оптимизирующих — далеко не редкость. ведь большинство из компиляторов не верифицированы, см. compcert. потому и нам от тестирования своих программ редко удается избавиться полностью). Я так-же хочу определять смысл моей программы в терминах используемых мною конструктов, а не в терминах некоего предполагаемого внутреннего механизма который их реализует. Это и составляет смысл абстракции.
  2. Он должен поддерживать обработку путем оценки и обработку путем исполнения. Оценка это плавное обобщение школьной и высшей математики, и определяется в терминах стандартных математических концепций таких как кортежи, функции, числа и так далее. Переменные получают значение путем подстановки, а оценка заключается в упрощении выражений. Исполнение же есть действие программы над другим агентом или структурой данных, которая предположительно существует независимо от самой программы. Данные живут «тут» а программа «оттуда» халтурит с этими данными. Назначаемое (мой термин для того что в императивных языках неправильно называют переменными) получает значение путем операций извлечения и помещения (get/fetch и put/store), а не путем подстановки. Исполнение состоит из осуществления этих операций.
  3. Должно быть вполне удобно рассматривать как хранимые (прим.перев. иногда говорят персистентные) так и эфемерные структуры данных. Это в сущности переформулировка предыдущего пункта 2. Хранимые структуры данных это значения, с которыми можно работать как и с любыми другими значениями, невзирая на их очевидный «размер» или «сложность». Мы можем так-же легко передавать функции как аргументы и возвращать их результатами, как мы делаем эти вещи с целыми числами. Мы можем думать о деревьях или потоках как о значениях, в одной манере. Эфемерные структуры данных это те, которым вы учились по книгам. Они внешние по отношению к программе и обрабатываются деструктивно путем исполнения. Они полезны, но далеко не настолько центральны как нынешние книги могли бы заставить вас поверить (поскольку в них не рассматриваются никакие другие).
  4. Язык должен иметь естественную параллельную стоимостную модель, основанную на зависимостях между вычислениями, так чтоб кто угодно мог рассуждать о параллельных алгоритмах и их сложности так же естественно как они сейчас обсуждают последовательные алгоритмы. Чисто-императивные языки программирования к сожалению не удовлетворяют этому критерию, поскольку с ними слишком много неявных зависимостей между компонентами обработки, в результате которых вы принуждаетесь к последовательности обработки через искусственные ограничения императивного мышления.
  5. Язык должен иметь богатую структуру типов, которая допускает введение новых абстрактных типов и которая поддерживает модульную разработку программ (прим.перев. очень немногие языки программирования поддерживают нормальную модульность, чаще есть лишь пародия на нее, не дающая нужной степени изоляции, зато имеющая всякие попсовые навороты типа ООП). Мало уделяя внимания выражениям и их оценке, императивные языки содержат хилое понятие типа и не помогают модульности.
    Что хуже, объектно-ориентированное программирование, являющееся подвидом императивного программирования, принципиально антимодульно поскольку абсурдно акцентируется на наследовании и полагается во всем на классовые структуры, в которых функциональность прорастает через всю программу как раковая опухоль, размазываясь по ней.

Какие же языки удовлетворяют этим критериям лучше всего? В основном, МЛ (и Стандартный МЛ и Объектный Камл, если забыть про «объектную» часть), а так-же Хаскелл.
(К сожалению, у Хаскелла проблемы с моделью стоимости, о чем будет еще разговор.)

Вот поэтому мы и преподаем МЛ.

Языки и Машины

Модели вычисления могут быть разделены на две категории, лямбда-исчисление, и все остальные. Ну, возможно, системы продукций Поста и уравнения Гербранда-Геделя тоже относятся к первой категории, однако безусловно что все хорошо известные и широко применяемые модели, такие как машины Тьюринга или машины произвольного доступа к памяти, находятся довольно далеко от лямбда-исчисления. Гай Блеллох определил это различие как между языками и машинами. Машинные модели все основаны на идее ограниченного управления, дополненного неограниченной памятью. На программиста возложена ответственность управлять памятью таким образом, чтоб реализовать все более структурированное чем бит, и нет способа кроме как через интерпретатор, для изменения программы во время исполнения; машинные модели все несомненно не фон-Ньюмановские, поскольку в них отсутствует идея хранимой программы. Единственная модель, основанная на языке, напротив, не отделяет программу от данных, и предлагает основу на которой могут быть построены реалистичные языки, напрямую и без кодирования.
Это будет похоже решающим преимуществом для лямбда-исчисления: несмотря на то что машинные модели рассматриваются в первых главах наших книг, они в основном не имеют практического значения, в то время как лямбда-исчисление непосредственно полезно для программирования и автоматизации логических систем. И тем не менее, все еще именно машинные модели доминируют, особенно в мире алгоритмов и вычислительной сложности, а лямбда-исчисление остается известной лишь посвященным загадочной штучкой, которая изучается лишь меньшей частью компьютерщиков-теоретиков. Как такое могло случиться?

Будучи поставлены перед этим вопросом, мой типичный коллега (по крайней мере, из теоретиков) снимает вопрос как полностью неинтересный, поскольку «все модели вычисления эквивалентны с точностью до полиномиального временного коэффициента», так что кого волнует этот вопрос?

Ну, если ваша работа вся делается с точностью до полиномиального фактора по сложности, и вас волнуют лишь вычисления с натуральными числами (или другими финитными объектами), то я полагаю это действительно не имеет значения. Один раз и навсегда вы описываете как интересующие вас объекты отображены на некую модель, и оставляете их так; детали просто не имеют значения.

Но очевидно модели всеже имеют значение, что наблюдается по неизбежному факту, что тот-же самый коллега никогда ни при каких условиях не рассматривает ничего кроме классической машинной модели как фундамента для своей работы! Конечно, если уж они все эквивалентны, то это не может иметь значения, так что мы все можем переключиться на лямбда-исчисление, правильно? Ну, хотя что-то верное в этом есть, я могу убедить вас что ваши аргументы вас никуда не ведут. По-видимому, в конце концов некоторые модели «более эквивалентные» чем другие! Почему такое возможно?

Одна из причин это то что много работ все-же не укладывается в полиномиальный фактор (некоторые даже могут подозревать что большинство не укладывается). Так что для этих целей модель имеет значение. С другой стороны, никто не использует на самом деле «официальных» моделей в своей работе. Никто не пишет код для машины Тьюринга чтоб описать свой алгоритм, не пишет даже и обычного машинного кода (Кнут погоды не делает). Вместо этого они пишут то что очаровательно называется птичий Алгол, или птичий С, или подобную императивную программную нотацию. Другими словами, они таки используют программный язык, а не машину! Собственно, они должны. Но тогда почему такое внимание придается машинным моделям? И что этот птичий язык, который они пишут, означает?

Ответ таков что язык определяется путем трансляции (компилятором) которая определяет что такой-то и такой-то птичий Алгол соответствует такому-то и такому-то машинному коду или коду машины Тьюринга. Описание естественно неформальное, однако достаточно точное чтобы вы ухватили суть.

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

Тогда зачем такой неловкий подход используют с такой настойчивостью? Одна причина, очевидно, традиция. Если это было неплохо для моего наставника, будет неплохо и для меня.

Другими словами, если хочешь чтоб тебя опубликовали, то лучше пиши в стиле, знакомом для людей принимающих решения.

Более существенная причина, однако, в том что машинные модели являются базисом для определения стоимости вычисления. «Шагом» вычисления определяется машинный шаг, и мы сравниваем алгоритмы путем оценки количества шагов которые они предпримут для решения одной и той-же проблемы (с точностью до мультипликативного фактора, в большинстве случаев). Как только мы можем провести «ручную компиляцию» с птичьего Алгола на машинный код, мы можем назначить стоимость программам написанным на языке выше уровнем чем ассемблер, и мы можем делать разумные сравнения между алгоритмами. Эта методология служила нам неплохо, но начинает уже ломаться (одна из причин этого параллелизм, но есть и много других; дискуссия на эту тему оставляется пока до другого удобного случая).

Этой методологии есть альтернатива, заключающаяся в предоставлении стоимостной семантики непосредственно для языка на котором мы пишем, и проводить свои анализы непосредственно от этого базиса, без обращения к компилятору или отсылки к нижележащей машине. Короче говоря, мы принимаем лингвистическую модель вычислений вместо машинной, и жизнь становится лучше! Имеется много способов для выражения алгоритмов, и мы сократим историю того как алгоритмы будут анализироваться.

Что-бы сделать это, требуется чтоб мы дали стоимостную семантику языку который мы действительно используем. Именно тут лямбда-исчисление вступает в игру, поскольку является типичным примером того как задавать языковую модель вычислений. Вкратце, основное понятие в лямбда-исчислении это концепция редукции, записываемая как М->М’, выражающая один шаг вычислений программы М и выдающая в результате программу M’. Исполнение определяется непосредственно над программами которые мы пишем, и модель предоставляет хорошо определенное понятие вычислительного шага, которые мы можем подсчитывать, чтоб получить временнУю сложность программы. Десятилетия опыта показывают что этот подход масштабируется до реалистичных языков.

Что не нравится? Лично я без понятия. Я был озадачен подозрением с которым лямбда-исчисление похоже принимается в алгоритмических кругах. Практически любая машинная модель принимается как замечательная основа, в то время как ситуация в отрасли показывает что машинные модели имеют ограниченную применимость для работы которая действительно делается!

Единственная причина которую я могу придумать (без учета могущественных социальных причин), это то что имеется давнее, в то же время полностью безосновательное, сомнение в том может ли концепция стоимости возникающая из лямбда-исчисления быть пригодна для анализа алгоритмов. (Один исследователь недавно сказал мне «да вы можете спрятать слона внутри бета-редукции!», правда он при этом так и не смог объяснить мне в чем я был неправ.) Единственный путь оправдать свое заявление это определить, раз и навсегда, компилятор из лямбда-исчисления в машинный код который ясно покажет что абстрактные шаги лямбда-исчисления могут быть реализованы за константное время на машинах с произвольным доступом к памяти (в том смысле что не будут зависеть от размера входных данных, только от размера статической программы). Блеллох и Грейнер провели как раз этот анализ в своей конструктивной работе в ранних 90-х; ищите подробности в работах Гая.

В следующем сообщении я немного разовью эти идеи и покажу (объясняя работу Блеллоха) что лямбда-исчисление служит хорошей моделью не только для последовательных алгоритмов, но так же и для параллельных! И что мы сразу можем расширить модель до языков с важными абстракциями такими как функции высокого порядка или исключения (эксепшны), без того чтоб подвергать риску ее полезность для выражения и анализа алгоритмов.

Параллелизм не значит согласованность

(прим.перев. concurrency, в русском языке что-то не могу припомнить специального термина для того о чем он говорит, у нас эти понятия вообще похоже слиты вместе в «параллельности», а зря. выбрал «согласованность» как более отражающую смысл чем «одновременность»)

В одном из предыдущих сообщений я упоминал что одной из целей нового вводного курса по программированию в УКМ было преподавать параллелизм как типичный случай обработки, а не как загадочный специализированный предмет для продвинутых студентов. Многие люди настроены весьма скептически когда я говорю им такое, поскольку это немедленно вызывает в их мозгу мириады заморочек согласованности: блокировки, мониторы, тупики, обедающие философы, … И так-же если вы взглянете на современную научную литературу, вы увидите бессчетное число статей вида (а) параллелизм важен так что (б) поговорим о согласованности. Ситуация зашла настолько далеко что мне кажется что нынче большинство компьютерщиков-теоретиков вообще не способны различить эти две концепции. (Или возможно они сознательно путают эти две вещи чтоб обосновать финансирование работ над согласованностью взывая к важности параллелизма.) (прим.перев. предположение может быть не лишено оснований. люди вообще склонны больше делать вид а не работу, потому что это им легче. особенно если получают не за качество результата. поэтому области в которых можно накрутить на пустом месте необязательную сложность, так «развиты», взять то-же ООП. Или распараллеливание, которое действительно можно подавать сложно, через неудобные нити и ручные синхронизации. При том что параллелизм по данным это давно и полностью решенная задача. А в комплекте с подходом вроде «будущих», то есть связанных потоками данных этапов вычислений, вообще покрывает 99% задач распараллеливания. Мда, ИТ это эльдорадо для «распильщиков» бюджетов, здесь неоправданные материальные расходы на сложность поначалу незаметны а потом обязательны.)

С учетом такого состояния дел, я не в состоянии объяснить что мы делаем в УКМ (для тех кто до сих пор не знает) без предварительной перезагрузки вас. Поверьте мне, я действительно жму Ктрл-Альт-Дел и затем щелкаю Рестарт. Итак, мы загрузились.

Первая вещь которую нужно понять это то что параллелизм не имеет ничего общего с согласованностью. Согласованность имеет дело с недетерминированной компоновкой программ (или их компонент). Параллелизм занимается вопросами асимптотической эффективности программ с детерминированным поведением.
Согласованность это все что относится к управлению неуправляемым: события прибывают из-за причин лежащих вне нашего контроля, и мы должны на них реагировать. Пользователь щелкает мышкой, менеджер окон должен прореагировать, вовремя хотя дисплей тоже требует внимания. Такие ситуации по своей природе недетерминированы, мы пытаемся решить их с помощью введения формального недетерминизма, который по своей сути детерминирован, изображая что компоненты сигналят событиями в произвольном порядке и что мы должны отвечать на них когда они возникают. Недетерминированная компоновка это мощная идея структурирования программ. Параллелизм, с другой стороны, занимается лишь зависимостями между подвычислениями детерминистического вычисления. Получение результата не подвергается сомнению, однако есть много способов достичь его, и некоторые более эффективны чем другие. И мы хотим использовать эти возможности к своей выгоде.

Теперь я слышу как вы возражаете — разве не согласованность требуется чтоб реализовать параллелизм? Ну, часто да, однако согласованность так-же требуется для реализации и последовательного выполнения тоже! Сигнал генератора частоты в вашем процессоре представляет собой в сущности механизм синхронизации, с помощью которого координируется независимая деятельность компонент процессора. (Да, я в курсе что есть асинхронные процессоры, но это лишь делает мои утверждения еще более сильными, вы по прежнему нуждаетесь в механизмах управления согласованностью.) Смысл в том что согласованность не имеет отношения к параллелизму, даже если инженеры которые проектируют наши параллельные вычислительные платформы должны иметь дело с согласованностью.
Другой способ сказать ту-же самую вещь это то что параллелизм это полезная абстракция, и что абстракции никогда не должны быть перепутаны со своими реализациями. (Числа это конечно не множества, но могут быть реализованы в терминах множеств. И так далее.)

Ну чтож, все хорошо и замечательно, параллелизм это не согласованность, но что он есть? Какова подходящая модель для параллельных вычислений? Как и в последовательном случае, есть два ответа, машинный подход и языковой подход. Я собираюсь критиковать машинный подход, и приводить доводы в пользу языкового подхода на двух основаниях: (а) он сам по себе более элегантный и естественный и (б) его можно преподавать студентам сразу, без всякой суеты и беспокойства. Большинство из того что я скажу, происходит от конструктивных и прекрасных работ Гая Блеллоха, которые я впитал за годы сотрудничества. В той степени в которой я их верно понял, прошу ставить это в заслугу Гаю; в той где я что-то не понял, вините меня.

Каноническая машинная модель параллелизма это ПРАМ, или Параллельная РАМ (прим.перев. параллельная машина с произвольным доступом к памяти, ППДП), которая обобщает классическую РАМ модель и разрешает ей иметь р>0 процессоров, которые разделяют доступ к общей памяти. Есть много вариантов на тему ПРАМ, в зависимости от того какие виды взаимодействий позволяются и как конфликты разрешаются между процессорами. Для нашего обсуждения различия между ними не важны, так что я не буду пытаться классифицировать эти разновидности тут. Ключевая идея во всех это то что р, число процессоров, не может увеличиваться, результаты выражаются в терминах того как эффективно алгоритм выполняется на р-процессорной ПРАМ в зависимости от n, размера входных данных. Это неплохо подходит как стоимостная модель для параллельного исполнения, однако совсем никуда не годится как модель программирования!
Что-бы писать код для ПРАМ, вы фиксируете количество процессоров, и пишете код для этого количества процессоров (часто отличающиеся случаи «аналогичны», но в реальности вам все-же приходится фиксировать р и писать код для этого фиксированного р). Более того, вы обязаны (официально, как бы то ни было) писать низкоуровневый императивный код РАМ, который вносит избыточные зависимости между подвычислениями из-за того что явно планирует шаги вычисления. Это ужасающе!
Конечно обычно каждый пишет птичий С и прикидывает как он будет скомпилирован, но факт в том что вы все еще пишете последовательный, императивный код для того чтоб реализовать параллельный алгоритм.

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

Образцовым примером является БыстраяСортировка, естественно параллелящийся алгоритм. Многие люди полагают что основная идея быстрой сортировки заключается в технике обмена-на-месте, которую Хоар изобрел в первоначальном определении своего алгоритма. Я утверждаю, что это лишь деталь реализации; основная идея алгоритма это то что он параллелится (прим.перев. стандартный прием и решения сложных задач и распараллеливания, разделяй-и-властвуй). Что-бы заметить это, мы должны работать на правильном уровне абстракции: функция сортировки переупорядочивает непустую последовательность элементов (которые можно сравнивать) что-бы получить другую последовательность которая будет обладать свойством упорядоченности.

fun qs xs =
if |xs|=1 then xs
else let
val (xsl, xsg) = split xs
in concat (qs xsl, qs xsg)

То есть, мы делим последовательность на две части (по какому-то принципу), такие что все в левой части меньше чем все в правой, затем упорядочиваем части независимо (и параллельно!) и затем объединяем результаты вместе. Точная сложность БыстройСортировки зависит от представления последовательностей и от сложности операций над ними. Пока что давайте просто проскочим это что-бы сосредоточиться на общей структуре вычисления. Если мы можем быть уверены что последовательность делится примерно пополам (любым удобным способом, включая рандомизацию), тогда рекурсия будет логарифмической глубины. На каждой стадии мы делаем линейную работу, но рекурсивные вызовы независимы друг от друга. Алгоритм имеет естественную структуру разветвиться-объединиться, в которой мы (а) делим последовательность на две части, (б) параллельно сортируем две части, и (с) объединяем результаты вместе. (Разбиение и само может делаться параллельно, но мы об этом тут не будем беспокоиться.)

Анализ БыстройСортировки разбивается на две части, работу и глубину (или размах). Работа это общее количество шагов требуемое что-бы выполнить алгоритм. Для последовательности длины n, мы выполняем O(n log n) шагов что-бы упорядочить последовательность, как возможно и ожидалось. Это последовательная сложность, количество времени, которое займет выполнение программы на одном процессоре.
Что-бы учесть параллелизм, имеется вторая единица измерения, называемая глубина, которая измеряет длину критического пути вычисления, то есть длину наибольшей цепочки зависимостей между подвычислениями. Не имеет значения сколько параллелизма нам может быть доступно, мы никогда не найдем решение быстрее чем за величину глубины; оно представляет идеализированную параллельную сложность алгоритма, минимальное количество времени, которое он всегда займет сколько ему процессоров не давай.
В зависимости от выбора структур данных, глубина БыстройСортировки O(log^2 n), или что-то вроде того, что делает ее достаточно неплохо параллелизуемой. (Заметьте что, как и в нашей предыдущей дискуссии, шагом вычислений является переходной шаг в операционной семантике языка, который мы используем для выражения алгоритма.)

Это все очень хорошо и элегантно, однако теперь подходит действительно прекрасная часть, концепция доказуемо гарантированной реализации языка. (Слово «доказуемая» используется здесь только из-за жалкого состояния дел в отрасли; наличие доказательства что ваша реализация работает, и насколько хорошо она работает, остается чем-то редким среди того что упоминается, в то время как должна быть скорее обязательна для приведения любым уважающим себя программистом.) Идея в том что языковая модель может быть реализована на ПРАМ (с определенными свойствами межпроцессорных связей, о которых тут рассказывать не будем) в гарантируемых пределах по стоимости, которые учитывают накладные расходы планирования на р-процессорное параллельное устройство. Поэтому, р не требуется задавать заранее, вместо этого оно определяется средой времени выполнения (прим.перев. runtime) языка и компилятором, как показывается в доказательстве теоремы.

Теорема. Вычисление с работой w и глубиной d может быть реализовано на р-процессорной ПРАМ за время O(max(w/p, d)).

(Иногда второй фактор d log p, это зависит от наших предположений об устройстве целевой ПРАМ.)

Эта теорема называется Принципом Брента, и формулирует вполне очевидный факт.
Прежде всего, мы никогда не сможем выполнить программу глубиной d менее чем за d шагов. Глубина это длина критического пути; это количество времени которые мы обязаны будем прождать пока выполняется алгоритм, независимо от доступного параллелизма.
Во-вторых, в той мере в которой параллелизм возникает из структуры зависимостей (независимостей) вычисления, в лучшем случае мы можем делать р единиц работы одновременно, держа все процессоры занятыми до тех пор пока все не сделаем.
Вот и все!

Степень эффективности языковой модели параллелизма лежит целиком в ее способности показывать структуру зависимостей вычисления путем избегания введения любых других зависимостей, которые не наложены на нас природой самого вычисления. Ключом к этому является функциональное программирование, которое обнаруживает себя здесь в трансформационном подходе к вычислению: сортировка задумывается как математическая функция, которая трансформирует данную последовательность в другую последовательность. Она не разрушает данную последовательность, не более чем сложение двух чисел разрушает эти два числа! Поскольку БыстраяСортировка это математическая функция, нам не нужно беспокоиться что выполнение qs xsl пересечется с (или будет зависеть от) qs xsg; мы сразу можем запускать их параллельно без опасений насчет неблагоприятных последствий. Результат таков что тут намного меньше зависимостей между подвычислениями, и поэтому намного больше возможностей для параллелизма, которые могут быть использованы, в согласии с принципом Брента, когда планируется выполнение на параллельном вычислительном устройстве.

Заключение после всего вышеизложенного таково что функциональное программирование имеет первостепенную важность для параллелизма. Вот почему (это главная причина) мы преподаем функциональное программирование первокурсникам в УКМ. И это основная причина почему мы на это способны. В этом ничего такого нет, просто пишите программы так же как делаете математические выкладки, и параллелизм сам о себе позаботится!

Обновление: Саймон Марлоу (прим.перев. какой-то хаскилятор известный вроде… не помню, их там больно много и каждый круче всех других )) ) высказывал мысли похожие на мои некоторое время назад.

Динамические языки это статические языки

Пока просматривал некоторые комментарии на мое сообщение про параллелизм и согласованность, я заметил что великая ошибка на тему динамических и статических языков продолжает держать людей в своем плену. Так что, в том же стиле «все что вы знаете это неправда», позвольте мне попробовать выправить это: динамический язык это статический язык в смирительной рубашке, который предоставляет меньше а не больше выразительности. Если вы один из счастливчиков кто уже это понимает, поздравляю, вы возможно сможете поступить в УКМ! Для тех кто этого не понимает или думает что я ошибаюсь, давайте попробуем разобраться. Я не буду использовать большое число технических подробностей в этом сообщении; все эти подробности имеются в моей книге которая скоро выходит, Практичные Основы Языков Программирования (ПОЯП), черновик книги доступен в интернете на

Так называемые динамические языки ( «так называемые» поскольку я покажу что они не существуют как отдельный класс языков) популярны уже давным-давно. Как я могу судить, это вопрос маркетинга по большему счету (прим.перев. списочный ассемблер с именем Лисп раньше использовал еще духИ с афродизиаком с пометкой «его используют для искусственного интеллекта» но они вышли из моды. еще, как мне кажется, динамических языков так много сейчас по той простой причине что они проще в реализации. в самом деле, всего один тип же, согласовывать типы не нужно. такое каждый студент написать может. и пишет). Эй, мы все хотим быть динамичными, не правда ли? Динамичная личность это та которая заставляет вещи происходить, рискует, получает удовольствие, нарушает границы обыденного! А кому охота быть статичным? Это синонимично скучному, в конце концов, а никто не хочет быть скучным (даже если он такой, или даже — особенно если он такой). Так что, эй, динамические языки это круто, правда (прим.перев. а какой же студент не хочет быть крутым)? Или, как ни посмотри, а крутым людям нравятся динамические языки (прим.перев. поскольку аудитория которая это слушает всего лишь студенты а не логики, они делают безосновательный вывод — люби динамические языки и будешь крутым, активным. будешь писать много кода получая от этого удовольствие плюс много денег). Статические языки — для сопляков и неудачников (прим.перев. которые тихо сидят в углу и уныло разбирают бардак после творцов за гроши).

Это один из аргументов, и, если говорить честно, вполне успешный пример маркетинга. Как большинство приемов маркетинга, он создан чтоб запутывать а не просвещать, и чтоб создавать впечатление а не информировать.

Другой частью привлекательности динамических языков похоже является то что они приобрели ауру нарушителя. Динамические языки сражаются против тирании статических языков, сражайтесь вместе с нами! Мы героические партизаны, защищающие свободу от тирании типизации! Мы крутые программисты, нам не нужна никакая вонючая система типов!

Сейчас я так-же подвержен соблазнам партизанщины как и парень рядом (свидетель того как я сейчас пишу), так что я способен оценить желание ударить вместе с ними, опрокинуть империю зла. Но у меня для вас новости: когда дело касается «динамической типизации», это безнадежное дело. Не потому что империя настолько могуча. Не потому что зло всегда побеждает.
Просто лишь потому что разница не имеет никакого значения. Динамическая типизация это всего лишь специальный случай статической типизации, такой что ограничивает а не освобождает, такой который перекрывает возможности а не открывает новые перспективы. Должен ли я был говорить это? Некую вещь врядли можно противопоставить той, частным случаем которой она является. Так что не занимайтесь холиварами, займитесь лучше программированием! Есть плохо определенные языки и есть хорошо определенные языки.
Хорошо определенные языки все статически типизированы, и языки с развитыми статическими системами типов включают динамические языки как частный случай, узкая система типов, но этот случай привлекает значительное внимание.

Витгенштейн сказал что все философские проблемы это проблемы грамматики.
Здесь мы наблюдаем то-же самое. Корень проблемы лежит в путанице между типом и видом (прим.перев. я счел необходимым перевести class именно так чтоб у читателя не возникало мыслей об ООП, оно тут не причем). Мы все понимаем что часто бывает очень полезным иметь несколько видов значений одного типа. Характерный пример предоставляется нам комплексными числами. Имеется один тип комплексных чисел, которые соответствуют точкам на двумерной плоскости. В школе мы встречали два вида комплексных чисел, в прямоугольной и полярной системах координат.
То есть, имеется два способа представить комплексное число, используя две разные системы координат. Они, само собой, взаимозаменимы, поскольку представляют значения одного типа. Но форма представления отличается, и некоторые формы более удобны чем другие (прямоугольная для сложения, полярная для умножения, например). Мы можем, конечно, выбрать «структуру реальности», и представлять все комплексные числа одним способом, и считать координаты всего лишь способом представления числа. Но так же может быть и удобно считать что тип комплексных чисел состоит из двух видов, каждый из которых образован двумя вещественными числами, которые однако интерпретируются по-разному в зависимости от используемой системы координат.

Принципиально тут то что различие между двумя видами комплексных чисел динамическое в том смысле что некое вычисление может вернуть число любого вида, в зависимости от удобства или соглашения. Программа может проверять, находится ли комплексное число в полярной или прямоугольной форме, и мы можем формировать структуры данных, такие как множества комплексных чисел, в которых отдельные элементы могут быть любого из видов. Но это не противоречит тому основному факту, что есть только один статический тип комплексных чисел! С точки зрения теории типов я говорю что тип комплексное определен как объединение (прим.перев. множеств, sum) двух картезианских произведений вещественного типа с самим собой. Одно из произведений представляет вид прямоугольных представлений, другое представляет вид полярных представлений. Будучи типом-объединением, мы можем «диспетчеризовать» (проводить анализ случаев) по виду значения типа комплексное, и решать что делать во время выполнения. В этом ничего особенного нет. Фактически, это вполне просто и естественно в языках таких как МЛ или Хаскелл, которые поддерживают типы-объединения. (Языки которые объединения не поддерживают, связаны по рукам и ногам, и отсюда происходит часть путаницы.)

Какое все это имеет отношение к концепции динамического языка? Характеристики динамического языка те-же самые, значения делятся по видам на множество форм, которые можно отличать друг от друга во время выполнения. Наборы значений могут содержать значения нескольких видов, и мы можем отделять во время выполнения что есть что и как обрабатывать каждый вид значения. Поскольку каждое значение в динамическом языке делится по видам в этой манере, что мы делаем так это склеиваем все значения языка в один, гигантский (возможно даже расширяемый) тип. Заимствуя удачное описание у Даны Скотт, так называемые нетипизированные («динамически типизированные») языки являются, фактически, единотипными (языками с одним типом). Вместо того чтоб иметь множество типов из которых можно выбрать, имеется только один!

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

Конечно я полностью в курсе что «компилятор может это оптимизировать», по крайней мере в некоторых случаях, но что-бы добиться этого нам потребуется одна из двух вещей (без учета недостижимых степеней наивности которые могут легче и выгоднее быть выраженными программистом непосредственно)(прим.перев. смысл выражения в скобках оказался слишком глубок для моего понимания). Либо вы отказываетесь от модульной разработки, и начинаете полагаться на средства анализа всей программы как целого (включая все библиотеки, сторонний код, наработки), или вы вводите статическую систему типов конкретно для цели отслеживания межмодульных зависимостей (прим.перев. смотрите статью по модульности). «Цельнопрограммный» подход не масштабируется, и вообще не сочетается с самым главным преимуществом которое динамические языки предположительно имеют, а именно — динамическая эволюция и разработка компонент (прим.перев. тут я почему-то вспомнил EVE Online и вечную нехватку стабильности и производительности Питона с которыми эта безусловно весьма прибыльная коммерческая разработка уже столько лет мужественно «борется»). Второй вариант, со вводом статической системы типов, работает отлично, и прекрасно подтверждает мою точку зрения (прим.перев. автор видимо снова про typed racket).

Я так-же полностью в курсе, что многие статически типизированные языки, в частности те которые широко используются коммерчески, не имеют достаточно выразительной системы типов, что-бы сделать осуществимой работу динамически (с несколькими видами значений) внутри статически типизированного фреймворка. Это аргумент лишь против плохих языков, а не аргумент против систем типов.
Цель системы типов (статической конечно, других видов не бывает) это именно предоставить выразительную мощность чтобы охватить все вычислительные феномены, включая динамическую диспетчеризацию и динамически расширяемую классификацию на виды, в пределах выразительного фреймворка статической дисциплины типов (прим.перев. предназначенного для ловли неизбежных случайных ошибок). Более «академические» языки, такие как МЛ или Хаскелл, не имеют никаких проблем с поддержкой динамических режимов программирования.

Почему вас это должно беспокоить? Потому, показываю я, что полностью выразительный язык это тот который поддерживает хрупкий баланс между статическими и динамическими техниками. Языки которые навязывают вам только один подход, а именно динамические языки, связывают вас; языки которые допускают оба режима рассуждения освобождают вас от тирании одного типа.
Пусть расцветут тысячи цветов (прим.перев. автор имеет ввиду очевидно доступное под рукой разнообразие типов. еще подобную фразу используют китайцы по поводу своего строя)!

Собака которая не лает

Ключевой факт, который позволил Холмсу раскрыть загадку Серебряного была собака, которая не лаяла: очевидно убийца и конокрад был не посторонний, а сам тренер, единственный кто мог войти в конюшни незамеченным. Как я упоминал, в этом семестре Дэн Ликата и я совместно преподаем новый курс функционального программирования для первокурсников в УКМ. За исключением параллелизма, который я уже обсуждал, мы уделяем большое внимание верификации и доказательствам как инструментам практикующего программиста, главные среди которых это нечестивые адские гончие компьютерных наук, индукция и рекурсия. И я счастлив сказать что, как в истории про Холмса, это собаки которые не лают. Результаты домашних работ и классных занятий ясно показывают что преобладающее большинство класса состоящего примерно из 80 студентов овладевают этими ключевыми техниками без лишней суеты и беспокойства. В этом сообщении я буду рад объяснить почему я полагаю что мы добились успеха там где, очевидно, так много других не добились ничего.

Одно из удовольствий преподавания в УКМ это то что студенты одаренные (одни из наиболее одаренных в стране, согласно обычным метрикам), непредубежденные (они играются со всем что я бы им не подкинул), и работоспособные (девиз УКМ «Мое сердце в работе.»).
Я уверен что большая часть нашего успеха из-за этого. Скорее всего наши студенты могут освоить почти что угодно, независимо от того насколько плохо мы будем объяснять!
Однако успех не может быть лишь по одной этой причине. Мои коллеги в других высших школах, и в исследовательских университетах и в колледжах, публичных и частных, американских и интернациональных, часто говорили о своем расстройстве и отчаянии в преподавании программирования с использованием рекурсии, не говоря уже о индуктивном доказательстве, для первокурсников или даже студентов старших курсов. Некоторые заходят даже так далеко что говорят что это невозможно, что хотя самые умные студенты «схватывают», у менее одаренных никак это не получается, так что нам вообще следует перестать пытаться это преподавать. Они меня не убедили. У меня нет твердых доказательств что я прав, но у меня есть вполне приличное количество лет опыта вытягивания всего этого на себе, так что по крайней мере можно представить что проблема лежит не в студентах, а в методах преподавания. Так что позвольте мне предложить свои для примера, возможно другие смогут их тоже применить.

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

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

Что делает структурную операционную семантику такой полезной так это то что модель исполнения напрямую задается индуктивным определением отношения трансформации, M->M’, над программами. (Тут нет места чтоб объяснить это полностью, но вы можете обратиться в ПОЯП за полным разъяснением.) Главная идея это использовать правила вывода для получения стурктурного описания процесса оценки для самой программы, а не путем трансляции ее в некий абстрактный машинный код реализации. Например, одно из правил для оценки выражений со сложениями, это

(M->M’) => ( (M+N) -> (M’+N) ),

которое гласит что один шаг оценки сложения M+N состоит из шага оценки M для получения M’, и что оценка суммы будет M’+N. Другое правило говорит что

(N->N’) => ( (m+N) -> (m+N’) ),

где m это число, а третье говорит что

(m+n) -> p,

где p это сумма m и n. С такими (и подобными) правилами в наличии, любой может получить путь выполнения в форме

M_1 -> M_2 -> … -> M_k,

который покажет явно шаги оценки. Каждый шаг обосновывается «деревом вывода» состоящим из композиции правил. Важно что размер выражений M_i соотносится напрямую с объемом памяти, требуемым реализацией, позволяя чистое и ясное объяснение особенностей расхода памяти таких как концевая рекурсия.

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

Отправная точка это, в очередной раз, индуктивное определение. Для конкретности и легкости демонстрации, позвольте мне привести индуктивное определение натуральных чисел:

=> Zero nat

m nat => Succ(m) nat

Определение использует точно тот-же формат правил, который мы использовали для определения семантик. Индуктивные определения задаваемые набором правил становятся второй натурой. Более того, они переписываются почти дословно на МЛ:

datatype nat = Zero | Succ of nat

Так что здесь у нас есть исконный пример индуктивно определенного типа.
Многие структуры данных, такие как различные формы деревьев, укладываются естественно в тот-же формат, факт который мы постоянно используем в течение семестра.

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

fun plus x y = case x of
Zero => y
| Succ x’ => Succ (plus x’ y)

Где бы у нас ни попадался индуктивный тип, мы используем тот-же формат каждый раз для функций определенных над ним. Главное, мы разрешаем себе «рекурсивные вызовы» точно соответствующие предпосылкам правила управляющего конкретным случаем. Нет нужды ни суетиться насчет «заталкивания» вещей, ни обсуждать «размеры» вещей, просто шаблон программирования который управляется непосредственно определением типа над которым мы работаем.

А теперь самое вкусное. Если мы хотим доказать что-нибудь о рекурсивно определенной функции, мы пишем доказательство, которое имеет в точности ту-же форму, по одному частному случаю на каждое правило в индуктивном определении. И, как только мы доходим до «рекурсивного вызова» для каждой предпосылки каждого правила, мы так-же делаем «рекурсивный вызов» к доказательству для каждой предпосылки, то есть ссылаемся на индуктивную гипотезу. Доказательство это, конечно, программа которая конструирует доказательство для каждого элемента индуктивного типа, формируя индуктивные шаги вокруг базового случая.

Важно что студенты «схватывают». На контрольной мы задаем им доказать (в течение занятия) небольшую теорему о куске кода, либо написать кусок кода и доказать небольшую теорему по нему, и они могут сделать это вполне уверенно. Другими словами, наш подход работает!

Думаю наиболее важно тут передать ощущение неизбежности и естественности индукции и рекурсии. Не преподавайте доказательства как отдельную тему! Не описывайте реализацию рекурсии более чем требуется языковой моделью. Просто делайте естественные вещи, и все будет вполне очевидно… и интересным!

Кроме того, это масштабируется. Наша верхняя граница перед контрольной это разработать и отладить сопоставитель регулярных выражений основанный на продолжениях в котором есть хитрая ошибка. Мы тщательно формулируем спецификацию сопоставителя, и пытаемся провести индуктивное доказательство что-бы обнаружить ошибку. Доказательство однако не проходит! И неуспех обнаруживает что есть ошибка, которую можно исправить несколькими способами, выправляя доказательство вместе с программой. Я расскажу подробнее об этом в другой раз, нетерпеливый читатель может впрочем посмотреть в моей статье озаглавленной «Отладка управляемая доказательством» в Журнале Функционального Программирования, там есть более ранний вариант того что мы преподаем в этом семестре.

Позвольте мне закончить тут двумя комментариями.

Маттиас Феллейсен в Северовосточном университете защищает в сущности эту-же методологию уже десятилетия; его работа сильно повлияла на мою. Его результаты вполне выдающиеся, и с гораздо большим количеством студентов чем я обычно сталкиваюсь здесь в УКМ. Так что всем без исключений: читать его «Как проектировать программы» и следовать ей!

Наконец, эта статья объясняет почему Хаскелл не подходит для моих целей: принцип индукции всегда неверен для программы на Хаскелле!
Проблема в том что Хаскелл это ленивый язык, а не язык с ленивостью. Он требует от вас существования «неопределенных» значений каждого типа, аннулируя краеугольный принцип доказательства по индукции. Если сказать другими словами как предложил Джон Лэнчбюри, типы Хаскелла нищие, нет даже стандартного типа натуральных чисел. Только представьте!

(И пожалуйста заметьте аналогию с динамическими языками, в противоположность языкам имеющим динамические типы. Тут та-же история, хотя и в другом виде, а именно нищета типов.)

Святая Троица

Христианская доктрина триединости гласит что существует единый Бог который проявляет себя в трех лицах, Отец, Сын и Святой Дух, которые вместе формируют Святую Троицу. Доктрина вычислительной триединости гласит что вычисление проявляет себя в трех формах: доказательства из пропозиций, программы из типов, и отображения между структурами. Эти три аспекта дают начало трем сектам поклонников: Логика, которая присваивает первенство доказательствам и пропозициям; Языки, которые считают первичными программы и типы; Категории, которые считают первичными отображения и структуры. Центральная догма вычислительной триединости гласит что Логика, Языки и Категории это только лишь три проявления одного божественного понятия вычисления. Не существует избранного пути к просветлению: каждый аспект предоставляет озарения вместе составляющие суть вычисления в наших жизнях.

Вычислительное триединство означает что любая концепция возникающая в одном из аспектов должна иметь смысл и с точки зрения остальных двух. Если вы придете к озарению которое имеет значение для логики, языков или категорий, можете быть уверены что вы прояснили важную концепцию в вычислении — вы сделали научное открытие которое будет важным еще долго.
Продвижения в нашем понимании вычисления могут происходить от озарений полученных разными путями (любые данные полезны и актуальны), но их неотъемлемая истинность не зависит от их популярности.

Логика говорит нам о том какие пропозиции существуют (какие виды размышлений мы хотим выражать) и о том что составляет доказательство (как мы передаем наши размышления другим). Языки (в смысле программирования) говорят нам какие типы существуют (какие вычислительные феномены мы желаем выражать) и о том что составляет программу (как мы можем добраться до этого феномена).

Категории говорят нам какие структуры существуют (какие математические модели у нас есть чтоб с ними работать) и что представляет из себя отображение между ними (как они связаны друг с другом). В этом смысле все три имеют онтологическую силу; они кодируют что «есть», а не «как» описать то что нам уже дано. В этом смысле они фундаментальны; если мы предположим что они только описательны, мы останемся наедине с вопросом о том где эти только что данные концепции возникают, возвращая нас назад к основам. Это основы которые я хочу описать здесь, поскольку я верю что это поможет разъяснить некоторые распространенные недопонимания насчет понятий пропозиции, типа и структуры. В частности интересно что «система типов» это, согласно данной концепции, не есть произвольная коллекция условий наложенных на данное перед этим понятие программы (что написанных с «=>», что нет). Это, напротив, способ сказать что есть программы прежде всего, и что они значат как доказательства и как отображения.

Здесь я обрисую основные соответствия между логикой, языками и категорями путем исследования их структурных свойств (и, пока что, ничего более).

Фундаментальное понятие в логике это следование, записываемое P_1, …, P_n >- P, выражающее выводимость P из P_1, …, P_n. Это означает что P выводимо согласно правилам логики если есть P_i как аксиомы. В отличие от допустимости ( которую я тут обсуждать не буду) эта форма следования не выражает импликацию! В частности, следование никогда не будет пустой истиной.

Следование имеет к счастью как минимум два критически важных структурных свойства, делающих его обязательным:

=> (P >- P)

(P >- Q) & (Q >- R) => (P >- R).

Дополнительно мы часто имеем еще следующие структурные свойства:

(P_1,…,P_n >- Q) => (P_1,…,P_n,P_n+1 >- Q)

(P_1,…,P_i,P_i+1,…,P_n >- Q) => (P_1,…,P_i+1,P_i,…,P_n >- Q)

(P_1,…,P_i,P_i,…,P_n >- Q) => (P_1,…,P_i,…,P_n >- Q).

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

В языках мы имеем фундаментальную концепцию суждения о типах, записываемую как x_1:A_1, …, x_n:A_n >- M:A, гласящую что M есть выражение типа A и включает переменные x_i типов A_i. Суждение о типах должно удовлетворять следующим базовым структурным свойствам:

=> (x:A >- x:A)

(y:B >- N:C) & (x:A >- M:B) => (x:A >- [M/y]N:C)

Мы можем думать о переменных как именах «библиотек», тогда первое гласит что мы можем использовать любую библиотеку которую захотим, а второе формулирует замыкание в результате «линковки» (как в Юниксовой программе ld или подобной), где [M/x]N есть результат линковки x из N к библиотеке M. Обычно мы ожидаем что аналоги аксиом «лишняя», «переупорядочивание» и «дублирование» тоже будут иметь место, однако это не обязательно так. Я оставлю их формулирование в качестве упражнения для читателя.

В категориях мы имеем фундаментальную концепцию отображения f: X —> Y между структурами X и Y. Наиболее элементарные структуры, возможно, есть множества, и отображения это функции, но будет более общим считать, скажем, что X и Y это топологические пространства, и f это непрерываная функция между ними. Отображения удовлетворяют аналогичным структурным свойствам:

=> (id_X:X —> X)

(f:X —> Y) & (g:Y —> Z) => (g o f : X —> Z)

Они выражают, соответственно, существование тождественного отображения и замыкание отображений путем композиции. Они соответствуют рефлексивности и транзитивности следования а так-же библиотечному и линкующему правилу языков. Как и в случае типов, можно ожидать дополнительные условия замыкания, соответствующие аксиомам «лишняя», «переупорядочение», «дублирование» путем назначения подходящего значения множественным предположениям. Я тут не буду этим заниматься, однако множество стандартных источников рассматривают эти условия подробно.

Что я нахожу интересным насчет вычислительного триединства так это то что оно красиво! Вообразите мир в котором логика, программирование и математика унифицированы, в котором каждое доказательство соответствует программе, каждая программа — отображению, каждое отображение — доказательству! Вообразите мир в котором код это математика, в котором нет разделения между рассуждением и выполнением, нет разницы между языком математики и языком вычисления. Триединство это центральный организующий принцип теории вычисления, который объединяет, унифицирует и обогащает язык логики, программирования и математики. Он предоставляет фреймворк для обнаружения и анализа вычислительных феноменов. Новшество в одном аспекте должно иметь последствия для других; хорошая идея это всегда хорошая идея, в какой бы форме она не возникла. Если идея не имеет полезного смысла логически, категориально и с точки зрения типов, то она не может быть проявлением божественного.

Функции это значения

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

Каков тип и значение выражения «fn x => raise Fail»?

Я почуял неприятности когда, в течение контрольной, один из студентов попросил меня уточнить для него что имеется ввиду в этом вопросе. Нет нужды объяснять что я просто потерял дар речи!
Очень сильно похоже что все студенты кроме одного понимали этот простой вопрос неправильно, иногда удивительно странным образом.

Многие говорили «у него нет значения» и делали попытку угадать какой у него может быть тип. Другие говорили «оно бросает исключение» и поэтому должно иметь тип «exn». (Для тех, кто не знает МЛ, тип exn это тип значений связываемых с исключениями.) Потом другие еще говорили «компилятор определит что оно всегда бросает исключение, и следовательно отбросит это выражение как недопустимое», ну или слова похожие на эти по смыслу. Черт возьми, где они нахватались таких причудливых представлений? Каковы бы не были недостатки нашего преподавания, мы определенно ничего близкого к этому не говорили никогда! Другие же определяли тип выражения правильно, но все никак не могли объяснить каково будет его значение.

С учетом того, что они вполне способны писать программы с функциями высокого порядка, как могло такое произойти? Очевидно неудача не в наших студентах, а в нас самих. Но что мы сделали не так? Как мы завели в тупик так много студентов с тем что по нашему мнению было свободным трехочковым вопросом (прим.перев. снова сленг не вполне понятен мне)? Честно говоря, я не знаю. Но у меня есть несколько теорий, которые я думаю тут высказать в надежде помочь другим избежать моих ошибок, или устранить непонимания в зародыше.

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

Вот где мы свернули не туда, и я думаю породили дикие предположения которые и привели к ошибкам на контрольной. Одно и крутых применений функций высокого порядка это организация деления вычисления на эпапы. Хорошим примером является сопоставитель регулярных выражений основанный на продолжениях, который я тут однако не буду объяснять во всех подробностях. Ключевой момент тут в том что он имеет тип

regexp -> string -> (string -> bool) -> bool

который говорит о том что он принимает регулярное выражение, строку, и продолжение, сопоставляет начальный сегмент строки, если возможно, и передает остаток в продолжение, или возвращает ложь если не удалось сопоставить. Как это описание предлагает, мы можем думать о сопоставителе как о кэррированной форме трехаргументной функции, и он такой и есть. Но более интересная формулировка делит вычисление на этапы таким образом что, получив регулярное выражение, оно вычисляет сопоставитель для этого регулярного выражения, который может быть применен повторно к большому числу разных строк без повторной обработки регулярного выражения. (Код для такой задачи вполне красив; он доступен на веб-сайте нашего курса если вас это заинтересовало.)

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

Так что, моя первая часть совета будет не упоминать компилятор для объяснения чего либо! У них будет еще куча шансов позже в их карьерах изучать компиляторы, и понять как семантики информируют компиляцию, что такое правильные тождественные рассуждения и так далее. Но для первокурсников, ограничьтесь моделью. Иначе вы напроситесь на неприятности.
(Я уже упоминал другие ситуации где упоминание «компилятора» только мутит воду и запутывает студентов, основным примером среди которых было преподавание рекурсии. Я собираюсь обсудить другие в будущих заметках.)

Теперь когда я принял на себя вину за свои ошибки, я буду чувствовать себя менее виноватым переадресуя ее часть куда-нибудь еще. У меня есть два предположения насчет того почему студенты сопротивляются идее того что функции есть значения фундаментально не отличающиеся от всех остальных. Один источник этого, без сомнения, это то что многие из них «выучили» программирование на улице и выработали все виды ошибочных представлений которые и были применены здесь. Большинство популярных языков делают трудной работу с функциями как значениями: вам приходится их именовать, у вас появляются особые затруднения при передаче их как аргументов или возврате как результатов, они называются «методы» и имеют странную семантику с использованием состояний, и так далее и тому подобное. От всего этого студенты приобретают чувство что функции «особенные», и о них нельзя думать так-же как об остальных вещах.

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

Постоянство Памяти

Шедевр Сальвадора Дали, Постоянство Памяти, одно из наиболее признанных творений искусства в мире. Критик Даун Эйдес описал его как «Сюрреалистическая медитация над крахом наших представлений о жестком космическом порядке» порожденная пронизывающим анализом Эйнштейна концепций времени и пространства в физическом мире. Совсем как Постоянство Памяти Дали обозначает переход от вековых концепций времени и пространства в физике, так же и вычислительная концепция постоянства (прим.перев. далее слово persistence я буду переводить как хранимость, так будет яснее о чем речь) памяти отмечает переход от последовательного времени и изменяемого состояния к параллельному времени и неизменяемому состоянию.

Совсем недавно я описал различие между параллелизмом и согласованностью (concurrency) в терминах стоимостной модели которая сопоставляет параллельную, так же как и последовательную, временнУю сложность программе. Параллелизм это лишь вопрос эффективности, не семантики; смысл программы не зависит от того, выполняется ли она на одном процессоре или многих (прим.перев. если зависит то просто программа не дописана). Функциональные языки выделяют параллелизм органичивая последовательные зависимости между частями вычисления; императивные языки вносят лишние зависимости которые препятствуют распараллеливанию.

Другой критический компонент для распараллеливания это концепция хранимой структуры данных, такой для которой связанные с ней операции трансформируют (прим.перев. структуру в другую), а не меняют ее. Хранимый словарь, например, имеет то свойство что вставка элемента приводит к возникновению нового словаря с расширенной областью; старый словарь сохраняется, и по-прежнему доступен для дальнейших трансформаций. Когда вычисляем сумму 2 и 2, получая в результате 4, никто ведь не представляет что двойки «расходуются» в процессе!
Так-же никто не беспокоится, является ли сумма 1 и 3 «той-же» 4 или «другой» 4! Сам этот вопрос нелеп (или, говоря более точно, тривиален) (прим.перев. результат 2+2 несет для нас тот же смысл что и результат 1+3, они имеют одно поведение, значение, равнозначны. это разные представления одной абстракции).
Тогда почему мы беспокоимся о том, «расходует» ли результат вставки 2 в словарь старый словарь? И зачем мы беспокоимся о том, получаем ли мы после двойной вставки 2 в пустой словарь «тот-же» словарь или «другой»?

И при всем при этом и академические и практические компьютерные разработки практически все ограничивают себя эфемерными (прим.перев. так называют, как вы поняли, обычные императивные данные в памяти, перезаписываемые и существующие очень недолго) структурами данных, которые показывают именно такое поведение.
Операции над эфемерной структурой данных «расходуют» ее, делая ее недоступной для дальнейшего использования, если не пройти через некоторые неприятности чтоб получить ее назад. Патологии, происходящие из-за этого, обширны. Стандартные тексты по компиляторам, например, посвящают главу концепциям наподобие «блочно-структурированные таблицы символов», которые, фактически, есть ничего более чем хранимые словари, сделанные сложным способом (прим.перев. так и хотелось написать — через ж.). Говоря более общо, как только структура данных имеет несколько «будущих» (futures), например как при бэктрекинге или распараллеливании, эфемерные структуры данных мешаются под ногами. На самом деле, неподъемная груда ООП, с его абсурдным переакцентом на метафору «посыла сообщений», концентрируется на изменении объектов как на центральном организующем принципе, ставя в тупик параллелизм и усложняя простые алгоритмы (прим.перев. привет и тебе, надежно тормозящий Erlang… как изменение состояния в силу своей однонаправленной разрушительности не является безопасной абстракцией так и посыл сообщения есть, наподобие goto, указателей, нитей, наследования, и т.д. излишне мелкой и небезопасной, в силу однонаправленности, абстракцией. такие абстракции могут комбинироваться неправильно и от этого все ошибки. о б этом будет еще один комментарий потом).

Основным достоинством функциональных языков является то что хранимость используется по умолчанию, и при том они с той-же легкостью могут поддерживать эфемерные структуры данных как и любые другие императивные (включая объектно-ориентированные) языки. Все функциональные языки включают типы изменяемых ячеек и изменяемых массивов, и предоставляют поддержку для стандартного, последовательного, императивного программирования с точками с запятой и даже фигурными скобками (прим.перев. сколько не говорили что фигурные скобки нужны во всех новых языках для совместимости со старыми, по-моему это было всего лишь перевешиванием фигурки с зеркала старой машины на зеркало новой)! (Некоторые делают это лучше прочих; Хаскелл это, с моей точки зрения, лучший в мире императивный язык программирования, и второй по качеству функциональный язык, но это предмет для отдельного обсуждения.) Но зачем вам бы этого хотеть? Зачем лишать себя преимуществ хранимости и настаивать вместо этого на эфемерности структур данных?

Этот вопрос всплыл недавно при нашем планировании класса функционального программирования который мы читали в этом семестре для первокурсников в УКМ. Весь семестр мы использовали техники функционального программирования что-бы писать ясные, проверяемые, модульные, параллельные программы. Студенты планово доказывали теоремы о своем коде, структурировали программы используя абстрактные типы, и извлекали параллелизм чтоб улучшить асимптотическую производительность своих программ. Последние домашние задания включали реализацию параллельного алгоритма Барнеса-Хатта для проблемы N тел в физике, и параллельный алгоритм Джамбори для поиска по игровому дереву в играх с полной информацией. Хранимые структуры данных являются ключом к тому чтоб это было возможно; просто попробуйте закодировать Барнеса-Хатта на императивном языке, и вы быстро обнаружите себя в болоте забот о согласованности в то время как вы должны вместо этого заниматься планированием рекурсивного дерева разбиения пространства, и вычислением сил используя формулы из школьного курса физики.

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

Большинство аргументов насчет эффективности, однако, игнорируют вопросы функционала. Бессмысленно сравнивать «эффективность» некой структуры данных которая предоставляет отличающуюся от другой структуры функциональность. Хранимая структура данных делает для вас больше чем эфемерная (прим.перев. не могу не обратить внимание на то что этот «лишний» функционал таки является необходимым. так-же необходимы while вместо goto, сборка мусора для указателей и многое другое. осторожнее! слишком многие мечты об эфемерной эффективности отрезАли нужные органы от программы).
Она позволяет вам иметь множественные «будущие», включая те что развиваются параллельно друг с другом. Не имеет смысла настаивать что некие эфемерные аппроксимации такой структуры данных «более эффективны» если они не предоставляют таких возможностей! И попытка заставить аппроксимации их выполнять, несомненно, проблема (прим.перев. в оригинале тут более крепкое выражение)! Стандартные эфемерные структуры данных не являются легко параллелизуемыми; зачастую попытку получить приличную степень параллелизма с использованием императивных методов стоит опубликовать (прим.перев. имеется ввиду что она достаточно сложна чтоб представлять научный интерес). Для сравнения, даже первокурсник (в смысле, первокурсник УКМ) может реализовать параллельный поиск по дереву игры или основанное на древоподобном разбиении пространства решение проблемы N тел в течение домашнего задания, на которое отводится неделя.

Тогда в чем проблема? Зачем нам беспокоиться об эфемерных структурах данных вообще? Лично я без понятия. По большему счету, это просто налог на жадность (прим.перев. мне показалось более точным это выражение), налагаемый на нас чрезмерно фанатичным упором на императивные методы и машинные модели вычислений, вместо языковых моделей вычислений. Но это изменится.
Начиная с этой осени, введение в структуры данных и алгоритмы будет освобождено от ограничений императивного, объектно-ориентированного программирования, и вместо этого будет подчеркивать хранимые (так-же как эфемерные) структуры данных, и параллельные (включая как специальный случай последовательные) алгоритмы. Будущее вычислительных технологий зависит от параллелизма (для эффективности), распределенных вычислений (для масштабирования) и верификации (для качества). Только новые функциональные языки поддерживают все эти три вещи естественно и удобно; старые языки просто это не осилят (прим.перев. я сознательно отнес неразвитые функциональные языки типа Лиспа к неосиливающим, у них проблемы и с параллелизмом и с верификацией).

Обновление: вот диаграммка подводящая итог ситуации как я ее вижу:

Последовательноеимперативноеблагоприятные эффекты
Параллельноетрудно сделать правильнофункциональное

Стандартное императивное программирование работает неплохо для случая эфемерный-последовательный; представляет известную трудность использовать императивные методы для параллелизма. БлагоприятныеЭффекты, как показывается самоподстраивающимися структурами данных, могут быть использованы для приближения к хранимому поведению в последовательной обстановке, но использование эффектов препятствует параллелизму.

Дохлый пес

В бывшем ранее сообщении я писал о нашем подходе обучения студентов рассуждать индуктивно при программировании рекурсивно. Оно породило некоторое обсуждение, поскольку преподавание индукции и рекурсии представляет известную трудность, вплоть до того что многие из моих коллег практически потеряли надежду даже донести эти идеи до большинства своих студентов.
Я уже объяснял наши методы, и предлагал некие причины почему нам похоже это удалось в то время как остальным нет.

Мы подходим к концу семестра, и я должен сказать что я так горжусь нашими студентами что не могу не похвастаться немножко. Прежде всего, небольшое введение. Как я упоминал, я со-преподаю новый курс функционального программирования с Дэном Ликатой в этом семестре, как часть тщательной переделки вводного курса компьютерных наук, который делает сильный акцент на рассуждениях о корректности и эффективности программ как в последовательной так и в параллельной обстановке. Дэн и я работали тесно с впечатляющей командой помощников (Dan Licata, Michael Erdmann, Ian Voysey, Michael Arntzenius, Luke Zarko, Abigail Motley, Amy X. Zhang, Brandon Bohrer, Dan Yang, Eric Balkanski, Esha Uboweja, Laura Scharff, Matt McKay, Nick Kindberg, Rafee Memon, Robert Murcek, Sri Raghavan, Tyler Hedrick, Todd Nowacki) при разработке новой программы обучения и учебных материалов для нее. С целью непрерывности, Дэн читал все лекции, а я сидел в аудитории, иногда произнося провоцирующие комментарии, но в основном просто уделяя внимание сигналам которые подают студенты и думая о том что мы можем сделать лучше в следующий раз. Несмотря на то что это был сравнительно большой класс из примерно 83 студентов, мы старались поддерживать интерактивную атмосферу в которой студенты свободно спрашивают, и отвечать на вопросы, иногда работая парами в течение нескольких минут независимо в течение лекции. Это работало очень хорошо для всех, создавая творческую атмосферу для обучения тому как писать красивый код.

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

Но достаточно уже введения в контекст сообщения. То что заставляет меня чувствовать такую гордость сегодня — это профессионализм, продемонстрированный нашими студентами при сегодняшней разработке программ в режиме диалога. Упражнением было реализовать удаление в двоичном дереве поиска в хранимом (трансформационном) стиле, а так-же в эфемерном (императивном) стиле, двумя разными способами. Дэн сформулировал задачу, и попросил студентов помочь ему написать код. Что впечатлило меня так глубоко так это то что когда я прислушивался к болтовне в учебной комнате и к предложениям, высказываемым громко, я мог слышать студентов говорящих вещи типа:

…Чтож, индуктивно, мы можем полагать что проблема была решена для левого поддерева, так что для того чтоб идти далее нам нужно только…

Блестяще! (И не забываем, это лишь первокурсники!) Как раз как я и надеялся, для этих студентов индуктивные размышления приходят сами собой, как очевидный путь размышлять над куском рекурсивного кода! Они знают инстинктивно как формулировать индуктивную аргументацию корректности программы, вместо того чтоб прибегать к подверженному ошибкам вождению руками по воздуху на тему «идем сюда и потом сюда по циклу», которое слишком часто встречается на данном уровне обучения. Что сделало это возможным так это то что функциональные программы в сущности математические, позволяя студентам концентрироваться на идеях, а не на сложностях кодирования на менее выразительных императивных языках. Я думаю это дает им уверенность в себе для того чтоб браться за некоторые достаточно трудные проблемы, наподобие алгоритма Барнеса-Хатта для задачи N тел или алгоритма Джамбори параллельного поиска по дереву игры, в рамках домашнего задания на одну неделю. Материал, который считается сложным или откладывается до более продвинутых курсов, может легко выполняться новичками, если у вас есть правильный каркас в рамках которого можно выражать идеи (прим.перев. это основная мысль не только данного сообщения но и всего блога, пожалуй. главное — правильный подход. чтоб его найти надо знать какие подходы НЕ правильны и почему. именно поэтому прежде всего надо выискивать во всем недостатки).

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

Модули важнее всего

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

(G >- M:A) & (G,x:A >- N:B) => (G >- [M/x]N:B)

Словами пешехода (прим.перев. имеются ввиду императивщики), тип A это «заголовочный файл» описывающий M, а N это новый код, реализующий спецификацию B с использованием понятий еще не заданной реализации функциональности, описываемой A. Взаимодействие между M и N проходит полностью через тип A; доступ к исходному коду M не разрешен клиенту, именно для того чтоб зависимость между компонентами была ослаблена, в ожидании будущих изменений в M, либо чтоб добиться гибкости в разработке (M не обязан даже существовать для того чтоб шла разработка N, нужно только чтоб тип A был задан).

Для извлечения максимальной пользы, важно чтоб отношение между M и A было многие-ко-кногим, а не многие-к-одному или один-к-одному. Думайте об A как об API (прим.перев. описании прикладного интерфейса программы) для отображения между ключами и значениями. Абсолютно необходимо чтоб язык допускал многие разные модули M быть типа A, и так-же абсолютно необходимо чтоб данный модуль M удовлетворял многим различным типам A, без предварительного упорядочения. Тип A есть только описание экстенсионального поведения модуля данного типа, и не может трактоваться как фиксирующий любую частную реализацию данного поведения. Более того, данный модуль может так-же поддерживать множество проекций типа, например «забывая» определенные аспекты его в некоторых контекстах. Например, допустимо пренебречь тем что реализация отображения поддерживает удаление в условиях когда только расширение и аппликация требуются.

Все эти возможности вполне базовые, но что удивляет меня так это то как мало языков поддерживает их ясно и просто (прим.перев. меня тоже удивили в свое время черты поддержки модульности в МЛ, в поисках «идеальной модульности» я и набрел на этот блог одного из разработчиков МЛ). Один из особенно уродливых способов это полагаться на внеязыковые «средства» которые манипулируют параметрами сборки для переключения вариантов выбора M для данного N, быстро приводя к появлению отдельного самопального языка используемого просто для управления скриптами сборки (прим.перев. зоопарк make-систем, привет тебе. однако при всех этих словах автора в реализациях МЛ все-таки есть отдельные языки сборки CM и MLB… правда создается впечатление что они лишь оптимизация и следствие артефактов файловых систем. вопрос требует углубленного изучения). Другая техника заключается в манипулировании наследованием или ограничении наследования (прим.перев. все современные авторитеты практически единогласно дают основанный на практическом опыте совет ограничиваться наследованием от абстрактных родительских типов и причем одиночным наследованием. что как раз и приближает его к отношению между интерфейсом и реализацией в модульности. например Майкл Франц и его Компонентное программирование) так что некоторая доля модульности может быть промоделирована, но это почти то-же самое что забивать гвозди плоскогубцами. Общая методология, фактически, пытается ограничить наследование для того чтоб предоставить то что мы имели в МЛ в ранних 80-х (функторы), пытаясь обойти прошедшие с тех пор десятилетия неправильных реализаций сомнительных идей.

Больше всего расстраивает, по крайней мере меня, то что даже относительно продвинутые языки, такие как Хаскелл или Fsharp, не имеют поддержки этих основных механизмов модульности.

В Хаскелле у вас есть классы типов (type classes, тайпклассы), которые необъяснимо популярны (возможно потому что это первая вещь которую многие люди осваивают). Есть две фундаментальные проблемы с классами типов. Первая это то что они требуют чтоб тип мог реализовать класс типов строго одним способом. Например, согласно философии классов типов, целые числа могут быть упорядочены строго одним способом (стандартное упорядочение), однако очевидно есть и много других полезных упорядочений (например по степени делимости). Вторая это то что они сталкивают лбами два отдельных момента: спецификацию того как тип реализует класс типов и спецификацию того когда та первая спецификация реализации должна быть использована при выводе типов. Как следствие всего этого, использование классов типов, по словам Грега Моррисетта, напоминает управление Королевой Мэри (прим.перев. это большой корабль однотипный как мне помнится Титанику): вам требуется направить всю эту огромную массу корпуса в нужную сторону так чтоб потом механизм вывода вывел вещи в том виде который вам нужен (прим.перев. эта ситуация так-же плоха как и использование машинной модели вычислений). В Fsharp ситуация еще более непростительна, по моему мнению, ведь они начали с правильной системы (Caml) и выбросили как раз ту вещь которая наиболее значима в МЛ, его систему модулей (прим.перев. чему удивляться, они просто слышали что есть такой крутой язык Камл и сделали нечто похожее на него сами и ровно в той мере в какой смогли осилить)! Вместо этого они ввели кучку объектной чепухи (ради совместимости с .net и устройством мозга ее разработчиков), и попытались обмануть язык самопальными наворотами которые более легко и гибко, предоставляются системой модульности. Какая досада (прим.перев. голосом Фрекен Бок из мультфильма Карлсон)!

Почему вообще возник этот вопрос (прим.перев. о модульности)? Вопреки глухому (прим.перев. точно, все говорят но никто не слушает) общественному мнению, я утверждаю что у нас на самом деле небольшой выбор того какой язык программирования использовать при обучении наших студентов (прим.перев. лично я полагаю что и при обычном прикладном программировании можно прийти к тем-же выводам при сравнении языков. по крайней мере если есть цель упростить поддержку проекта в дальнейшем. японцы официально развивают SMLsharp именно с такой целью. а отполировать реализации, доклепать библиотек и напечатать учебных материалов можно, это дело поправимое. тем более что у МЛ в этом плане все вовсе не так уж плохо).
Модульность важнее всего, и у нас должен быть язык который поддерживает гибкую модульность в том виде который я описал тут. Когда мы рассмотрели доступные нам варианты, что мы сделали очень аккуратно, единственные претенденты остались Стандартный МЛ и Окамл. Мы могли использовать любой, но были убеждены что надо использовать Стандартный МЛ, который сработал прекрасно для наших целей. Определяющим фактором в выборе между двумя вариантами МЛ явилось просто то что у нас уже были прошлые наработки на Стандартном МЛ от которых можно оттолкнуться, и то что есть две реализации Стандартного МЛ которые поддерживают параллелизм (MLton и Poly/ML), хотя ни одна из них не оптимальна для наших целей (прим.перев. вижу три фактора — автор один из разработчиков МЛ, МЛ проще и меньше как язык чем ОКамл, у МЛ достаточно наработок по параллелизму. что касается параллелизма то это как CML, причем иногда даже с нитями на уровне ОС как у упомянутых тут Mlton и Poly, так и Facile и наработки Берри-Тернера. увы добавлю что по крайней мере у Poly еще год назад параллелизм был простенький, чисто под Isabelle. и вообще и там и в разработках на базе CML сборщик мусора и рантайм обычно непараллельные и соответственно достигаемое ускорение обычно упирается в цифру 4-6 на реальных задачах. впрочем так-же часто отмечают что куски написанные в чисто функциональном стиле имеют малое разделяемое состояние и потому масштабируются более многообещающе. в целом обстановка на уровне Хаскеля полагаю). Хаскелл предоставляет лучшую поддержку для параллелизма (откатывая свое неудачное стремление к ленивости, которая приводит к стоимостной модели для времени и, особенно, занимаемого объема памяти, такой что ей невозможно пользоваться), но он нам не подходит поскольку недостаточно поддерживает модульность.

Как я уже упоминал, наш план это переделать вводный курс программирования ради его модернизации и большего акцента на принципы а не на текущие технологии. Одна из сторон этой задачи это переделать стандартный курс структур данных и алгоритмов чтоб исключить чрезмерный акцент на эфемерные структуры данных, и начать рассматривать параллельные алгоритмы как общий случай который включает в себя становящийся все менее важным случай одного процессора. (Да, это направление развития технологий, но более важно что это концептуальное изменение которое возникает от сосредоточения на языке а не на машине) Что такое структура данных?
Это сигнатура, или интерфейс, записанный на языке на котором вы программируете. Что такое алгоритм? Это структура, или реализация, этой сигнатуры. Сигнатура, такая как для отображения, может быть реализована различными способами, с различными стоимостными компромиссами (логарифмическое время выборки либо константное время выборки, например).
Некий алгоритм, такой как сбалансированное дерево, может реализовать многие различные структуры данных, такие как отображения или множества. Различие между хранимым и эфемерным отображением это различие структур данных, то есть — сигнатур. Требования различны, алгоритмы различны. Мы должны быть способны поддерживать обе формы одинаково легко и чисто, должны быть способны сравнивать их, и объяснять, например, почему эфемерный случай имеет ограниченную применимость. Не так уж и много мы просим — иметь возможность записать эти примеры как выполняющийся код, с минимумом возни и беспокойства!

В течение десятилетий мы боролись с использованием объектно-ориентированных языков, таких как Java или C++, чтоб объяснить эти простые идеи, и все время терпели неудачу. И я могу сказать тем из вас кто не вовлечен в сферу академического образования в данный момент, многие из моих коллег по всему миру находятся в той-же ситуации, и отчаялись найти выход из нее. Уродливая методология, «шаблоны проектирования», «руководства по стилю», все они мешают преподавать принципы программирования. И даже если это отодвинуть в сторону, вы по-прежнему делаете императивное программирование на эфемерных структурах данных. Это просто не работает, поскольку это фундаментально неправильная вещь. Просто попробуйте преподать, скажем, удаление в двоичном дереве поиска; это ужасающая путаница! Вы закончите абсурдной ерундой «null указателей», и сложной путаницей вызванной методологией, а не самой задачей. Очень скоро вам придется прибегнуть к «каркасам» и «средствам» просто чтоб дать студентам шанс довести до конца что-нибудь вообще, отдаляя их от существа идей и создавая впечатление что программирование болезненно и уродливо, что является огромной трагедией.

Нашим решением было выбросить все это целиком, подвинув ОО техники в более старшие курсы для студентов которые захотят их изучать, и сосредоточиться на основных принципах модульности, параллельном и последовательном анализе стоимости, и прямой верификации работающего кода на первом курсе. Дейкстра говорил «красота это наш бизнес», к чему я могу добавить что жизнь слишком коротка а одаренные мозги слишком ценны чтоб тратить их зря на уродливые вещи. И если вы отнесетесь к данной точке зрения серьезно, лучших и самых сообразительных данный подход привлек а не оттолкнул (прим.перев. тут опять какой-то сленг но думаю смысл такой). Следуя словам моих коллег из Мажорного Института Технологий (прим.перев. мне кажется он тут дразнит Массачусетский Технологический, расшифровывая его аббревиатуру по своему. и я попытался передать прикол. Что я могу сказать на опыте перевода блога — мужик за словом в карман не лезет, профессор же. Иногда тяжело изложить по русски его сленг), студенты абсолютно влюбляются в программирование и влюбляются в красоту кода, при условии что код который вы просите их написать, красив на самом деле. Нет ничего более мрачного чем корпоративная бюрократия ООП, и мало вещей более привлекательны чем математическая элегантность ФП.

Некоторые мысли по преподаванию ФП

Несколько людей задавали очень неплохие вопросы о деталях того как мы преподаем определенные понятия в нашем новом курсе функционального программирования первокурсникам в УКМ. Вместо того чтоб разбрасывать ответы по разным сообщениям, я опишу несколько основных моментов здесь с надеждой помочь другим которые захотят преподавать подобный курс. Так что это сообщение на самом деле не для широкой аудитории, а для специалистов; вы свободны пропустить его если оно покажется слишком специфическим для ваших интересов. Я обещаю написать более любопытный для большинства материал вскоре!
Тем не менее, вот некоторые соображения, представленные в произвольном порядке независимо от их важности.

Поскольку курс предназначается для начинающих, мы начинаем с нуля с языковой моделью вычислений. Это значит что, с учетом одной прискорбной ошибки с нашей стороны, мы никогда не говорим о внеязыковых концепциях наподобие «стеков времени выполнения» или «компиляторов». Студенты обычаются думать в терминах самого языка, и рассуждать напрямую о корректности и эффективности кода который они действительно пищут, а не о коде в который он якобы копмилируется или транслируется. Одна из красивых возможностей подхода основанного на языке это то что мы начинаем с очень знакомой моделью вычислений, с оценки полиномов над вещественными числами. Они хорошо знакомы всем студентам, и я полагаю студенты находят эту область очень удовлетворяющей именно потому что полиномы имеют прямой вычислительный смысл. Вы подставляете переменные и сокращаете, и получается ответ. Далее мы можем основываться на этом как на нашей отправной точке; программы это просто обобщенные полиномы.
В частности, в функциональном языке переменные это переменные: математическое понятие переменных, которые получают значение путем подстановки, в точности есть программное понятие переменной. Оно не аналогичное, оно то-же самое. Так что мы можем отталкиваться от их опыта и просить их доказывать вещи о программах используя методы которые построены непосредственно на том что они уже знают. Это предельно естественно, и очень красиво, и легко приводит нас к объединенному взгляду на математику и программирование. Кроме того, это выравнивает игровое поле. Студенты с предыдущим «опытом программирования» находятся, если что, в неудобных условиях, поскольку они думают что знают вещи, которые либо ошибочны либо неприменимы. Еще одним следствием является равенство по половому признаку, поскольку даже с американским обществом таким какое оно есть, женщины не будут в неудобных условиях по сравнению с мужчинами когда дело доходит до нашего стиля мышления и программирования. Это в любом случае выигрышная ситуация.

Переходя к более техническому уровню, использование структурной операционной семантики является необходимым для предоставления строгого основания для понимания выполнения программы, рассуждения о корректности программы, и для определения стоимостной модели в поддержку рассуждений об асимптотической сложности. Это ничем нельзя заменить! Без кристалльно ясного формулирования семантики языка, невозможно обсуждать ни один из этих моментов осмысленно и технически точно. Имея ее вы можете легко разрешать любые вопросы типа «что будет если…», предоставляя студентам инструмент который они могут использовать сами что-бы отвечать на такие вопросы.
Кроме того, поскольку верификация программ становится более важна как в промышленной практике программирования, так и в академических исследованиях, необходимо чтоб студенты были образованы в инструментах семантики. Структурная операционная семантика очень проста в преподавании, и не представляет проблем для студентов. Мы просто используем ее, и они усваивают ее без всякой суеты и беспокойства. Она является естественным расширением их опыта школьной алгебры. Не бойтесь ипользовать эти инструменты для преподавания программирования!

Как я раньше объяснял, очень хорошая идея избегать Булевы величины так долго как только это возможно. И, прежде всего, не упоминайте о равенстве! Знак равенства в языках программирования это не тот же знак равенства что в математике. Пропозиции это не Булевы величины, и это только запутывает дело если использовать обозначения которые провоцируют неверное понимание. В связи с этим, так-же полностью избегайте if-then-else, и вместо него используйте только анализ случаев для ветвления, даже когда рассматриваемое значение Булевское. Мы последовательно пишем вещи наподобие

case,y) of
LESS => …
| GREATER => …
| EQUAL => …

вместо вложенного условного ветвления. Это способствует тому чтоб студенты думали в понятиях сопоставления образцов, и подготавливает почву для дальнейших разработок, включая мягкий переход к сопоставлению с образцами для более сложных структур данных и индуктивных рассуждений при рекурсивном программировании.

Преподавание параллелизма полностью прямолинейно, поскольку языковая модель вычисления сама по себе избегает неестественных и лишних проблем взаимовлияния, и сосредотачивает внимание на критическом моменте зависимостей по данным между вычислениями в программе. Студенты не испытывают проблем с вычислениями работы (последовательной временнОй сложности) или размаха (параллельной временнОй сложности) программы, и не испытывают проблем с чтением соотношений для соответствующих временнЫх сложностей. Позже, когда мы вводим последовательности, идея вычисления параллельно над всеми элементами последовательности, вместо поэлементного (как поощряется ужасными итераторами так любимыми в мире ОО), приходит естественно и легко. Ключом к этому, конечно, является то что структуры данных в функциональном языке естественно хранимы; чудовищно трудно использовать эфемерные структуры данных в параллельных вычислениях, и это не то что мы можем надеяться преподать первокурсникам.

Сложным выбором для нас было как преподать выражение и принуждение абстракции в программе. Отступая от нашего предыдущего подхода, мы решили не использовать пометку непрозрачности (герметизацию) как способ принудить абстракцию. У данного способа есть свои преимущества, но проблема в том что он не очень хорошо увязывается с другими возможностями языка, в частности с подструктурами и классами типов (видами)(прим.перев. возможно речь идет про виды для МЛ, предложенные Окасаки). Для примера, рассмотрим сигнатуру отображения которое определено над упорядоченным типом ключей:

signature MAPPING = sig
structure Key : ORDERED
type ‘a mapping
val lookup : Key.t -> ‘a mapping -> ‘a


К несчастью, герметизация структуры с такой сигнатурой делает модуль бесполезным:

structure IntMapping :> MAPPING = struct
structure Key = Int
type ‘a mapping = ‘a bst


Проблема в том что не только тип `a IntMapping.mapping получается абстрактным, как намеревалось, но так-же и IntMapping.Key.t, на что мы вовсе не рассчитывали! Что-бы обойти это мы должны будем создать специализацию сигнатуры MAPPING используя один из нескольких способов таких как

where type Key.t=int
structure IntMapping :> INT_MAPPING = …

Конечно никому не понадобиться называть сигнатуру, но это иллюстрирует общую проблему. Как только вещи станут более сложными, у вас будет все больше и больше предложений которые специфицируют типы вещей (разделяемые спецификации).

Альтернатива, которая работала для нас очень хорошо, это сторониться пометок непрозрачности, и вместо этого полагаться на механизм типов данных для того чтоб делать типы абстрактными. Тогда чтоб задать реализацию абстрактного типа отображений с целыми ключами, мы поступаем так:

structure IntMapping : MAPPING = struct
structure Key : ORDERED = Int
datatype ‘a bst = Empty | Node of ‘a bst * (Key.t * ‘a) * ‘a bst
type ‘a mapping = ‘a bst
val insert = …

Смысл тут в том что поскольку конструкторы типа `a bst не экспортируются в интерфейсе, то тип `a IntMapping.mapping будет абстрактным.
Так-же обратите внимание что использование пометки прозрачности на структуре Key гарантирует что ключи действительно будут целыми числами (типа, и не будут абстрактными, в точности как задумывалось. Данное определение позволит нам сформулировать простые правила сопоставления сигнатур (каждая спецификация в сигнатуре имеет соответствующее объявление в структуре), и позволит нам принудить границы абстракций без лишней суеты. Студенты не должны иметь абсолютно никаких проблем с этим вообще, и мы не должны иметь проблем структурируя наш код данным способом.

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

functor Referee
(structure Player1 : PLAYER and Player2 : PLAYER
sharing type Player1.Game.t = Player2.Game.t) : REFEREE = …

Спецификация разделения формулирует точно и кратко естественное ограничение согласования управляющее двумя игроками. Здесь снова, собака которой мы боялись, никогда не лает, и студенты находят все это вполне интуитивным и беспроблемным. Это позволяет им тратить их время на действительные сложности изучаемой проблемы, такие как способ думать о альфа-бета отсечении в параллельном поиске по игровому дереву, вместо того чтоб быть полностью связанными самой бюрократией структурирования кода.

Преимущество преподавания умным молодым студентам в том что они умны и они молоды. Их одаренность это, конечно, удовольствие. Мы тяжело работали чтоб прийти с достаточно интересными заданиями, и многие студенты испытывают нас своими решениями наших проблем. Их молодость означает что они приходят к нам с минимумом ошибочных представлений и сведений которые они подхватили на улице, и что они открыты для обучения методам которые полностью нестандартны (по крайней мере на данный момент) по отношению к тому что их друзья изучают в других университетах. Что делает УКМ особым местом так это именно то что студенты подталкиваются к интенсивным размышлениям способами, о которых они возможно бы и не подумали. Лично я надеюсь что больше университетов по всему миру подхватят то что мы начали, и дадут своим студентам те же преимущества которым уже радуются наши.

Вопрос Ленивости

Как я говорил ранее, есть несколько серьезных причин почему Хаскелл не подходит для преподавания вводного курса функционального программирования (прим.перев. по моему скромному мнению и для промышленного программирования тоже. это типичный исследовательский язык, из категории лиспа и скриптовых, а не инженерный. прототипы на нем писать удобно но потом их поддержка другим человеком не особо гладка. кстати степень простоты освоения языка студентами это один из индикаторов пригодности языка для обычного прикладного программирования,наряду с модульностью. не достаточный но необходимый. другими словами, большие текучие группы индусов/русских программистов по-моему чем-то похожи на группы студентов). Основная среди этих причин это ленивость, которая в контексте чистого функционального языка имеет фатальные последствия.
Во-первых, Хаскелл страдает от скудности типов. В Хаскелле невозможно определить ни тип натуральных чисел, ни тип списков натуральных чисел (как и списков чего-либо еще), ни любой другой индуктивный тип! (В стиле Льюиса Кэролла в Хаскелле имеются типы называемые «натуральные» и «списки», но это они так только называются, а не такими являются.) Во-вторых, язык имеет проблематичную стоимостную модель. Монументально тяжело рассуждать о том сколько времени, не говоря уж о том сколько памяти, использует программа на Хаскелле. Хуже того, параллелизм возникает естественно в энергичном, а не ленивом, языке (прим.перев. кстати это показывает недостаточную обоснованность утверждений Хаскеллистов о том что, мол, их язык замечательно параллелится. если подумать, сложная и гибкая семантика ленивого вычисления на самом деле должна скорее создавать проблемы, требовать синхронизаций, убивающих ускорение. самомодифицирующиеся эфемерные структуры данных плохо параллелятся). Например, вычисление каждого элемента конечной последовательности является фундаментальным для параллельных вычислений, однако несовместимо с идеологией ленивости, которая определяет что мы должны вычислять только те элементы которые потребуются далее (прим.перев. снова обращаю внимание как простая тупая задача обязательного вычисления всех элементов в любом порядке, моментально превращается в нечто со сложным динамическим поведением и требующее сложной реализации с согласованиями и синхронизациями. да, это будет иногда гибче, но… тормоза и затруднения с масштабированием тоже гарантированы. так же и параллельный сборщик мусора сам по себе тормознее обычного, сравните scala/jvm и камл).

Аргументы в поддержку ленивости никогда не казались мне убедительными. Кто-то заявлял что теория тождеств в ленивых программах считается более удобной; например, бета-редукция применима без ограничения. Но это имеет значение только до тех пор пока вы игнорируете другие типы в языке. Как Андржей Филински говорил десятилетия назад, там где ленивые языки содержат произведения (прим.перев. картезианские) но не объединения (прим.перев. суммы множеств), энергичные языки содержат объединения но не произведения. Делайте свою ставку, господа. Подобным же образом, там где ленивые языки полагаются на условия строгости (strictness), энергичные языки полагаются на условия всеобщности (totality). Преимущества и недостатки обоих вариантов двойственны, и похоже нет причины настаивать априори на одном наборе соотношений как на являющемся более важным чем другой.

Другое заявление это то что ленивость поддерживает определение бесконечных типов данных, таких как бесконечные последовательности значений некоторого типа. Однако ленивость не является необходимой, или даже реально полезной, для этой цели. Например, тип nat->nat является естественным представлением бесконечных последовательностей натуральных чисел которое поддерживает многие, но не все, операции конечных последовательностей (не поддерживает, например, операции такие как расположение в обратном порядке, которая не имеет смысла в случае бесконечных последовательностей). Вообще говоря, нет никакой неотъемлемой связи между ленивостью и такими бесконечностными типами. Ноам Зейльбергер разработал элегантную теорию энергичных и ленивых типов основанную на различении позитивных и негативных полярностей конструкторов типов, позитивные включают индуктивные а негативные включают коиндуктивные. Коиндуктивные типы не более связаны с ленивостью чем индуктивные типы связаны с указателями.

Я хочу показать что ленивость важна, но не для чистоты функционального программирования, а напротив только для функционального программирования в присутствии эффектов. Это принцип Канна-МакКвина, представленный в 1970-х Гиллесом Канном и Дэвидом МакКвином в их плодотворной работе по рекурсивным сетям преобразователей потоков. Дэн Ликата и я подчеркивали эту точку зрения на наших лекциях по ленивости в составе нашего нового вводного курса функционального программирования для первокурсников.

Давайте будем использовать потоки как наш мотивирующий пример, сравнивая их со списками, с которыми они перемешаны в Хаскеле. Список это пример позитивного типа, такого который определен своими условиями принадлежности (конструкторами). Определение функции над списком заставляет прибегать к сопоставлению с образцами, предоставляя один вариант для каждого конструктора (nil и cons), и используя рекурсию для применения функции к хвосту списка. Поток это пример негативного типа, такого который определяется своими поведенческими условиями (деструкторами). Определение потока заставляет прибегать к определению того как он себя ведет когда вычисляются его голова или хвост. Критический момент насчет списков, или любого позитивного типа, это то что они разграничивают (прим.перев. имеется ввиду граница между двумя сущностями которая их в некотором смысле и объединяет); как часть их семантики нам известно то как значение типа список строится. Критический момент насчет потоков, или любого негативного типа, это то что они ограничивают (прим.перев. проводят черту за которой нет уже ничего); как часть их семантики нам известно как они себя ведут когда разрушаются.

Поскольку у нас нет доступа к «внутренности» потока, мы должны думать о нем не как о статичной структуре данных, но как о динамическом процессе который производит, по запросу, последовательные элементы потока. Внутри себя, поток хранит информацию о том будет ли нужно определять последующие элементы; он имеет свое собственное состояние которое не видимо иначе снаружи. но если поток рассматривается как задаваемый процессом генерации, то он в сущности является эфемерной структурой данных. Взаимодействие с потоком меняет его состояние; «старый» поток теряется когда создается «новый» поток. Но, как мы обсуждали ранее, эфемерные структуры данных имеют ограниченную применимость. Роль мемоизации трансформировать эфемерный процесс в хранимую структуру данных путем сохранения последовательных значений производимых процессом так чтоб они могли быть «проиграны еще раз» если будет необходимо, и все это нужно чтоб позволить потоку иметь множественные будущие.
Таким образом, вместо того чтоб быть вопросом эффективности, мемоизация это вопрос функциональности, предоставляя обладающий хранимыми свойствами интерфейс к нижележащему эфемерному процессу.

Что-бы посмотреть как это работает на практике, давайте рассмотрим сигнатуры PROCESS и STREAM которые Дэн Ликата и я разработали для нашего курса. Вот вырезка из сигнатуры процесса:

signature PROCESS = sig
type ‘a process = unit -> ‘a option
val stdin : char process
val random : real process

Процесс это функция которая, когда применяется, генерирует значение некоторого типа, или сообщает что она завершена. Процесс stdin представляет стандартный поток ввода Юникса; процесс random это генератор псевдослучайных чисел. Сигнатура потоков выглядит по существу так:

signature STREAM = sig
type ‘a stream
datatype ‘a front = Nil | Cons of ‘a * ‘a stream
val expose : ‘a stream -> ‘a front
val memo : ‘a Process.process -> ‘a stream
val fix : (‘a stream -> ‘a stream) -> ‘a stream

Тип `a front это тип значений которые возникают когда поток наблюдается; он может либо завершиться либо предоставить элемент и другой поток. Конструктор memo создает хранимый поток из эфемерного процесса создания его элементов. Операция fix используется для создания рекурсивных сетей потоков. Там так-же есть и другие операции, но эти иллюстрируют суть абстракции.

Используя эти сигнатуры как основу, предельно легко подготовить набор процедур для скриптинга. Фундаментальными компонентами будут процессы которые генерируют элементы потоков. Комбинаторы на потоках, такие как композиция или отображение (map) и сокращение (reduce), легко определимы, и могут быть развернуты на местах (deployed) для построения более высоких уровней абстракции. Например, юниксовые утилиты, такие как grep, являются преобразователями потоков которые берут потоки как входы и производят потоки на выходах. Эти утилиты не выполняют ввод/вывод; они просто трансформируют потоки. Кроме того, поскольку потоки хранимы, никогда не возникает возни с «буферизацией» или «заглядыванием вперед» или «откатом»; вы просто манипулируете потоком как любой другой (хранимой) структурой данных, и все работает само собой. Классический стиль Лабораторий Белл чередований ввода-вывода с обработкой устраняется, приводя не только к более чистому коду, но так-же большей гибкости и реиспользованию. Это достигнуто не перебросами туда-сюда которые требуются механизмами наследования оо-языков, но вместо этого проведением четкого семантического различия между обработкой потоков и постановкой процессов на поток. Истинное реиспользование работает на уровне абстракций, а не на уровне кода который к ним приводит.

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

Обновление2: Леннар Аугустссон приводит свои причины почему ему нравится ленивость.
(прим.перев. далее приводится окончание сообщения Л.А.)

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

(прим.перев. Уважаемый Аугустссон, похоже вы переоцениваете важность реиспользования.
Любое реиспользование создает односторонние зависимости между частями программы и усложняет ее архитектуру. И эти усложняющие непроверяемые односторонние зависимости есть источник ВСЕХ программных проблем. Goto, указатели, threads, наследования, эфемерные данные (спасибо РХ), последовательное выполнение (спасибо РХ), слепое реиспользование и так далее… Все это односторонние зависимости и потому (в отличие от контролируемых реляционных двусторонних зависимостей) могут быть безопасно использованы ТОЛЬКО в комплекте с неким проверяющим целостность связей или управляющим механизмом. Примерами таких необходимых добавок будут — инкапсуляция goto в структурные управляющие конструкции, добавление сборщика мусора к языку с указателями, инкапсуляция threads в более высокоуровневые параллельные абстракции… и так далее.
Вам придется это сделать либо любые изменения в программе будут весьма болезненны. Это противоречит вашим словам о том что у реиспользования только достоинства. Вы получите и недостатки тоже. При изменениях программы возможна ситуация когда ее участки перестанут быть похожими друг на друга.
Мне так-же кажется что не так уж и просто реиспользовать функции высокого порядка или самодельные управляющие структуры. Монады вот вроде невозможно автоматически комбинировать в общем случае.
Вы по сути изобретаете свой собственный самопальный недокументированный язык, у которого возможны самые разные логические нестыковки с другими такими языками. Вот почему Хаскелл до сих пор смотрится нечитабельной академической игрушкой. Вспомните и статью Сполски об Астронавтах Архитектуры. Вспомните и другой важный принцип KISS (делай просто), который рекомендует делать все как можно более плоско и однородно, который в чем-то противоречит DRY. РХ не зря сказал насчет реиспользования в-большом, на уровне абстракций, подзадач, модулей. Модуль — довольно плоский набор типов, данных, операций. Не старайтесь идти в сторону упаковочного сумасшествия Форта. Думайте о реиспользовании как о преждевременной оптимизации. Пока еще не делайте его. )

Само собой в МЛ есть монады!

Есть популярное выражение в мире языков программирования звучащее «в Хаскелле есть монады», создающее впечатление что это отличительная особенность языка, отличающая его от всех остальных. В то время как верно, что Хаскелл популяризовал использование монад как механизма структурирования программ, сама идея монады это не столько момент дизайна языка (если не учитывать самопальную синтаксическую поддержку ее предоставляемую Хаскеллем), сколько момент дизайна библиотек. В конце концов, монада это просто одна из миллиардов сигнатур (классов типов) которыми структурируют программы, и нет никакой особой причины почему она не может быть использована в любом языке который поддерживает хоть чуточку модульности.
Однако всеж имеется особая причина почему монады распространились в Хаскелле, а именно, чтоб победить бич ленивости. Но даже при наличии монад, все еще требуются вещи типа seq для сериализации вычислений, поскольку ленивая стоимостная модель такая невыгодная. Забавный поворот истории в том что акцент на монады в Хаскелле означает что программирование на Хаскелле похоже на программирование на обновленном диалекте Алгола с более богатой структурой типов чем у оригинала, но общая структура та-же.

Рассматривая с точки зрения МЛ, монады есть частный случай модулей. Сигнатура монад задается определением

signature MONAD = sig
type ‘a monad
val ret : ‘a -> ‘a monad
val bnd : ‘a monad -> (‘a -> ‘b monad) -> ‘b monad

Имеется много, много, много структур которые удовлетворяют этой сигнатуре; мне не нужно (да в любом случае и не смогу) озвучивать все их здесь. Один из простых частных примеров должен быть достаточен чтоб показать общую идею:

structure Option : MONAD = struct
type ‘a monad = ‘a option
fun ret x = SOME x
fun bnd (SOME x) k = k x
| bnd NONE k = NONE

Это конечно монада option, которая иногда используется для моделирования моментов связанных с потоками данных в исключениях (exception), возможно с некоторой обработкой случая NONE для ассоциации значения исключения с безрезультатностью. (Моделирование потоков управления однако не моделируется правильно с помощью такого подхода. Для этого дополнительно необходимо иметь доступ к некоторой разновидности механизма переходов.)

Примеры наподобие этого весьма многочисленны. Монада представляется с помощью структуры. Любая структура предоставляющая возможности специфицированные сигнатурой MONAD приводит к характерной последовательной композиционности механизмов закодированных с ее помощью. Монадные трансформеры это функторы которые трансформируют одну монаду в другую, не требуя никакой суеты и беспокойства и всяких самопальных механизмов для этого. Стандартных техник модульного программирования достаточно для представления монад; кроме того упомянутые техники полностью универсальны, и равно применимы и к другим интересным нам сигнатурам (будь то стрелы, колчаны, луки и что там у вас есть) (прим.перев. тут автор очевидно в открытую прикалывается над Хаскеллистами, любящими вводить специальные обозначения для разных частных случаев, типа упомянутых стрелок. что является кстати прямым следствием из психологического профиля их гикнутого большинства, получающего удовольствие только от осознания что они знают некое редкое кунфу. необходимость в котором с практической точки зрения обычно обосновывается лишь наспех и без интереса к качеству обоснования. если вообще обосновывается. вот и выдумывают пятиколесные велосипеды. потому что это «круто»). Кроме того, в моей статье с Чакраварти и Дрейером показано как интегрировать модули в механизм вывода типов МЛ таким образом чтоб автоматически получать экземпляр функтора в тех ограниченных случаях где очевидно само собой что подразумевается (прим.перев. другими словами, автоматическая генерация монадных трансформеров в некоторых частных случаях). Все это было реализовано Карлом Крари в прототипе компилятора для расширения Стандартного МЛ, и было бы неплохо увидеть поддержку этого в более широко доступных компиляторах языка.

Основной объем мании насчет монад можно отнести поэтому на счет достоинств модулей.
Я однако ничуть не сомневаюсь, что вы гадаете насчет бесчестной монады IO в Хаскелле (и связанной с ней обходного пути unsafePerformIO).
Не является ли это как раз фундаментальной особенностью языка которую нельзя повторить в МЛ? Вряд ли! Это целиком и полностью вопрос проектирования сигнатур модулей библиотеки стандартного базиса (прим.перев. стандартной библиотеки МЛ идущей в комплекте), и ничего больше. Умолчальная библиотека базиса не пытается изолировать эффекты в монады, но можно совершенно прямолинейно сделать это самому, предоставив свой собственный слой поверх стандартного базиса, или реорганизовав стандартный базис чтоб принудить разделение. Например, сигнатура ссылочных ячеек может выглядеть наподобие этого:

signature REF = sig
type ‘a ref
val ref : ‘a -> ‘a ref IO.monad
val ! : ‘a ref -> ‘a IO.monad
val := : ‘a ref -> ‘a -> unit IO.monad

Здесь мы предполагаем что у нас есть четкое объявление

structure IO : MONAD = …

которое содержит в себе основные примитивы ввода-вывода которые уже реализованы в рантайме МЛ, более или менее наподобие того как в Хаскелле. Другие сигнатуры, такие как для мутабельных массивов или осуществления ввода/вывода, будут модифицированы в подобной манере чтоб упрятать эффекты в монаду IO. И вуаля, у вас получатся монадические эффекты, совсем как в Хаскелле.

На самом деле ничего особенного в этом нет. Фактически, все данное упражнение было уже проделано студентом УКМ, Филиппом Аджуксом, несколько лет назад. Он так-же написал несколько программ в таком стиле просто чтоб посмотреть как это все работает: гладко и плавно. Он так-же разработал синтаксические расширения для MoscowML компилятора которые предоставляют более удобную нотацию для программирования с использованием монад, наподобие того как в Хаскелле, но более в стиле общепринятых соглашений МЛ. (В идеальном случае должно быть возможно предоставлять синтаксическую поддержку для любой сигнатуры, не только монад, но мне неизвестны проработанные решения для такого общего случая, с учетом того что это будет дикая смесь синтаксического разбора и согласования типов.) (прим.перев. категорически несоглашусь. по-моему всякие дополнительные синтаксисы/макросы это ужасно плохая идея, текст программы приобретает контекстную зависимость и появляются как водится разные глюки от нестыковок этих синтаксисов. нет, нет, нет, Дэвид Блэйн, такая уличная магия нам не нужна)

Я хочу сказать что система модулей МЛ может быть реализована вами самостоятельно для принуждения разновидностей изоляции эффектов налагаемых на вас по умолчанию в Хаскелле. Нет ничего особенного в Хаскелле что делает это возможным, и нет ничего особенного в МЛ что могло бы это запретить. Это всего лишь режим использования модулей.

Тогда почему мы не сделали этого по умолчанию? Потому что это на самом деле не такая уж замечательная идея. Да, я знаю что на первый взгляд она смотрится чудесно, но потом вы осознаете что она довольно ужасна. Как только вы попадаете в монаду IO, вы застреваете в ней навечно, и ограничиваете себя до императивного программирования в стиле Алгола. Вы не можете легко конвертировать свой код между функциональным и монадическим стилями без радикальной его перестройки. И вам все равно неизбежно потребуется unsafePerformIO чтоб сделать что-либо серьезное. С практической точки зрения, вы лишаете себя полезной концепции благоприятных эффектов, и сама идея такого ограничения просто воняет!

Мораль всей истории это то что конечно «в МЛ есть монады», как и в Хаскелле. Захотите ли вы использовать их это ваше дело; они ровно настолько же полезны и раздражающе надоедливы в МЛ как и в Хаскелле. Но они вам не навязаны разработчиками языка!

Обновление1: Это сообщение возможно должно было называться «В МЛ есть монады, почему бы и нет?» или «Конечно в МЛ есть комонады!» но никто так и не заинтересовался такой возможностью (прим.перев. автор видимо имеет ввиду что есть много интересных вещей но все упоминают только пропиареные монады).

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

Семестр завершен

Единственной причиной по которой я начал этот блог было записать мой опыт полученный от нового курса функционального программирования для первокурсников в УКМ.
И вот преподавание завершено, итоговые экзамены проведены, и мы находимся в процессе получения дивидендов с того что мы достигли, и определения того что мы могли бы сделать лучше.
Это был первый год чтения данного курса, прочитанный 83-м первокурсникам курса компьютерных наук которые изъявили желание быть частью новой программы обучения. (Это составляет примерно 2/3 всего потока первокурсников.) Все прослушали новый курс по императивному программированию прочитанный Фрэнком Пфеннингом в предыдущем семестре, и все одновременно слушали курс 251, легендарный курс теоретических основ разрабатываемый у нас в течение последней дюжины или около того лет.

Начиная с этой осени (прим.перев. 2011) курс будет частью стандартной программы обучения, и будет преподаваться большему количеству студентов, включая радиотехнический факультет и всему факультету компьютерных наук. Мы все еще работаем над тем, должен ли стандартный порядок чтения курсов быть императивное-потом-функциональное либо функциональное-потом-императивное. Многое зависит от математической подготовки поступающих студентов. Те у кого математический скилл не прокачан (подавляющее большинство), но имеющие некоторый опыт программирования, скорее всего начнут с императивного программирования, и будут слушать его одновременно со стандартным курсом дискретной математики преподаваемым математическим факультетом. Те у кого математика прокачана, или высокие запросы, начнут с функционального программирования. Слабо образованное меньшинство погуляет один семестр, слушая дискретную математику и курс программирования для чайников, что-бы набрать обороты.

Наш новый курс структур данных и алгоритмов, разрабатываемый Гаем Блеллохом, будет доступен осенью для студентов которые уже прослушали императивный и функциональный курс. Гай планирует плотно пользоваться функциональным программированием, и будет делать упор на параллельные алгоритмы над хранимыми структурами данных как общим случаем, оставляя традиционный последовательный эфемерный случай для курса императивного программирования. Курс Гая это по сути продолжение (кхм) курса функционального программирования, которое делает упор на более навороченные структуры данных и алгоритмы, и более сложные проблемы программирования.

Для тех кому любопытно я прицепил к сообщению итоговый экзамен курса. Студенты справляются исключительно хорошо (средний балл 88%), хотя мы поначалу боялись что он будет слишком длинным и трудным. Разброс показателей был очень узок, возможно потому что экзамен был слишком прост, или потому что это был класс добровольцев и потому их скиллы были равномернее и сильнее обычных.
Мы соберем больше информации к зиме когда мы прочитаем курс большему количеству стулдентов. Я полагаю что экзамен отражает реальную ситуацию того что мы ожидали от них чтоб они могли делать под конец, и они действительно показали нам что они на это способны. Определенно это успех курса!

15-150 Итоговый Экзамен (Весна 2011)

Многомерная теория типов

(прим.перев. В данном сообщении приводятся некоторые интересные научные находки Р.Х. но мне кажется они будут менее интересны основному количеству наших читателей, и менее важны в плане популяризации языка МЛ, так что их можно перевести и потом)

Трансформации как строгие группоиды

(прим.перев. В данном сообщении приводятся некоторые интересные научные находки Р.Х. но мне кажется они будут менее интересны основному количеству наших читателей, и менее важны в плане популяризации языка МЛ, так что их можно перевести и потом)

Типы и ячейки

(прим.перев. В данном сообщении приводятся некоторые интересные научные находки Р.Х. но мне кажется они будут менее интересны основному количеству наших читателей, и менее важны в плане популяризации языка МЛ, так что их можно перевести и потом)

Сердечный приступ

Хочу просто ответить на вопросы некоторых людей и сказать что я все еще тут, и вскоре планирую продолжить писать в блог. Просто я сейчас несколько занят более срочными делами, включая преподавание в Орегонской летней школе языков программирвоания (OPLSS), подготовку публикации в POPL, посещение Института программных систем имени Макса Планка, и наконец изо всех сил пытаюсь закончить свою книгу (по которой у меня был значительный прогресс в течение лета).

Слова имеют значение

Вчера, в течение очень хорошей презентации Охада Каммара в УКМ, обсуждение сошло с рельсов, в частности, по причине стандартной, хотя и ни на чем не основанной, терминологической неразберихи относительно слова «переменная».
И я буду настолько глуп что попробую ее исправить.

Проблема в том что мы были приучены путать переменные с переменными — то есть программные переменные с математическими переменными. Различие в основе. С незапамятных времен (ну, как минимум начиная с Мухаммада ибн Мусы аль-Хорезми) у нас было понятие переменной, правильно называемой так, поскольку она получает значение путем подстановки. Переменная это неизвестная, или неопределенная, величина которая может быть заменена любым значением своего типа ( тип является, по крайней мере со времен Бертрана Расселла, областью значений переменной). Готлиб Фреге провел первое систематическое изучение кванторов, а Алонзо Черч использовал критически важную концепцию переменной чтоб сформулировать наиболее первичную и широко применимую модель вычислений, лямбда-исчисление.

С рассвета Фортрана нечто что не является переменной начало называться переменной. Программная переменная, в смысле Фортрана и любого императивного языка с тех пор, не получает значение путем подстановки (прим.перев. имеется ввиду что нормальная математическая переменная есть обозначение некоей сущности и как таковое либо еще не действительно либо уже раз и навсегда определено. яблоко всегда останется яблоком. оно не может называться яблоком а являться апельсином. ведь смысл обозначения в точности и значит вам надо будет сказать уже апельсин-называемый-яблоком. в противоположность этому, аппаратные ограничения первых компьютеров привели к тому что программные переменные стали скорее не обозначением самих сущностей, а обозначениями ящиков в которых эти сущности временно и поочереди находятся. поскольку задачу просто нельзя было втиснуть в то железо целиком в хранимом параллельном виде и приходилось реиспользовать и память и процессор, назначая им разные функции с течением времени. так все императивное и получилось — как приемы борьбы с ограничениями железа используя разнесение по времени. этакое программирование четырехмерного железа. в частности поэтому мне кажется что доля императивности всегда останется, но конечно та доля которая не имеет недостатков).
Вместо этого, программная переменная получает значение путем (как минимум) двух операций связанных с ней, одна для получения ее содержимого и одна для помещения в нее нового содержимого. (И возможно, операция для получения ссылки на нее, как в С или даже Алголе.) Сейчас, как многие из вас знают, я полагаю что концепция программной переменной в этом смысле есть очень плохая идея, и уж по крайней мере далеко не настолько важная какой она сделана в стандартных (включая объектно-ориентированные) языки, но на этом мы остановимся в другой раз.

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

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

Так что мое предложение: давайте называть переменные переменными и давайте называть эти другие штуки назначаемыми. В перспективе развития ИТ (то есть когда ярмо императивного программирования будет снято) нам возможно более не потребуется это различие. Но до тех пор, почему бы не провести это различие правильно?

Обновление: Похоже стоит упомянуть что в ПОЯП у меня есть свежее (как мне известно) толкование концепции ссылки, что будет подробнее рассмотрено в следующем сообщении блога.

Прозрачность ссылок

После прочтения некоторых комментариев к моему сообщению слова-имеют-значение, я подумал что стоит прояснить толкование ссылок в ПОЯП. Большинство людей удивляются когда обнаруживают что я отделил концепцию ссылки от концепции изменяемой памяти. Я осознаю что мое толкование не стандартно, но я считаю что одна из вещей которые я понял пока писал книгу это то как надо формулировать ссылки так чтоб концепция ссылки была отделена от той вещи на которую она ссылается. Если сделать так это позволит проводить замечательно единообразный подсчет ссылок возникающий в ситуациях самого разного типа, и являющийся основой для, в числе прочих вещей, нестандартного, но я полагаю более ясного, толкования связи в исчислении процессов.

Нет смысла для меня пытаться воспроизвести всю информацию тут в коротком сообщении, так что я ограничусь несколькими комментариями которые возможно побудят вас прочесть все полностью в ПОЯП.

Имеется, прежде всего, общее понятие символа, или имени, на базе которого строится большая часть выводов. Возможно наиболее важной вещью которую следует понять о символах по моему мнению, является то что символы не есть формы значений. Они вместо этого есть скорее индексы в бесконечном, открытом (расширяемом) семействе операторов для формирования выражений. Например, когда кто-то вводит символ a как имя назначаемого, что он делает так это вводит два новых оператора, get[a] и set[a], для получения и установки содержимого этого назначаемого. Подобным же образом, когда некто вводит символ a для использования как имени канала, он вводит операторы send[a] и receive[a] которые работают с каналом по имени a. Суть тут в том что эти операторы интерпретируют символ; например, в случае изменяемого состояния, операторы get[a] и set[a] есть то что заставляет его быть состоянием, что отличается от некоторого другого использования символа a как индекса для некоторого другого оператора. При этом не требуется чтоб состояние формулировалось используя «ячейки»; каждый может с тем же успехом использовать каркас алгебраических эффектов придуманный Плоткиным и Павером чтобы назначить динамическую семантику этим операторам. В данный момент меня не беспокоит как эта динамика формулируется; меня интересуют лишь законы которые она соблюдает (это как раз суть подхода Плоткина/Павера как я его понимаю).

С каждым символом a связан тип который, спешу подчеркнуть, не есть тип самого символа (символы не являются чем-то типизированным) a, но только лишь связан с ним (прим.перев. тип связан с этим символом посредством a). Например, если a имеет ассоциированный тип nat, то get[a] будет командой возвращающей число, а set[a](e) будет принимать число e как аргумент. Подобным же образом для каналов, а так-же других применений символов как индексов для других операторов.

Имея символ a с ассоциированным типом T, можно сформировать ссылку на a, записываемую &a, как значение чей тип, в случае ссылки на назначаемое, будет, скажем, T-ссылка-на-назначаемое, или что-то похожими словами.
Этот тип интерпретируется сокращением форм которые берут значение как аргумент, и переходом к соответствующему оператору для данного назначаемого: getref(&a) переходит в get[a], и setref(&a;e) переходит в set[a](e). Подобные же правила управляют другими применениями символов. Операция «ref» просто разименовывает символ (определяет на какое назначаемое он ссылается, в случае назначаемых), и подготавливается к дальнейшей интерпретации указанного символа. В случае исчисления процессов передача каналов производится с использованием ссылок на каналы, и имеются операции которые определяют событие на базе ссылающегося на значение типа ссылки на канал (прим.перев. я и сам не понял что написал). (Это значительно проясняет, с моей точки зрения, некоторый беспорядок в п-исчислении, и приводит к намного более хорошо себя ведущей теории эквивалентности процессов.)

Назначение области действия символам, или именам, поддерживается независимо от их интерпретации. Можно применять либо ограниченную областью либо глобальную интерпретацию символов. Ограниченные областью символы имеют ограниченную область применения (прим.перев. в английском языке есть несколько слов которые можно перевести на русский как «ограниченный», поэтому и получилось тут «масло масляное». сначала говориться о принадлежности символов некоей общности-области а потом о ограниченности той области которую составляют применения символа. в-общем тут две области и обе они ограничены); свободные символы имеют неограниченную применимость. Концепция мобильного типа, приспособленная из нашей работы над ML5, управляет взаимодействием между объявлениями с ограниченной областью и процессом оценки (концепция может быть прочитана в книге)(прим.перев. ПОЯП конечно, кто-бы сомневался. настоящий мужик/ученый должен сделать в своей жизни три вещи — построить дом/книгу, посадить дерево/в-лужу-оппонента, вырастить сына/фанатичных-последователей. шучу, конечно. Харпер молодец). Одним из следствий этого является то что можно формировать ссылки как на ограниченные так и на глобальные назначаемые, независимо от дисциплины управления областями. Другими словами я сознательно ломаю стандартную (и, полагаю, ошибочную) связь между областью применения назначаемого и формированием на него ссылки (прим.перев. тут я не рискну согласиться с автором). Зачастую люди смешивают ссылки с состоянием и с глобальной применимостью; я сознательно не следую этому соглашению, поскольку полагаю что оно наводит беспорядок в способах, с которыми лучше работать в манере которую я описываю. Так, например, как мне помнится в Алголе у меня не было проблем в введении ссылок на назначаемые ограниченной области, и в передаче их как аргументов в процедуры, например (прим.перев. тут автор по-моему ведет себя как императивщик восхищающийся мощью указателей. я согласен с тем что в случае хранимых неизменных областей, в функциональном стиле, нет особенных проблем со ссылками между ними. однако в том-же Алголе области были эфемерные, несмотря на сборщик мусора. в-общем не знаю. не нравится мне сама идея ссылок между областями. может это я неправильно понял про что он. а раз я не въехал то и другие могут). Сначала я нашел эту ситуацию удивительной, но потом как только рассмотрел ее более тщательно, вполне естественной.

Наконец, позвольте мне упомянуть что критическая особенность назначаемых (фактически и символов вообще) это то что они позволяют неравенство. Два разный назначаемых, скажем a и b, никогда и ни при каких условиях выполнения, не могут быть синонимами друг для друга: присваивание одной никогда не заденет содержимое другой. Синонимичность это свойство ссылок, поскольку две ссылки, скажем привязанные к переменным x и y, могут ссылаться на то-же самое нижележащее назначаемое, но два разных назначаемых никогда не будут синонимами друг для друга. Вот почему «конверсия присваивания» как это называется в Схеме, ни коим образом не является адекватным ответом на мое заявление о необходимости смены терминологии (прим.перев. видимо он про слова-имеют-значение)! Назначаемые и переменные это разные вещи, а ссылки это третий вид, отличный от первых двух.