Эта статья пролежала в черновиках больше года. Решив открыть её сегодня, я понял, что на самом деле она готова на 90%. В связи с этим я решил добить всего пару абзацев и, наконец, её опубликовать. А всё самое интересное уже положить в следующие выпуски (с моей скоростью публикаций, видимо, года через два).

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

\[ \forall n, m \in \mathbb{N}, n + m = m + n \]

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

Погодите, а зачем это всё?

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

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

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

Есть еще товарищи, искренне считающие, что подобные методы позволят выпускать более качественное программное обеспечение, но я в последнее время отношусь к этому довольно скептически. Почему я в это не верю? Несмотря на то, что в этом цикле постов я буду доказывать, как вся эта магия проста и понятна, на самом деле применение таких подходов к разработке программного обеспечения — это очень сложно. Трудозатраты на формальное доказательство значительно превосходят затраты на те же тесты, тогда как разница между 100% и 99% надежностью системы не так критична. Существует исключительно мало областей, в которых готовы переплачивать за этот процент, а потому, эта сфера так и останется маргинальщиной.

Два слова про типы

Рассказывать подробно CoC (Calculus of Constructions) и CiC (Calculus of Inductive Constructions), на котором построены все современные языки с зависимыми типами, которые и используются для доказательств, я не буду. Но какие-то базовые вводные слова сказать стоит.

Типы можно рассматривать как некоторую альтернативу множествам, долгое время игравших роль "базового языка" математики. Другими словами, исходя из простейшей аксиоматики множеств (активно изучаемой в школах и на младших курсах технических ВУЗов) можно придти к произвольным математическим конструкциям от натуральных чисел до многомерных геометрических объектов. К сожалению, несмотря на свою аксиоматическую простоту и описательную мощность, сама теория множеств обладает фундаментальным недостатком: она противоречива, а значит, при желании её инструментарий позволяет доказать что угодно, в том числе очевидно ложные утверждения.

Еще одна широко используемая в школьной математике вещь, от которой стоит отказаться — это неконструктивность доказательств, то есть доказательство какого-то факта не позволяет вам получить доказываемый объект. Например, вы доказываете что существуют два иррациональных числа a и b, такие что \( a^b \) — рациональное. Но при этом не предъявляете сами эти числа. Ну, и зачем нам такое доказательство?

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

Теория типов (точнее, тот вариант, что мы будем здесь рассматривать) устанавливает жесткую иерархию на принадлежность объектов (термов) каким-либо скоплениям — типам. Так, все примитивные объекты будут лежать в тех или иных множествах — типах нулевого порядка, образующих вселенную таких типов Type 0, однако сами множества не могут лежать в других множествах. Вместо этого они будут принадлежать некоторым более крупным структурам — типам первого порядка (Type 1). Аналогично продолжая, мы можем получить правило, что каждый тип порядка u будет лежать в типе порядка u+1, то есть Type u : Type (u+1). Это позволяет избежать парадоксов, внеся еще больше строгости в описание рассматриваемых конструкций. Последним дополнением является кумулятивное вложение вселенных типов друг в друга. Это значит, что любой тип лежит не только в типе уровня на единицу больше, но и во всех типах более высокого порядка.

Под интуиционизмом в самом простом виде мы будем понимать отсутствие аксиомы исключенного третьего (A ∨ ¬A) или, что то же самое, закона снятия двойного отрицания (¬¬A → A). С философской точки зрения это означает, что из опровержения некоторого факта не следует доказательство его отрицания. Другими словами, единственный способ доказать что-то в интуиционизме — привести конструкцию (тот самый конструктивный метод доказательства). Например, для доказательства существования натуральных чисел меньше 10 требуется предъявить хоть одно такое число. А для доказательства упоминаемого выше факта коммутативности сложения натуральных чисел требуется показать, способ приведения обеих частей к одинаковому результату. Далее мы активно будем пользоваться этим соображением, предъявляя конкретные примеры термов, имеющих типы, содержащие утверждения, которые мы хотим доказать.

Setup

Скачать Lean 3 можно с GitHub или в репозиториях вашей операционной системы операционных систем. Пока этот текст готовился, ветка 3.х была заморожена (но продолжается в виде community ветки), сейчас в активной разработке версия 4, но она пока крайне недружелюбна к пользователям.

Для полноценного использования языка нам потребуется совместимая IDE, к которым в настоящий момент относятся Emacs, VIM и VS Code. Я пользуюсь последней, где вся работа выглядит вот так:

В языке активно применяется юникод, писать который можно и самому. Так, для получения красивого символа ℕ достаточно в VS Code ввести \nat, а красивая лямбда (λ) будет задаваться через \fun или \lam. Главным недостатком использования Lean в VIM, пожалуй, является отсутствие нормальной поддержки этой фишки. В остальном работать не менее удобно:

Hello World

Lean — язык, разработанный в первую очередь для формальной верификации, а не программирования в привычном понимании слова. Тем не менее мы можем легко вывести любую строку на экран с помощью команды #print. Для этого мы можем создать простейший файл (скажем, hello_world.lean):

#print "Hello World!"

И запустить его из консоли следующим образом:

$ lean hello_world.lean
Hello, World!

Далее мы не будем пользоваться консольным запуском, предпочитая вместо этого работу в интерактивной среде. Однако писать на Lean можно хоть в Блокноте: все команды, начинающиеся с # будут выводить информацию в stdout при запуске на них интерпретатора Lean.

Вывод типа

Базовой командой, которой мы постоянно будем пользоваться, является команда #check, осуществляющая проверку типа некоторого выражения. Вот несколько примеров её использования:

#check 5
#check 'a'
#check tt

Каждая из этих строчек в процессе выполнения вернет тип выражения. Ими станут:

5   : ℕ
'a' : char
tt  : bool

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

#check ℕ
#check fun x, x + 1

Вернет, соответственно:

ℕ                : Type
λ (x : ℕ), x + 1 : ℕ → ℕ

Стрелочная конструкция также может быть протипизирована (для рисования красивой стрелочки требуется воспользоваться сокращением \r):

#check ℕ → ℕ

Такая конструкция, ожидаемо, вновь вернет Type.

Сама конструкция Type может быть протипизирована, ведь это некоторый тип, а типы в Lean, как мы уже сказали, являются объектами первого класса.

#check Type

Поскольку Lean является языком исчисления предикативных индуктивных конструкций, то все типы образуют в нем кумулятивную иерархию. Тип Type (0) лежит в Type 1 и всех более высоких вселенных (Type n). Наш запрос отобразит нам ближайшую:

Type : Type 1

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

#check prod ℕ ℕ
#check ℕ × ℕ
#check (1, 1)          -- будет иметь тип ℕ × ℕ

#check sum nat bool
#check nat ⊕ bool

Вычисление и редукция

Как и в любом нормальном языке программирования мы можем попросить Lean вычислить значение некоторого выражения. Для этого используется команда #eval:

#eval 1 + 2                                 -- 3
#eval (λ x, x + 39) 3                       -- 42
#eval tt && ff                              -- ff

Не все вычисления, однако, заканчиваются каким-то результатом — значением, представимом в виде элементарного машинного типа. В связи с этим более распространенной конструкцией является команда #reduce, приводящая результат в виде нормальной формы:

#reduce (λ x y, x) 1                        -- λ (y : ?M_1), 1

Вывод в данном случае заодно показал нам, как можно специфицировать тип в лямбда-абстракции (использовать стиль Чёрча). Можно воспользоваться этим в следующем примере:

#reduce (λ (x : ℕ) (y : ℕ), x + 10) 1 4     -- 11

В принципе, командой #reduce вместо #eval можно пользоваться всегда. Последняя имеет лучшую производительность, но пока мы не применяем Lean для программирования общего назначения, это не так важно, как удобство однообразия.

Функции

Разумеется, писать на одних лишь только лямбдах было бы весьма неудобно, а потому в Lean есть механизм связывания имен с различными термами. Например, так мы можем задать константную (нулярную) функцию foo, возвращающую натуральное число 5:

def foo : ℕ := 5

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

def my_bool : Type := bool

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

def add1 (n : ℕ) (m : ℕ) : ℕ :=
    n + m

def add2 (n m : ℕ) : ℕ :=
    n + m

def add3 (n : ℕ) : ℕ → ℕ :=
    λ m, n + m

def add4 : ℕ → ℕ → ℕ :=
    λ n m, n + m

Поддержка зависимых типов позволяет в типе возвращаемого значения использовать аргументы. Это значит, что в стрелке A → B тип B зависит от значения a, иными словами, a как-то участвует в записи B. Такую конструкцию принято записывать в виде Π (a : A), B. Приведенная же выше стрелка является синтаксическим сахаром для частного случая, когда B от a не зависит. Тем не менее можно написать полную дешугаризированную версию:

def add5 : Π (n : ℕ), Π (m : ℕ), ℕ :=
    λ n m, n + m

Разумеется, как любой приличный язык, Lean поддерживает довольно-таки продвинутый pattern matching аргументов, что позволяет объединить все имеющиеся у нас знания и применить их для получения чего-нибудь очень практически полезного. Например, функции вычисления чисел Фибоначчи:

def fib : ℕ → ℕ
| 0 := 1
| 1 := 1
| (n + 2) := fib n + fib (n + 1)

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

Однако, спустя почти сутки после публикации, мы поняли, что не на том хайповали. 😂

Во-первых, начиная с macOS Mojave, Apple полностью перешла на свой фреймворк Metal 2, не только убив поддержку NVidia CUDA (до свидания MatLAB, Photoshop, несколько десятков удобный утилит и вся рабочая разработка на CUDA C/C++), но и усложнив работу с OpenGL.

Во-вторых, сейчас вся разработка интерфейсов построена на web-технологиях, и именно эта область развивается быстрее всего. Это значит, что для построения нормального переиспользуемого решения, которое не будет объявлено deprecated уже через полгода после выпуска, также стоит поддаться web тренду. Ведь даже среда разработки, которой я иногда пользуюсь для Haskell — это Visual Studio Code, построенный на основе Electron (сейчас, правда, его почти полностью вытеснил SpaceVim). На нем же работает приложение Ghost (в котором пишется этот текст), а также Slack, Skype и многие другие программы общего пользования.

В качестве примера я решил рассмотреть Three.JS, предоставляющий высокоуровневые интерфейсы для использования WebGL, который, как я надеюсь, следует знакомым мне принципам OpenGL. Так как до этого я веб-разработкой никогда не занимался, меня сильно смутил весь окружающий её тулинг. Этой заметкой я хочу зафиксировать свой путь создания простейшего проекта.

В мире web-разработки безраздельно правит JavaScript, а в мире JavaScript связка node + npm, позволяющая использовать его не только для браузерной разработки, но и писать удобные консольные инструменты. В том числе для сборки классических браузерных проектов. 😊

Но для начала создадим максимально глупый код, состоящий из трех файлов: верстки, стиля и скрипта отрисовки.

<!doctype html>
<html>
  <head>
    <title>Пример</title>
    <!-- Подключаем файл со стилями -->
    <link rel="stylesheet" type="text/css" href="style.css" />
  </head>
  <body>
    <!-- Создаем контейнер, в котором будет происходить отрисовка -->
    <div id="container"></div>
    <!-- Подключаем ThreeJS с официального сайта -->
    <script src="https://threejs.org/build/three.js"></script>
    <!-- Подключаем файл со скриптом, который будет делать отрисовку -->
    <script type="text/javascript" src="app.js"></script>
  </body>
</html>

body {
  background-color: #000;
  margin: 0px;
  overflow: hidden;
  color: white;
  text-align: center;
}

#container {
  position: absolute;
  width: 100%;
  height: 100%;
}

var container = document.querySelector('#container');


var scene = new THREE.Scene();
scene.background = new THREE.Color('skyblue');

var fov = 35; // AKA Field of View
var aspect = container.clientWidth / container.clientHeight;
var near = 0.1; // the near clipping plane
var far = 100; // the far clipping plane

var camera = new THREE.PerspectiveCamera(fov, aspect, near, far);
camera.position.set(0, 0, 10);

var geometry = new THREE.BoxBufferGeometry(2, 2, 2);
var material = new THREE.MeshBasicMaterial();
var mesh = new THREE.Mesh(geometry, material);
scene.add(mesh);

var renderer = new THREE.WebGLRenderer();

renderer.setSize(container.clientWidth, container.clientHeight);
renderer.setPixelRatio(window.devicePixelRatio);

container.appendChild(renderer.domElement);
renderer.render(scene, camera);

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

На самом деле, работать, конечно, можно и так. Но мы сталкиваемся с рядом ограничений, терпеть которые людям, пришедшим из тепличной backend-разработки решительно невозможно, а именно:

• невозможность разбиения кода на модули;
• зависимость от кода на удаленном сервере;
• ограничение vanila-JS, который неравномерно развивается в разных браузерах;
• отсутствие проверок кода и выполнения на нем каких-либо CI процедур;
• необходимость вносить изменения сразу в несколько мест (html, css, js);
• и многое другое...

Будем последовательно бороться с этими недугами.

Создание npm-проекта

В первую очередь создадим проект в нашей директории:

$ npm init -y
Wrote to /prjoect/path/package.json:

{
  "name": "example-project",
  "version": "1.0.0",
  "description": "",
  "main": "app.js",
  "scripts": {
    "test": "echo \"Error: no test specified\" && exit 1"
  },
  "keywords": [],
  "author": "",
  "license": "ISC"
}

Теперь её содержимое выглядит так:

$ tree .
.
├── app.js
├── index.html
├── package.json
└── style.css

0 directories, 4 files

Содержимое package.json еще можно подредактировать, указав автора и прочую мета-информацию, мы же перейдем к следующим шагам.

Подключение webpack

Одна из главных болей — это, конечно, невозможность использовать модули при нашей разработке. Её, и не только, решает превосходная утилита Webpack, также являющаяся почти незаменимой в каждом современном проекте. Для её использования у нас требуется ввести всего лишь команду установки:

$ npm install --save-dev webpack webpack-cli
...
+ webpack-cli@3.3.7
+ webpack@4.39.3
added 453 packages from 237 contributors and audited 5286 packages in 13.776s
found 0 vulnerabilities

Теперь мы можем собирать один JS-"бандл" из нескольких модулей. Воспользуемся этим для того, чтоб подключить ThreeJS:

$ npm install --save three
...
+ three@0.108.0
added 1 package from 1 contributor and audited 5287 packages in 2.73s
found 0 vulnerabilities

Теперь мы можем добавить в наш файл app.js подключение ThreeJS:

var THREE = require('three');
...

Из index.html можно убрать строчку подключения библиотеки со стороннего CDN. Но это не единственное изменение, которое нам потребуется сделать в HTML-файле. Дело в том, что результатом "сборки" будет не модификация JS-файла и даже не добавление новых строчек в HTML — это будет создание нового JS, который будет содержать в себе весь используемый код. По умолчанию такой бандл будет лежать в dist/main.js, а потому на него и сошлемся. Итоговый вид нашего index.html будет:

<!doctype html>
<html>
  <head>
    <title>Пример</title>
    <!-- Подключаем файл со стилями -->
    <link rel="stylesheet" type="text/css" href="style.css" />
  </head>
  <body>
    <!-- Создаем контейнер, в котором будет происходить отрисовка -->
    <div id="container"></div>
    <!-- Подключаем файл со скомпилированным javascript -->
    <script type="text/javascript" src="./dist/main.js"></script>
  </body>
</html>

Как же теперь собрать наш проект? Для этого в скрипты файла package.json нужно добавить соответствующую команду:

...
  "scripts": {
    "test": "echo \"Error: no test specified\" && exit 1",
    "build": "webpack --mode production"
  },
...

Теперь проект может быть собран командой:

$ npm run build

> example-project@1.0.0 build /path/to/project
> webpack --mode production


Insufficient number of arguments or no entry found.
Alternatively, run 'webpack(-cli) --help' for usage info.

Hash: c8e9ac5d52d7c3c70555
Version: webpack 4.39.3
Time: 52ms
Built at: 04.09.2019 09:56:46

ERROR in Entry module not found: Error: Can't resolve './src' in '/path/to/project'
npm ERR! code ELIFECYCLE
npm ERR! errno 2
npm ERR! example-project@1.0.0 build: `webpack --mode production`
npm ERR! Exit status 2
npm ERR!
npm ERR! Failed at the example-project@1.0.0 build script.
npm ERR! This is probably not a problem with npm. There is likely additional logging output above.

npm ERR! A complete log of this run can be found in:
npm ERR!     /home/dir/.npm/_logs/2019-09-04T06_56_46_316Z-debug.log

Кажется, что-то пошло не так. Действительно, Webpack по умолчанию ищет все JS-файлы в директории src, а главный файл ожидает увидеть под именем index.js. Поможем ему:

$ mkdir src
$ mv app.js src/index.js
$ npm run build

> example-project@1.0.0 build /path/to/project
> webpack --mode production

Hash: 9a8895c35652a46d21af
Version: webpack 4.39.3
Time: 706ms
Built at: 04.09.2019 10:05:35
  Asset     Size  Chunks                    Chunk Names
main.js  587 KiB       0  [emitted]  [big]  main
Entrypoint main [big] = main.js
[0] ./src/index.js 842 bytes {0} [built]
    + 1 hidden module
...

Скорее всего мы увидим еще несколько предупреждений (они связаны с тем, чот получившийся бандл слишком большой — мы добавили в него всю библиотеку ThreeJS, а не только нужные нам функции), но мы пока их проигнорируем и насладимся результатом, открыв index.html. Браузер покажет нам ровно тот же белый квадрат на голубом фоне.

Пакуем HTML

Во время наших манипуляций с компиляцией JS-файлов нам пришлось также менять и наш HTML. В будущем таких манипуляций может быть еще много, а потому почему бы не научиться генерировать часть этого HTML автоматически? Webpack поможет нам и в этом. Но для этого нужно научиться его конфигурировать.

Вся конфигурация сборки с помощью Webpack описывается в специальном файле webpack.config.js. Создадим базовую болванку такого файла:

module.exports = {
  // Здесь указываем, какой файл считать главным.
  entry: './src/index.js',
  // Скомпилированный бандл положим под именем main.js.
  output: {
    filename: "main.js"
  },
  module: {
    rules: [
    // Здесь мы будем описывать правила трансформаций, которые будут
    // применяться к файлам различного типа.
    ]
  },
  // Здесь мы применим различные плагины, расширяющие возможности Webpack
  plugins: [
  ]
};

Запуск npm run build приведет ровно к тому же результату, поскольку мы, фактически, воспроизвели конфигурацию по умолчанию. При изменении output.filename нам опять придется менять index.html. Чтоб этого не делать мы можем воспользоваться волшебным плагином HtmlWebpackPlugin. Для начала поставим его, а также HTML-загрузчик, который нам также потребуется:

$ npm install --save-dev html-webpack-plugin html-loader
...
+ html-loader@0.5.5
+ html-webpack-plugin@3.2.0
added 63 packages from 75 contributors and audited 5407 packages in 4.757s
found 0 vulnerabilities

Как несложно догадаться, теперь нам потребуется промодифицировать конфиг Webpack`а:

// Импортируем модуль плагина в нашу конфигурацию.
var HtmlWebpackPlugin = require("html-webpack-plugin");

module.exports = {
  entry: './src/index.js',
  output: {
    filename: "main.js"
  },
  module: {
    rules: [
      {
        // Для всех файлов HTML
        test: /\.html$/,
        use: [
          {
            // Воспользуемся загрузчиком html-loader
            loader: "html-loader",
            // Который заодно проминимизирует наш HTML
            options: { minimize: true }
          }
        ]
      }
    ]
  },
  plugins: [
    // Скопируем наш index.html в папку dist
    new HtmlWebpackPlugin({
      template: "./index.html",
      filename: "./index.html"
    })
  ]
};

Также удалим из index.html вызов скрипта, теперь Webpack подставит его самостоятельно:

<!doctype html>
<html>
  <head>
    <title>Пример</title>
    <!-- Подключаем файл со стилями -->
    <link rel="stylesheet" type="text/css" href="style.css" />
  </head>
  <body>
    <!-- Создаем контейнер, в котором будет происходить отрисовка -->
    <div id="container"></div>
  </body>
</html>

После npm run build теперь содержимое dist будет таким:

$ tree dist
dist
├── index.html
└── main.js

0 directories, 2 files

Новый index.html теперь избавлен от комментариев и содержит вызов скрипта. А потому мы можем увидеть наш знакомый белый квадрат при его открытии (NB: это неправда!). Сам скрипт теперь можно переименовывать как угодно, всё сохранится.

Пакуем CSS

Если открыть-таки index.html, то можно заметить, что в предыдущем абзаце я соврал: никакого квадрата не будет, по причине того, что наш контейнер был нулевого размера — ведь никакие стили не были импортированы. Конечно, мы можем скопировать их вручную, и все заработает. Но зачем это делать, если Webpack может взять это на себя?

Традиционно начнем с добавления пары модулей в режиме разработки:

$ npm install --save-dev css-loader style-loader
...
+ style-loader@1.0.0
+ css-loader@3.2.0
added 16 packages from 47 contributors and audited 5543 packages in 3.974s
found 0 vulnerabilities

Также промодифицируем файл конфигурации Webpack. А именно, в секцию module.rules добавим следующее:

...
{
    test: /\.css$/,
    use: [
        {
            loader: "style-loader"
        },
        {
            loader: "css-loader"
        }
    ]
}
...

Теперь нам нужно указать, откуда брать файл со стилем. Для этого уберем строчку подключения стилей из index.html и добавим строчку подключения стилей в наш JavaScript:

<!doctype html>
<html>
  <head>
    <title>Пример</title>
  </head>
  <body>
    <!-- Создаем контейнер, в котором будет происходить отрисовка -->
    <div id="container"></div>
  </body>
</html>

var css = require("./../style.css");
var THREE = require("three");
...

Теперь наш Webpack с помощью css-loader подгрузит наши стили прямо в JavaScript, и нам больше не придется ничего копировать. Команды npm install и npm run build теперь будут собирать полностью рабочий проект без необходимости что-либо доделывать руками. Это покрывает создание базового проекта web-приложения без каких-либо надстроек или дополнительных фишек типа поддержки новых версий ECMAScript. О них мы поговорим в другой раз.

Итоговый проект будет выглядеть так (автоматически скачиваемые или генерируемые файлы скрыты):

$ tree
.
├── index.html
├── package.json
├── src
│   └── index.js
├── style.css
└── webpack.config.js

1 directory, 5 files

{
  "name": "example",
  "version": "1.0.0",
  "description": "",
  "private": true,
  "scripts": {
    "test": "echo \"Error: no test specified\" && exit 1",
    "build": "webpack --mode production"
  },
  "keywords": [],
  "author": "",
  "license": "ISC",
  "devDependencies": {
    "css-loader": "^3.2.0",
    "html-loader": "^0.5.5",
    "html-webpack-plugin": "^3.2.0",
    "style-loader": "^1.0.0",
    "webpack": "^4.40.2",
    "webpack-cli": "^3.3.9"
  },
  "dependencies": {
    "three": "^0.108.0"
  }
}

var HtmlWebpackPlugin = require("html-webpack-plugin");

module.exports = {
  entry: './src/index.js',
  output: {
    filename: "main.js"
  },
  module: {
    rules: [
      {
        // Для всех файлов HTML
        test: /\.html$/,
        use: [
          {
            // Воспользуемся загрузчиком html-loader
            loader: "html-loader",
            // Который заодно проминимизирует наш HTML
            options: { minimize: true }
          }
        ]
      },
      {
        test: /\.css$/,
        use: [
          {
            loader: "style-loader"
          },
          {
            loader: "css-loader"
          }
        ]
      }
    ]
  },
  plugins: [
    // Скопируем наш index.html в папку dist
    new HtmlWebpackPlugin({
      template: "./index.html",
      filename: "./index.html"
    })
  ]
};

<!doctype html>
<html>
  <head>
    <title>Пример</title>
  </head>
  <body>
    <!-- Создаем контейнер, в котором будет происходить отрисовка -->
    <div id="container"></div>
  </body>
</html>

body {
  background-color: #000;
  margin: 0px;
  overflow: hidden;
  color: white;
  text-align: center;
}

#container {
  position: absolute;
  width: 100%;
  height: 100%;
}

var css = require("./../style.css");
var THREE = require("three");

var container = document.querySelector('#container');

var scene = new THREE.Scene();
scene.background = new THREE.Color('skyblue');

var fov = 35; // AKA Field of View
var aspect = container.clientWidth / container.clientHeight;
var near = 0.1; // the near clipping plane
var far = 100; // the far clipping plane

var camera = new THREE.PerspectiveCamera(fov, aspect, near, far);
camera.position.set(0, 0, 10);

var geometry = new THREE.BoxBufferGeometry(2, 2, 2);
var material = new THREE.MeshBasicMaterial();
var mesh = new THREE.Mesh(geometry, material);
scene.add(mesh);

var renderer = new THREE.WebGLRenderer();

renderer.setSize(container.clientWidth, container.clientHeight);
renderer.setPixelRatio(window.devicePixelRatio);

container.appendChild(renderer.domElement);
renderer.render(scene, camera);

data Nat :: * where
  Zero :: Nat
  Succ :: Nat -> Nat
  
zero :: Nat
zero = Zero

one :: Nat
one = Succ Zero

two :: Nat
two = Succ (Succ Zero)

add :: Nat -> Nat -> Nat
add n Zero     = n
add n (Succ k) = Succ (add n k)

mul :: Nat -> Nat -> Nat
mul n Zero     = Zero
mul n (Succ k) = add m (mul n k)

pred :: Nat -> Nat
pred Zero     = Zero
pred (Succ k) = k

minus :: Nat -> Nat -> Nat
minus Zero     m        = Zero
minus n        Zero     = n
minus (Succ k) (Succ l) = minus k l

Простейший способ кодирования таких чисел при помощи нетипизированного лямбда-исчисления — метод Чёрча, не имеющий, как кажется, прямого отношения к понятному индуктивному типу:

\[
‌‌\begin{align*}
‌‌0 &= \lambda s z. z\\
‌‌1 &= \lambda s z. sz\\‌‌
2 &= \lambda s z. s(sz)\\‌‌
&\ldots\\‌‌
n &= \lambda s z. s^nz\\‌‌
\end{align*}
‌‌\]

При этом используется нотация степени, являющаяся синтаксическим сахаром для следующей записи:

\[‌‌
\begin{align*}‌‌
F^0(X) &= X\\
‌‌F^N(X) &= F^{N-1}(F(X))‌‌
\end{align*}‌‌
\]

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

\[
‌‌succ = \lambda n s z.s (n s z)‌‌
\]

Действительно, воспользовавшись таким термом, мы можем получить ожидаемое поведение:

\[
‌‌\begin{align*}‌‌
succ \; n &= (\lambda \color{red}n \color{black} s z.s (\color{red}n \color{black} s z)) \color{blue} (\lambda s z. s^n z) \color{black} = \\‌‌
&=  (\lambda s z.s (\color{green}  (\lambda \color{red} s \color{green} z. \color{red} s \color{green} ^n z) \color{blue} s \color{black} z)) = \\‌‌
&= (\lambda s z.s (\color{green}  (\lambda \color{red} z \color{green}. s^n \color{red} z \color{green}) \color{blue} z \color{black})) = \\
‌‌&= (\lambda s z.s (s^n z)) = (\lambda s z.s^{n+1} z)
‌‌\end{align*}‌‌
\]

Также нам доступны простейшие арифметические операции (их можно проверить абсолютно аналогично тому, как выше проверяется функция succ):

\[‌‌
\begin{align*}‌‌
add &= \lambda m n. m \; succ \; n\\
‌‌mul &= \lambda m n. m \; add \; n\\‌‌
pow &= \lambda m n. m \; mul \; n‌‌
\end{align*}‌‌
\]

Эти функции дают важное свойство натуральных чисел в кодировке Чёрча. Применение терма, являющегося n-ным натуральным числом к некоторым термам f и x обеспечит n-кратное применение f к x:

\[
‌‌n f x = (\lambda s z.s^n z) f x = f^n x‌‌
\]

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

data Pair :: * -> * -> * where
  MkPair :: a -> b -> Pair a b
  
fst :: Pair a b -> a
fst (Pair x y) = x

snd :: Pair a b -> b
snd (Pair x y) = y

Мы же вновь должны пользоваться лямбда-исчислением для их кодирования:

\[
pair = \lambda a b c.c a b
\]

Действительно, мы може записать любую пару элементов таким образом, ведь \( pair X Y = \lambda c. c X Y \). Более того, нам доступны две проекции, позволяющие брать первый и второй элемент пары:

\[
\begin{align*}
fst &= \lambda p. p \; K \\
snd &= \lambda p. p \; K*
\end{align*}
\]

\( K \) и \( K* \) здесь — это комбинаторы \( \lambda x y.x \) и \( \lambda x y. y \) соответственно. Действительно:

\[
\begin{align*}
fst (pair X Y) &= (\lambda p.p \; K) \; ((\lambda a b c.c a b) X Y) = \\
&= (\lambda p.p \; K) \; (\lambda c.c X Y) = (\lambda c.c X Y) K = \\
&= K X Y = (\lambda x y.x) X Y = (\lambda y.X) Y = X
\end{align*}
\]

Как же воспользоваться этой конструкцией для получения предыдущего числа? Давайте зададим пару, которая будет содержать в качестве первого аргумента некоторое число, а в качестве второго — следующее за ним. Получить её довольно просто:

\[
pair \; n \; (succ \; n)
\]

В частности, первые несколько таких пар будут (мы считаем, что предыдущее для ноля — ноль):

\[
pair \; 0 \; 0\\
pair \; 0 \; 1\\
pair \; 1 \; 2\\
\ldots
\]

А можем ли мы вместо выписывания всех пар просто придумать терм, позволяющий нам получить следующую пару из предыдущей? Да, запросто!

\[
sp = \lambda p. pair \; (snd \; p) (snd \; (succ \; p))
\]

Здесь первым элементом новой пары становится второй элемент предыдущей, а вторым — следующее число. Применив такую функцию к паре \( (pair \; 0 \; 0) \) n раз мы получим пару, где второй элемент — число n, а первое — n - 1. А ровно это нам и требуется. Собирая все вместе получим функцию получения предыдущего натурального числа:

\[
pred \; n = \lambda n.fst \; (n \; sp \; (pair \; 0 \; 0))
\]

Из тех же соображений можно получить вычитание чисел:

\[
minus = \lambda n m. m \; pred \; n
\]

Важным наблюдением тут является то, что функция pred работает за \( O(n) \), а minus и вовсе за \( O(n^2) \)! Это, очевидно, является проблемой кодировки натуральных чисел Чёрча.

Целочисленное деление также можно получить, вспомнив рекурсивное выражение через вычитание:

\[
\left[ \frac{n}{m} \right] =
\begin{cases}
1 + \left[ \frac{n - m}{m} \right] & n \ge m \\
0 & n < m
\end{cases}
\]

Для написания данного выражения нам потребуется еще один тип данных — Boolean, для того, чтоб выражать условие, в соответствии с которым мы будем возвращать 0 или идти в рекурсивную ветку. Классическое определение Boolean тривиально — это тип, который населяют два конктреных значения:

data Bool :: * where
  True  :: Bool
  False :: Bool
  
ifThenElse :: Bool -> a -> a -> a
ifThenElse True  x y = x
ifThenElse False x y = y

В нетипизированном лямбда-исчислении представление тоже не особо сложное:

\[
\begin{align*}
true &= \lambda t f.t \\
false &= \lambda t f.f
\end{align*}
\]

Оператор if для такой кодировки совсем тривиальный:

\[
if = \lambda c x y.c x y
\]

Действительно, это можно проверить:

\[
\begin{align*}
if \; true \; X \; Y &= (\lambda c x y.c x y) \; true \; X \; Y = \\
&= (\lambda x y.true \; x \; y) \; X \; Y = \\
&= (\lambda y.true \; X \; y) \; Y = true \; X \; Y = \\
&= (\lambda t f.t) \; X \; Y = (\lambda f.X) \; Y = \\
&= X\\

if \; false \; X \; Y &= (\lambda c x y.c x y) \; false \; X \; Y = \\
&= (\lambda x y.false \; x \; y) \; X \; Y = \\
&= (\lambda y.false \; X \; y) \; Y = false \; X \; Y = \\
&= (\lambda t f.f) \; X \; Y = (\lambda f.f) \; Y = \\
&= Y
\end{align*}
\]

Для получения нашей формулы требуется еще понять, как сравнивать два числа. Простейший способ — вычесть одно из другого и сравнить с нулем. Вычитать мы уже умеем, а вот сравнение с нулем — это новое смешение двух миров: натуральных чисел и булевых значений. Тем не менее делается это сравнение очень просто. Заметим, что ноль выглядит так же, как false, а число отличное от нуля применит n раз какую-то функцию к нулю. Это позволяет нам написать функцию iszero по аналогии с if:

\[
iszero = \lambda n.n \; (\lambda x.false) \; true
\]

Теперь мы можем записать рекурсивную форму нашего деления:

\[
div = \lambda n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (div \; (minus \; n \; m) \; m))
\]

Отлично! За одним исключением: мы не умеем работать с рекурсивными термами. Но это легко исправить. Для начала проабстрагируемся по упоминанию div в нашем терме:

\[
div = (\lambda \color{red} d \color{black} n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (\color{red} d \color{black} \; (minus \; n \; m) \; m))) \; \color{red} div \color{black}
\]

Теперь наш терм принял вид \( X = F \; X \), иными словами div является неподвижной точкой для терма:

\[
\lambda d n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (d \; (minus \; n \; m) \; m))
\]

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

\[
Y = \lambda f.(\lambda x.f (xx))(\lambda x.f (xx))
\]

Итого, финальное нерекурсивное выражение для деления:

\[
div = Y (\lambda d n m. if \; (iszero \; (minus \; m \; (add \; n \; 1))) \; 0 \; (add \; 1 \; (d \; (minus \; n \; m) \; m)))
\]

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

Начнем, непосредственно, с введения формального языка, который позволит нам описывать термы лямбда-исчисления. Простейшим элементом исчисления являются переменные — элементы множества \(V = {x, y, z, \ldots}\) произвольных символов латинского алфавита. Любая подобная переменная уже будет считаться термом:‌‌‌‌
\[x
\in V \Rightarrow x \in \Lambda.
\]‌‌‌‌
Также обязательным условием построения любого исчисления является то, что термом является терм в скобках:‌‌‌‌
\[
t \in \Lambda \Rightarrow (t) \in \Lambda.
\]‌‌‌‌
Теперь мы можем строить уже бесконечное множество термов:‌‌‌‌
\[
x, y, (x), ((x)), (((z))), \ldots
\]
Однако это явно не то, что мы хотим в итоге, ведь наше исчисление должно иметь способность выражать любое вычисление. А значит, требуется добавить в него еще видов формул. Понятная и естественная конструкция — это применение. Терм, представляющий из себя функцию, применяется к некоторому терму (представляющий аргумент), в результате чего получается новый терм. В лямбда-исчислении это можно выразить следующим образом:‌‌‌
\[
m, n \in \Lambda \Rightarrow (m \, n) \in \Lambda,
\]‌‌‌‌
что позволяет нам писать еще больше бессмысленных конструкций:‌‌‌‌
\[
(x \, y), ((x \, y) z), ((x \,y) z) (m n), \ldots
\]

Последняя, но очень важная конструкция — абстрация терма по переменной, позволяющая показать зависимость некоторой функции от своего аргумента. По историческим причинам она пишется через букву \( \lambda \), что и дало название исчислению:‌‌‌‌
\[
x \in V, m \in \Lambda \Rightarrow \lambda x. m \in \Lambda.
\]

Если допустить, что у нас есть некоторые именованные термы (e.g. plus, prod и pow), представляющие те или иные операторы (+, *, ^), мы можем написать произвольную арифметическую функцию:‌‌‌‌
\[
f(x,y) = x^2 + 3 \cdot y \rightarrow \lambda x.\lambda y.((plus ((pow \, x) 2)) ((prod \, 3) y))
\]
Из-за обилия скобочек выражение выглядит совершенно нечитаемым, так что для начала добавим несколько соглашений, которые позволят упростить запись. В первую очередь, это правила ассоциативности. Применение мы будем считать ассоциативным влево, а абстракцию вправо:‌‌‌‌
\[
‌‌‌‌(m n) (k) = m \, n \, k \\
‌‌‌‌\lambda x. \lambda y. m = \lambda x \, y. m‌‌‌‌
\]
Теперь переписать ту же конструкцию можно короче и совсем понятно:‌‌‌‌
\[
f(x,y) = x^2 + 3 \cdot y \rightarrow \lambda x \, y. plus \, (pow \, x \, 2) (prod \, 3 \, y)
\]
Чтоб еще сильнее забыть про скобки, начнем думать про наши термы не как про строки, а как про синтаксические деревья. Правила переходов в деревья будут следующие:

Наша функция \( f \) теперь может быть представлена в виде синтаксического дерева:

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

import Data.Text (Text)

data Term = Var Text       -- переменные
          | App Term Term  -- аппликация
          | Lam Text Term  -- абстракция
  deriving (Show)

Чтоб сконструировать интересующий нас терм \( f \) нам также потребуется поддержка числовых литералов (числа 2 и 3). Их можно добавить в наше исчисление (добавив еще один конструктор, например, Lit Int) или сэмулировать через переменные two и tree:

{-# LANGUAGE OverloadedStrings #-}

f :: Term
f = Lam "x" (Lam "y" (App (App (Var "plus") xSqr) p3y))
  where xSqr = App (App (Var "pow") (Var "x")) (Var "two")
        p3y  = App (App (Var "prod") (Var "tree")) (Var "y")

Полученное выражение вновь изобилует скобками и вообще трудно перевариваемо:

Вывод термов

Чтоб как-то жить с этим, лучше сразу написать некоторый pretty printer, который будет выводить наши термы красиво. Начнем с простой реализации, печатающей все скобки:

import Data.Monoid ((<>))

pretty :: Term -> Text
pretty (Var name)     = name
pretty (App algo arg) = "(" <> pretty algo <> " " <> pretty arg <> ")"
pretty (Lam var body) = "λ" <> var <> "." <> pretty body

Читать подобный вывод уже можно, но все же лишние скобки явно затрудняют понимание:

ghci> import Data.Text.IO as TIO
ghci> TIO.putStrLn (pretty f)
λx.λy.((plus ((pow x) two)) ((prod tree) y)) 

Скобки требуется убирать вокруг аппликации в трех случаях: если она верхнеуровневая, если она является алгоритмом (algo) другой аппликации или если она является телом (body) абстракции. Модифицируем соответствующим образом нашу функцию:

data Parens = ParensLess | ParensFull

pretty :: Term -> Text
pretty = pretty' ParensLess
  where
    pretty' :: Parens -> Term -> Text
    pretty' _          (Var name)     = name
    pretty' ParensLess (App algo arg) = pretty' ParensLess algo <> " " <> pretty' ParensFull arg
    pretty' ParensFull app@(App _ _)  = "(" <> pretty' ParensLess app <> ")"
    pretty' _          (Lam var body) = "λ" <> var <> "." <> pretty' ParensLess body

Теперь мы получаем красивый и наглядный вывод:

ghci> import Data.Text.IO as TIO
ghci> TIO.putStrLn (pretty f)
λx.λy.plus (pow x two) (prod tree y)

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

data Position = AppAlgo | AppArg | LamBody | Other

pretty :: Term -> Text
pretty = pretty' Other
  where
    prettyLB :: Term -> Text
    prettyLB (Lam var body) = var <> pretty' LamBody body
    prettyLB _              = undefined
    
    pretty' :: Position -> Term -> Text
    pretty' LamBody lam@(Lam _ _)  = " " <> prettyLB lam
    pretty' AppAlgo lam@(Lam _ _)  = "(" <> pretty' Other lam <> ")"
    pretty' _       lam@(Lam _ _)  = "λ" <> prettyLB lam
    pretty' LamBody term           = "." <> pretty' Other term
    pretty' _       (Var name)     = name
    pretty' AppArg  app@(App _ _)  = "(" <> pretty' Other app <> ")"
    pretty' _       (App algo arg) = pretty' AppAlgo algo <> " " <> pretty' AppArg arg 

И финальный вывод:

ghci> import Data.Text.IO as TIO
ghci> TIO.putStrLn (pretty f)
λx y.plus (pow x two) (prod tree y)

Ввод термов

Помимо красивого вывода нам потребуется как-то забивать термы в наш калькулятор, поскольку набирать что-то вроде Lam "x" (Lam "y" (App (... совсем не весело. Для этого нам потребуется реализовать парсер для лямбда-термов. В идеале мы должны получить функцию, способную распарсить любой наш сжатый вывод функции pretty, то есть обеспечивающую следующее правило:
‌‌\[
parse \circ pretty = id
\]

Конечно, на самом деле мы должны обрабатывать ошибки синтаксиса и все такое, а потому наша функция parse будет несколько сложнее. Сама стратегия парсинга будет следующая: любой терм мы будем рассматривать как потенциальную аппликацию, т.е. несколько термов идущих друг за другом. Потенциальной она является в том смысле, что терм может оказаться всего один, и тогда никакой аппликации он не будет. Такой терм, не являющийся аппликацией, мы будем называть натуральным термом:
‌‌\[‌‌
\begin{align*}‌‌
term &::= {natural \, term}^n \\‌‌
natural \, term &::= (term) | variable | abstraction‌‌
\end{align*}‌‌
\]‌‌
Начнем нашу имплементацию с подключения необходимых модулей парсинга (здесь использован мой любимый attoparsec, для классического parsec или модного, но медленного megaparsec все аналогично), а также написания нескольких вспомогательных функций.

import           Control.Applicative ((<$>), (<*>), (<|>))
import           Control.Monad       (void)
import           Data.Text           (Text, pack)
import           Data.Attoparsec.Text

-- Один или несколько пробелов подряд
spaces :: Parser ()
spaces = void $ many' space

-- Парсит выражение, со всеми пробелами после него, пробелы опускает.
spaced :: Parser a -> Parser a
spaced x = x <* spaces

-- Парсит одну точку и опускает вывод парсера.
dot :: Parser ()
dot = void $ spaced (char '.')

-- Парсит символ лямбды или \\ или L и опускает вывод парсера.
lambda :: Parser ()
lambda = void $ spaced (char '\\' <|> char 'λ' <|> char 'L')

-- Парсит выражение окруженное скобками; перед открывающей и
-- после закрываающей скобок могут идти пробелы, которые будут съедены.
parens :: Parser a -> Parser a
parens x = spaced (char '(') *> x <* spaced (char ')')

-- Парсит строку, начинающуюся с символов латинского алфавита и
-- содержащую латинские символы, цифры и символ '.
name :: Parser Text
name = (pack .) . (:) <$> oneOf ['a'..'z'] <*> many' (letter <|> digit <|> char '\'')
  where
    oneOf = choice . (char <$>)

Теперь можно реализовать функции, которые будут прочитывать терм и натуральный терм в формулировках, данных выше:

-- Прочитывает не менее одного натурального терма; в случае
-- если их больше одной, соединяет их в один с помощью аппликации
-- по правилам левой ассоциативности.
term :: Parser Term
term = foldl1 App <$> many1 (spaced naturalTerm)

-- Прочитывает терм, возможно содержащий аппликацию, в скобках,
-- либо переменную, либо лямбда-абстракцию.
naturalTerm :: Parser Term
naturalTerm = parens term <|> variable <|> abstraction 

Осталось написать всего два парсера: для переменных и абстракции. Их вид столь же тривиален, что и у парсеров выше:

-- Парсит одну переменную.
variable :: Parser Term
variable = Var <$> name

-- Парсит лямбда-абстракцию, как символ лямбды, не менее 1 переменной,
-- точку и терм, являющийся телом абстракции; сворачивает переменные
-- во вложенные лямбда-абстракции по правилу правой ассоциативности.
abstraction :: Parser Term
abstraction = do lambda
                 vars <- many1 (spaced name)
                 dot
                 expr <- term
                 pure $ foldr Lam expr vars

Протестировать наши парсеры можно с помощью такой функции:

parseTerm :: Text -> Either String Term
parseTerm = parseOnly term

В интерпретаторе проверим, что все читается верно:

ghci> :set -XOverloadedStrings
ghci> Right t = parseTerm "λx y.plus (pow x two) (prod tree y)"
ghci> t
Lam "x" (Lam "y" (App (App (Var "plus") (App (App (Var "pow") (Var "x")) (Var "two"))) (App (App (Var "prod") (Var "tree")) (Var "y"))))
ghci> pretty t
λx y.plus (pow x two) (prod tree y)

Наполнение смыслом

Теперь пришло время наполнить наше исчисление смыслом. Для этого требуется ввести несколько правилм переписывания одних термов в другие, которые мы и будем считать вычислениями.

Прежде чем начать, введем пару определений. В зависимости от присутствия или отсутствия переменной под символом лямбды в абстракции мы будем делить все переменные на свободные и связанные. Начнем с интутитивного примера:‌‌
\[‌‌
(\lambda \color{red}x \color{black}. (\lambda \color{green}x \color{black}. \color{green}x \color{black} \, y) \, \color{red}x \color{black}) \, \color{blue}x‌‌
\]‌‌
Иксы разного цвета как бы "связываются" разными лямбдами. Проследить интуитивно это можно следующим образом, снимая некоторую лямбду можно "освободить" ту или иную переменную, поскольку её имя больше не будет означать, что она является аргументом какой-либо функции. После столь водянистого пояснения дадим нормальное определение:‌‌Для произвольного терма \( t \) множеством его свободных переменных \( FV(t) \) называют множество, сконструированное по следующим правилам (далее подразумевается, что \( x \in V, \, M, N \in \Lambda \)):‌‌
\[
‌‌\begin{align*}‌‌
FV(x) &= \{x\} \\‌‌
FV(M \, N) &= FV(M) \cup FV(N) \\‌‌
FV(\lambda x. M) &= FM(M) \backslash \{x\}‌‌
\end{align*}‌‌
\]
‌‌Аналогично задается множество \( BV(t) \) связанных переменных:‌‌
\[‌‌
\begin{align*}‌‌
BV(x) &= \varnothing \\‌‌
BV(M \, N) &= FV(M) \cup FV(N) \\
‌‌BV(\lambda x. M) &= BV(M) \cup \{x\}‌‌
\end{align*}‌‌
\]
‌‌Соответствующие функции на Haskell будут в точности повторять определение:

import Data.Set (Set, delete, empty,
                 insert, singleton, union)
                 
free :: Term -> Set Name
free (Var var)      = singleton var
free (App algo arg) = free algo `union` free arg
free (Lam var body) = var `delete` free body

bound :: Term -> Set Name
bound (Var var)      = empty
bound (App algo arg) = bound algo `union` bound arg
bound (Lam var body) = var `insert` free body

В лямбда-исчислении существует единственная нетривиальная аксиома — два терма являются равными, если они равны с точностью до переименования связанных переменных. Таким образом, следующие термы равны:
‌‌\[‌‌
\lambda \color{red}x \color{black} \, \color{green}y \color{black} . \color{red} x \color{black} = \lambda \color{red}z \color{black} \, \color{green}w \color{black} . \color{red} z \color{black} = \lambda \color{red}y \color{black} \, \color{green}x \color{black} . \color{red} y \color{black}
‌‌\]‌‌
Реализуем это, сделав наши термы представителем классов типов Eq следующим образом:

instance Eq Term where
  Var a == Var b        = a == b
  App a b == App a' b'  = a == a' && b == b'
  Lam v b == Lam v' b'  = b == substitute b' v' (Var v)
  _ == _                = False

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

Подстановкой \( M[x:=N] \) терма \( N \) вместо всех свободных вхождений переменной \( x \) в терм \( M \) называют терм, образованный по следующим правилам (как обычно, \( x \in V, \, M, N, P, Q \in \Lambda \)):
‌‌\[
‌‌\begin{align*}‌‌
x[x:=N] &= N \\‌‌
y[x:=N] &= y \\‌‌
(P \, Q)[x:=N] &= (P[x:=N]) \, (Q[x:=N]) \\‌‌
(\lambda x. M)[x:=N] &= \lambda x. M \\‌‌
(\lambda y. M)[x:=N] &= \lambda y. (M[x:=N]), \text{ если } x \not\in FV(N)‌
\end{align*}‌‌
\]
‌‌В последнем пункте есть дополнительное условие. Если его не соблюдать, то некоторые подставновки будут приводить к неприятным последствиям, а именно изменению структуры терма, называемой захватом переменной:‌‌
\[‌‌
(\lambda x.y)[y:=x] = \lambda x.x \, \color{red}\text{(это неправда!)}‌‌
\]

Для решения проблемы захвата существует несколько решений:

1. Использовать для связанных и свободных переменных символы из различного алфавита (соглашение Баррендрегта). Идея богатая, но мало реализуемая на практике.
   \[
   (\lambda \color{red}x' \color{black}. (\lambda \color{green}y' \color{black}. \color{green}y' \color{black} \, \color{red}x' \color{black}) \, \color{red}x' \color{black}) \, \color{blue}x‌‌
   \]
2. Убрать все имена связанных переменных, заменив их номерами, показывающими, сколько лямбд назад они были связаны. Такой способ называется индексами (нотацией) де Брауна и используется в большинстве языков программирования благодаря своей вычислительной эффективности.
   \[
   (\lambda (\lambda \color{green}1\color{black} \, \color{red}2\color{black}) \, \color{red}1 \color{black}) \, \color{blue}x‌‌
   \]
3. Мы же пойдем третим путем: каждый раз, встречая конфликт при подстановке, мы будем осуществлять переименование связанных переменных в некоторые еще не использованные имена. Это не так эффективно, зато очень похоже на то, что делает человек, оперируя вручную с лямбда-исчислением.

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

import Data.Text (Text, pack)
import Data.Set  (Set, member)

-- Генерируем бесконечный список предлагаемых имен и берем первое,
-- которое пока не встретилось в списке.
fresh :: Set Text -> Text
fresh conflicts = head . dropWhile (`member` conflicts) $ names
  where
    -- Простые имена — это просто малые буквы латинского алфавита
    primitiveNames = map (:[]) letters
    -- Составные имена состоят из буквы и цифры
    complexNames = [(l:n) | n <- numbers, l <- letters]
    -- Полный список имен
    names = map pack $ primitiveNames ++ complexNames
    -- Используемые буквы и числа
    letters = ['a' .. 'z']
    numbers = map show [1..]

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

alpha :: Set Text -> Term -> Term
alpha conflicts var@(Var _)    = var
alpha conflicts (App algo arg) = App (alpha conflicts algo) (alpha conflicts arg)
alpha conflicts (Lam var body) = if hasConflict then renamed_lam else alpha_lam
  where  
    hasConflict = var `member` conflicts
    alpha_lam   = Lam var (alpha conflicts body)
    renamed_lam = Lam new_var new_body
    new_var     = fresh $ conflicts `union` free body
    new_body    = substitute body var (Var new_var)

Для написания этой функции нам вновь пришлось прибегнуть к функции substitute, поскольку при смене переменной под лямбдой нам потребуется заменить все её упоминание в теле абстрации. Теперь у нас есть все, чтоб реализовать эту волшебную функцию:

substitute :: Term -> Text -> Term -> Term
substitute var@(Var var')     name expr = if var' == name then expr else var
substitute     (App algo arg) name expr = App (substitute algo name expr) (substitute arg name expr)
substitute lam@(Lam var body) name expr = if var == name then lam else new_lam
  where
    alpha_lam = alpha (free expr) lam
    new_body  = substitute body name expr
    new_lam   = if var `member` free expr then substitute alpha_lam name expr
                                          else Lam var new_body

Редукция

В лямбда-вычислении мы допускаем два вида редукции — одностороннего преобразования или "упрощения", которое и будет представлять вычисление. Первый такой вид редукции тривиален и называется \(\eta\)-преобразованием:
\[
\lambda x. M \, x = M
\]
Оно выводится из тривиальных соображений, о чем можно почитать у того же Баррендрегта. Реализуется оно практически столь же просто:

eta :: Term -> Term
eta (Lam var body) = case body of
                       App algo (Var v)
                         | var == v && v `notMember` free algo = algo
                       _                                       = Lam var (eta body)
eta (App algo arg) = App (eta algo) (eta arg)
eta var            = var

Главное же преобразование — это единственное правило вывода в лямбда-исчислении — \(\beta\)-преобразование:
\[
(\lambda x.M) \, N = M[x:=N]
\]
То есть любое применение лямбда-абстракции к какому-либо терму выполняется путем замены переменной абстракции (аргумента) на конкретное значение. На базе такого преобразования возможно написать правила одношаговой \(\beta\)-редукции \( M \rightarrow_{\beta} N\). Она проводится следующим образом:

1. \( (\lambda x.M) \, N = M[x:=N] \), то есть простым \(\beta\)-преобразованием;
2. \( M \rightarrow_{\beta} N \Rightarrow M \, Z \Rightarrow N \, Z \), то есть редукция в первом терме (алгоритме) применения.
3. \( M \rightarrow_{\beta} N \Rightarrow Z \, M \Rightarrow Z \, N \), то есть редукция во втором терме (аргументе) применения.
4. \( M \rightarrow_{\beta} N \Rightarrow \lambda x. M \Rightarrow \lambda x. N \), то есть редукция в теле абстракции.

Релизуем это следующим образом:

beta :: Term -> Term
beta var@(Var _)        = var
beta     (Lam var body) = Lam var (beta body)
beta     (App algo arg) = case algo of
                            Lam var body -> substitute body var arg
                            _            -> if algo /= algo' then App algo' arg
                                                             else App algo arg'
  where
    algo' = beta algo
    arg'  = beta arg

На этом все! У нас получился полный лямбда-калькулятор с парсером, красивым выводом и разными видами редукции. Превращать любой терм в нормальную форму, при её наличии, можно подобной простой функцией:

reduce :: Term -> Term
reduce term | beta term == term = eta term
            | otherwise         = reduce (beta term)

Ну, а попрактиковаться в применении лямбда-исчисления можно, например, на кодировании натуральных и целых чисел, как это описано в Википедии.

Я же напоследок приведу полный листинг получившегося:

module UntypedLambda where

import           Control.Applicative  ((<$>), (<*>), (<|>))
import           Control.Monad        (void)
import           Data.Text            (Text, pack)
import           Data.Attoparsec.Text
import           Data.Set             (Set, delete, empty,
                                       insert, singleton, union,
                                       member, notMember)

data Term = Var Text       -- переменные
          | App Term Term  -- аппликация
          | Lam Text Term  -- абстракция
    deriving (Show)

-- Pretty Print

data Position = AppAlgo | AppArg | LamBody | Other

pretty :: Term -> Text
pretty = pretty' Other
    where
    prettyLB :: Term -> Text
    prettyLB (Lam var body) = var <> pretty' LamBody body
    prettyLB _              = undefined
    
    pretty' :: Position -> Term -> Text
    pretty' LamBody lam@(Lam _ _)  = " " <> prettyLB lam
    pretty' AppAlgo lam@(Lam _ _)  = "(" <> pretty' Other lam <> ")"
    pretty' _       lam@(Lam _ _)  = "λ" <> prettyLB lam
    pretty' LamBody term           = "." <> pretty' Other term
    pretty' _       (Var name)     = name
    pretty' AppArg  app@(App _ _)  = "(" <> pretty' Other app <> ")"
    pretty' _       (App algo arg) = pretty' AppAlgo algo <> " " <> pretty' AppArg arg 

-- Parsing

spaces :: Parser ()
spaces = void $ many' space

-- Парсит выражение, со всеми пробелами после него, пробелы опускает.
spaced :: Parser a -> Parser a
spaced x = x <* spaces

-- Парсит одну точку и опускает вывод парсера.
dot :: Parser ()
dot = void $ spaced (char '.')

-- Парсит символ лямбды или \\ или L и опускает вывод парсера.
lambda :: Parser ()
lambda = void $ spaced (char '\\' <|> char 'λ' <|> char 'L')

-- Парсит выражение окруженное скобками; перед открывающей и
-- после закрываающей скобок могут идти пробелы, которые будут съедены.
parens :: Parser a -> Parser a
parens x = spaced (char '(') *> x <* spaced (char ')')

-- Парсит строку, начинающуюся с символов латинского алфавита и
-- содержащую латинские символы, цифры и символ '.
name :: Parser Text
name = (pack .) . (:) <$> oneOf ['a'..'z'] <*> many' (letter <|> digit <|> char '\'')
  where
    oneOf = choice . (char <$>)

-- Прочитывает не менее одного натурального терма; в случае
-- если их больше одной, соединяет их в один с помощью аппликации
-- по правилам левой ассоциативности.
term :: Parser Term
term = foldl1 App <$> many1 (spaced naturalTerm)

-- Прочитывает терм, возможно содержащий аппликацию, в скобках,
-- либо переменную, либо лямбда-абстракцию.
naturalTerm :: Parser Term
naturalTerm = parens term <|> variable <|> abstraction 

-- Парсит одну переменную.
variable :: Parser Term
variable = Var <$> name

-- Парсит лямбда-абстракцию, как символ лямбды, не менее 1 переменной,
-- точку и терм, являющийся телом абстракции; сворачивает переменные
-- во вложенные лямбда-абстракции по правилу правой ассоциативности.
abstraction :: Parser Term
abstraction = do lambda
                 vars <- many1 (spaced name)
                 dot
                 expr <- term
                 pure $ foldr Lam expr vars

parseTerm :: Text -> Either String Term
parseTerm = parseOnly term

-- Logic

free :: Term -> Set Text
free (Var var)      = singleton var
free (App algo arg) = free algo `union` free arg
free (Lam var body) = var `delete` free body

bound :: Term -> Set Text
bound (Var var)      = empty
bound (App algo arg) = bound algo `union` bound arg
bound (Lam var body) = var `insert` free body

instance Eq Term where
    Var a == Var b       = a == b
    App a b == App a' b' = a == a' && b == b'
    Lam v b == Lam v' b' = b == substitute b' v' (Var v)
    _ == _               = False

-- Генерируем бесконечный список предлагаемых имен и берем первое,
-- которое пока не встретилось в списке.
fresh :: Set Text -> Text
fresh conflicts = head . dropWhile (`member` conflicts) $ names
  where
    -- Простые имена — это просто малые буквы латинского алфавита
    primitiveNames = map (:[]) letters
    -- Составные имена состоят из буквы и цифры
    complexNames = [(l:n) | n <- numbers, l <- letters]
    -- Полный список имен
    names = map pack $ primitiveNames ++ complexNames
    -- Используемые буквы и числа
    letters = ['a' .. 'z']
    numbers = map show [1..]

alpha :: Set Text -> Term -> Term
alpha conflicts var@(Var _)    = var
alpha conflicts (App algo arg) = App (alpha conflicts algo) (alpha conflicts arg)
alpha conflicts (Lam var body) = if hasConflict then renamed_lam else alpha_lam
  where  
    hasConflict = var `member` conflicts
    alpha_lam   = Lam var (alpha conflicts body)
    renamed_lam = Lam new_var new_body
    new_var     = fresh $ conflicts `union` free body
    new_body    = substitute body var (Var new_var)

substitute :: Term -> Text -> Term -> Term
substitute var@(Var var')     name expr = if var' == name then expr else var
substitute     (App algo arg) name expr = App (substitute algo name expr) (substitute arg name expr)
substitute lam@(Lam var body) name expr = if var == name then lam else new_lam
  where
    alpha_lam = alpha (free expr) lam
    new_body  = substitute body name expr
    new_lam   = if var `member` free expr then substitute alpha_lam name expr
                                            else Lam var new_body

-- Evaluation

eta :: Term -> Term
eta (Lam var body) = case body of
                       App algo (Var v)
                         | var == v && (v `notMember` free algo) -> algo
                       _                                         -> Lam var (eta body)
eta (App algo arg) = App (eta algo) (eta arg)
eta var            = var

beta :: Term -> Term
beta var@(Var _)        = var
beta     (Lam var body) = Lam var (beta body)
beta     (App algo arg) = case algo of
                            Lam var body -> substitute body var arg
                            _            -> if algo /= algo' then App algo' arg
                                                             else App algo arg'
  where
    algo' = beta algo
    arg'  = beta arg

reduce :: Term -> Term
reduce term | beta term == term = eta term
            | otherwise         = reduce (beta term)

С 30 апреля по 4 мая проходила моя любимая ежегодная конференция PEGS Boston. На протяжении 14 лет в дизайне логотипа и всех сопутствующих материалов этой конференции используется изображение одного и того же белка, и вот уже 13 лет подряд организаторы конференции задают вопрос: что это за белок? В этом году команда ДВБ впервые ответила на этот вопрос. И теперь главный вопрос: как?

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

show_as cartoon, all
set cartoon_fancy_helices, 0
set cartoon_cylindrical_helices, 1

Также белок покрашен в режиме спектра, распределенного по длине последовательности. Самая первая аминокислота покрашена в фиолетовый, а последняя в красный. Делается это еще одной простой командой:

spectrum count, rainbow

Теперь мы можем превратить стандартное полноатомное представление

в симпатичный вид а-ля PEGS

Наша первая идея состояла в том, что можно нагенерировать изображений из Protein DataBank и сравнить их с нашим изображением, например, 2D-Хэммингом. Впоследствии мы отказались от этой идеи (а зря!), но скрипт генерации у нас появился:

from pymol import cmd
import os

DIR = '/path/to/locate/pdbs'
IMG = '/path/to/store/images'

if not os.path.exists(IMG):
    os.mkdir(IMG)

for ent in os.listdir(DIR):
    filename = os.path.join(IMG, "%s.png" % ent)
    if os.path.exists(filename):
        continue
    cmd.load(os.path.join(DIR, ent))
    cmd.show_as('cartoon', 'all')
    cmd.set('cartoon_fancy_helices', 0)
    cmd.set('cartoon_cylindrical_helices', 1)
    cmd.spectrum('count', 'rainbow')
    cmd.orient()
    cmd.save(filename)
    cmd.reinitialize()

Запуск через консольный режим PyMOL делается тоже просто:

pymol -qc make_images.py

Отказались мы от этой идеи по причине того, что актуальный PDB имеет уж слишком много записей. На момент написания этого поста статистика следующая:

В этом нам очень помогло, что Саша Надолинский узнал автора изображения и нашел на его сайте картинку высокого разрешения. Из нее мы пришли к выводу, что искать требуется белок с одной цепью, в состав которого входит не менее 30 альфа-спиралей, не менее 17 из которых имею длину 5 и менее аминокислот. Также мы обратили внимание, что в начале цепи идет альфа-спираль, так что мы решили добавить это знание в наши фильтры. Единственное, мы не были уверены, что раскраска цепи каноническая от синего к красному, поскольку помимо классического режима rainbow существует также rainbow_rev, в котором все ровно наоборот. С другой стороны белка также присутствовала спираль, но не с самого начала. В связи с этим мы решили перестраховаться и сказать, что 3 позиция должна покрываться спиралью.
Разумеется, главным критерием отсева была дата: первый PEGS проводился в 2005 году, а значит белок должен был быть кристаллизован ранее. Если посмотреть на график роста размера Protein DataBank, видно, что это действительно мощнейший фильтр из всех.

Итак, поехали. Предварительно нужно скачать весь Protein DataBank (у нас он был уже скачан ранее). Как это сделать, подробно можно прочитать здесь, там же дан удобный скрипт для скачивания всего добра через rsync. Мы же возьмем из него одну строчку, которая скачает нам только структуры по папочкам:

$> rsync -rlpt -v -z --delete --port=33444 rsync.wwpdb.org::ftp/data/structures/divided/pdb/ /path/to/your/local/dir > /tmp/pdb-download.log 2> /dev/null

Таким образом мы получаем все 130+ тысяч структур из RCSB PDB. Кажется, что это огромные данные, но мы будем работать с ними лишь примитивными инструментами командной строки, чтоб показать обратное. В первую очередь отберем все белки до 2005 года.

$> for filename in $(ls pdbs/*/*); do awk '$1 == "HEADER" {split($(NF-1),a,"-"); if (a[3] < 5 || a[3] > 18) {print FILENAME}}' $filename; done > pdbs_prior_2005.txt

На самом деле тот же код можно значительно ускорить, используя grep или ag для начальной фильтрации:

$> ag '^HEADER' pdbs | awk '{split($0,a,":"); split($(NF-1),b,"-"); if (b[3] < 5 || b[3] > 18) {print a[1]}}' > pdbs_prior_2005.txt

На маленьком множестве в 1000 файлов разница вот такая:

$> time (for filename in $(ls pdbs/*/*); do awk '$1 == "HEADER" {split($(NF-1),a,"-"); if (a[3] < 5 || a[3] > 18) {print FILENAME}}' $filename; done > /dev/null)
3,45s user 1,84s system 98% cpu 56,206 total

$> time (grep -e '^HEADER' pdbs/* | awk '{split($0,a,":"); split($(NF-1),b,"-"); if (b[3] < 5 || b[3] > 18) {print a[1]}}' > /dev/null)
7,34s user 0,19s system 100% cpu 7,530 total

$> time (ag '^HEADER' pdbs | awk '{split($0,a,":"); split($(NF-1),b,"-"); if (b[3] < 5 || b[3] > 18) {print a[1]}}' > /dev/null)
0,70s user 0,30s system 278% cpu 0,358 total

Очевидно, на выборке в 130+ тысяч стоит использовать ag 😉. Так или иначе, теперь у нас есть файл pdbs_prior_2005.txt, содержащий пути до всех файлов, чья дата загрузки в Protein DataBank раньше, чем 2005 год. Как и показано на графике выше, таких структур —

Теперь начнем отбирать по количеству альфа-спиралей. В первую очередь возьмем все белки с 30 и более спиралями. На этот раз сразу сделаем это эффективно:

$> cat pdbs_prior_2005.txt | xargs ag "^HELIX   30" | awk '{split($0,a,":"); print a[1]}' > pdbs_p2005_h30.txt

Следующая задача: найти 17 спиралей длиной не более 5 аминокислот. И вновь awk спасет нас, теперь благодаря возможности выполнения арифметических операций:

$> for filename in $(cat pdbs_p2005_h30.txt);do ag "^HELIX" $filename | awk 'BEGIN{i=0}{ if ($9-$6 < 6) {i++} }END{ if (i > 16) { print "'$filename'" } }'; done > pdbs_ph_h17.txt

Что же у нас получилось к текущему моменту?

$> wc -l pdbs_ph_h17.txt
2537 pdbs_ph_h17.txt

Размер файла уже достаточно разумный, всего 2537 записей, однако это всё еще слишком много, чтоб отсматривать глазами. Добавим правило про третью аминокислоту в альфа-спирали:

$> cat pdbs_ph_h17.txt | xargs ag "^HELIX    1" | awk '($6 < 3) { split($1,a,":"); print a[1] }' > pdbs_phh_aa3.txt
$> wc -l pdbs_phh_aa3.txt
142 pdbs_phh_aa3.txt

Теперь у нас есть всего 142 структуры!
Просмотрев их все глазами, мы смогли идентифицировать нужную — 1G72 (она была 117 в списке). Как оказалось, её изображение на сайте RCSB находится ровно в той же ориентации, что и на логотипе, а значит исходная идея с Хэммингом отлично бы сработала. Но это была замечательная возможность попрактиковаться в работе с инструментами командной строки над "большими" данными.

Выступил на зимней школе Future Biotech про методы работы с малыми молекулами. Так как велась прямая трансляция, можно сразу выложить видео.

Слайды можно посмотреть и скачать на F1000.

(Перенос поста со старого сайта от 22 июня 2016 года)

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

module Bayes where
 
import Data.Map.Strict (Map(..), (!), elems)
 
newtype Classifier c s = Classifier { getClass :: Map c [s] }
 
count :: Eq a => a -> [a] -> Int
count y = foldl (\acc x -> if y == x then acc + 1 else acc) 0
 
classSize :: Ord c => Classifier c s -> c -> Int
classSize cl = length . (getClass cl !)
 
totalSize :: Classifier c s -> Int
totalSize = length . concat . elems . getClass
 
sampleCount :: Eq s => Classifier c s -> s -> Int
sampleCount cl s = count s . concat . elems . getClass $ cl
 
sampleCountInClass :: (Ord c, Eq s) => Classifier c s -> s -> c -> Int
sampleCountInClass cl s = count s . (getClass cl !)
 
-- P(C)
prior :: Ord c => Classifier c s -> c -> Double
prior cl c = if tot == 0 then 0 else tr / fromIntegral tot
  where tr = fromIntegral $ classSize cl c
        tot = totalSize cl
 
-- P(D|C)
likelihood :: (Ord c, Eq s) => Classifier c s -> s -> c -> Double
likelihood cl s c = if tr == 0 then 0 else ss / fromIntegral tr
  where ss = fromIntegral $ sampleCountInClass cl s c
        tr = classSize cl c
 
-- P (D)
evidance :: Eq s => Classifier c s -> s -> Double
evidance cl s = if tot == 0 then 0 else sam / fromIntegral tot
  where sam = fromIntegral $ sampleCount cl s
        tot = totalSize cl
 
-- P(C|D) = P(D|C) * P(C) / P(D)
posterior :: (Ord c, Eq s) => Classifier c s -> c -> s -> Double
posterior cl c s = l * p / e
  where p = prior cl c
        l = likelihood cl s c
        e = evidance cl s
 
-- ln $ P(C|D) / P(not-C|D)
logLike :: (Ord c, Eq s) => Classifier c s -> c -> s -> Double
logLike cl c s = log $ p / (1 - p)
  where p = posterior cl c s

(Перенос поста со старого сайта от 21 мая 2016 года)

По мотивам Haskell Foldable Wats в Haskell Mailing Lists.

Знаете ли вы, что произойдет, если поинтересоваться у Haskell минимальным значением кортежа из двух элементов?

Prelude> minimum (1,2)
2

Не очень интуитивно, правда? Давайте разбираться почему так происходит.

Для начала поймем, как этот самый minimum устроен. Вопрос к Hoogle дает следующий результат:

minimum :: Ord a => [a] -> a

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

Prelude> :t minimum
minimum :: (Ord a, Foldable t) => t a -> a

В исходниках Data.Foldable мы, наконец, находим виновника нашего беспокойства:

-- | The least element of a non-empty structure.
minimum :: (Foldable t, Ord a) => t a -> a
minimum = foldr1 min

Правая свертка с функцией min на каждом шаге будет брать элемент в аккумуляторе и элемент из структуры (в нашем случае — кортежа), сравнивать их и оставлять в аккумуляторе минимальный. Чтобы функция была полиморфна, начальное значение аккумулятора не задается, а берется просто первое из структуры. Эту логику обеспечивает foldr1 — вариант правой свертки над непустым Foldable типом:

-- | A variant of 'foldr' that has no base case,
-- and thus may only be applied to non-empty structures.
--
-- @'foldr1' f = 'Prelude.foldr1' f . 'toList'@
foldr1 :: (a -> a -> a) -> t a -> a
foldr1 f xs = fromMaybe (error "foldr1: empty structure")
                (foldr mf Nothing xs)
  where
    mf x m = Just (case m of
                     Nothing -> x
                     Just y  -> f x y)

Если сворачиваемая структура пуста, foldr вернет Nothing, который, не пройдя барьер fromMaybe, вызовет ошибку. В ином случае, если структура непуста, на первом шаге свертки функция mf упакует в Just первое значение в структуре, а далее свертка пойдет как обычно. Если считать, что элементы структуры кортежа — это первое и второе значение кортежа, то все должно отработать как нужно, и минимальным элементом (1,2) должна быть единица.

Осталось вспомнить вид foldr для кортежа — проблема может крыться только в нем. Так и есть:

instance Foldable ((,) a) where
    foldMap f (_, y) = f y
 
    foldr f z (_, y) = f y z

Итак, правая свертка на кортежах из двух элементов игнорирует первый элемент кортежа и выполняет переданную функцию f на втором элементе кортежа и начальном значении. То есть кортеж из двух элементов — это контейнер, который хранит только свой второй элемент. Это логичное поведение, поскольку у нас нет никаких гарантий относительно согласованности типов первого и второго элемента. Но, как итог, правая свертка без начального значения и вовсе не будет обращаться к функции, а просто вернет второй элемент кортежа!

Prelude> foldr1 min (1,2)
2
Prelude> foldr1 (*) (1,2)
2
Prelude> foldr1 (+) (1,2)
2

Благодаря ленивой семантике работать будет даже:

Prelude> foldr1 (+) (undefined,2)
2
Prelude> foldr1 undefined (undefined,2)
2

Точно так же и все библиотечные функции, использующие правую свертку, будут давать неинтуитивный результат для людей, которые только начали связывать свою жизнь с Haskell.

Prelude> sum (3,2)
2
Prelude> prod (3,2)
2
Prelude> or (True,False)
False

Проблема не была бы столь значима, если бы не повальная привычка писать что-то типа:

type MyComplex = (Double,Double)

А потом люди недоумевают, что же происходит с их программами. В приведенной в начале статьи ссылке идет жаркая дискуссия относительно того, “как мы дошли до жизни такой”, “раньше [haskell98] такой фигни не было” и прочее. Почитать весьма занимательно. В ситуацию уже вмешался SPJ (на стороне тех, кто выступает за уничтожение Foldable (,) a), так что как-нибудь оно да разрешится. Ну а мы пока можем сделать три простых вывода:

1. Повальная реализация всего и вся через Foldable хороша только тогда, когда все представители Foldable разумны, а не кортежи.
2. Кортежи стоит использовать только для временных значений, а не как один из важных типов в логике программы.
3. Стоит всегда предпочитать кортежу собственный тип-запись.