Почему Haskell не не ML

 1. Теория.

Многие слышали про изоморфизм Карри-Ховарда, связывающий типы с логическими высказываниями, а программы с доказательствами. Конкретнее, есть такая штука, как логика высказываний (propositional logic). Она содержит ряд правил как из одних высказываний выводить другие. Например, если нам известна достоверность высказываний А и В, то из этого мы можем вывести достоверность высказывания А & B. Это правило ввода &. Аналогично, если у нас в программе есть значения типов А и В, мы можем построить значение типа А & B - тупл (а, b). Есть правило избавления от &: если известна достоверность высказывания А & В, то из него мы можем вывести достоверность А, а можем вывести В. Аналогично, имея тупл p типа А & B, мы можем получить значения типа А и типа В: 
let a = fst p
let b = snd p  
(здесь и дальше примеры кода на Окамле)

Затем вводится понятие импликации. Если мы допустим (предположим) достоверность высказывания А и из этого сможем вывести достоверность высказывания В, значит из А следует В, и справедливо высказывание А => B. Аналогично, если мы знаем, как из значения типа А вычислить значение типа В, то, значит, можем описать функцию из А в В, она будет иметь тип А -> B. Правило избавления от => известно также как Modus ponens: если известна достоверность высказывания А и высказывания А => B, то из них мы можем вывести достоверность высказывания В. Прямой аналог этого - вычисление: если у нас есть значение x типа А и функция f типа А -> В, то мы можем вычислить значение f(x) типа В.

Имея конъюнкцию и импликацию, мы можем определить дизъюнкцию (ИЛИ). Смысл высказывания А | B в том, что нам известна достоверность хотя бы одного из них. Правило ввода: если известна достоверность высказывания А, то из нее мы уже можем вывести достоверность высказывания А | B. Прямой аналог дизъюнкции - sum types, они же discriminated unions:

type int_or_string = Int of int | Str of string

Тут, имея число или строку, мы можем создать значение типа int_or_string, применив один из конструкторов. Правило избавления от дизъюнкции: если нам известна достоверность высказывания А | B, и мы из предположения А можем вывести достоверность высказывания С, а также из предположения В можем тоже вывести достоверность С (т.е. A => C и B => C), то из этих трех мы можем вывести достоверность С. Прямой аналог этого: если у нас есть значение типа A | B, и функции A -> C и B ->C, то мы можем получить значение типа С:

let to_float = function (* имеет тип int_or_string -> float  *) 
  | Int n -> float_of_int n 
  | Str s -> float_of_string s

Дальше интереснее: отрицание. Высказывание -А (не А) по определению достоверно тогда, когда из А мы можем прийти к абсурду, противоречию. Т.е. по определению -А = (А => _|_), где _|_ - это противоречие. Аналогом отрицания выступает продолжение (continuation) - нечто, что принимает на вход значение типа А и что-то с ним делает, обратно уже не возвращаясь. Его можно рассматривать как функцию из А в задницу (bottom, _|_), т.е. не возвращающую управление. В любом месте программы, когда мы вычисляем какое-либо значение типа А, у нас есть остаток программы, который что-то с этим значением может делать, а обратно уже не вернется, его мы можем рассматривать  как продолжение типа -А, или функцию А -> _|_.

В логике мы можем показать эквивалентность формул A => B  и -(A & -B). Действительно, если мы знаем, что из А следует В, то А & -B не может быть достоверным, ведет к противоречию, значит справедливо высказывание -(A & -B). Как этот факт выглядит с т.з. вычислений? Функция из А в В есть некий код, который принимает пару значений. Первое значение - аргумент функции, значение типа А, а второе - код, который принимает значение типа В и что-то с ним делает. По сути, это остаток программы, которая вызвала нашу функцию. Этот остаток должен получить значение типа В и что-то с ним делать, т.е. имеет тип -В. Если мы посмотрим, как обычно компилируется вызов функций, то увидим ту же пару: на стек кладется аргумент А и адрес возврата - это и есть значение типа -В. А сама функция принимает на вход эту пару и что-то с ней делает, т.е. имеет тип -(A & -B).

Теперь мы приходим к ленивым вычислениям. Если мы знаем, как вычислить некое значение типа А, но не хотим этого делать до тех пор, пока оно на самом деле не понадобится, то используем следующую схему. Когда где-то в программе это значение понадобится, то остаток программы будет продолжением, принимающим значение типа А, т.е. это будет -А. Теперь, вместо значения типа А мы можем хранить thunk - код, который принимает продолжение типа -А, вычисляет нужное значение и отдает его этому продолжению. Т.е. вычисление было отложено до того момента, когда его результат понадобился. Поскольку thunk принимает -А и что-то с ним делает, его тип --А, т.е. "не не А". Для каждого значения типа А мы можем построить такой thunk и получить эквивалентное ленивое значение типа --А с отложенным вычислением.

2. Практика.

Данный пост написан по результатам осмысления одноименной статьи за авторством преподобного SPJ, Алана Майкрофта (тоже большое имя в теории ЯП) и, совершенно неожиданно, товарища по имени Ben Rudiak-Gould, который известен как автор самого популярного беспотерьного видеокодека HuffYUV и системы скриптового видеоредактирования AviSynth. В статье они, помимо изложения теории, предлагают простую императивную абстрактную машину с командами выделения памяти, чтения-записи и перехода по адресу, и описывают компиляцию в нее некоего промежуточного представления (IL), которое интересно тем, что в нем система типов содержит туплы (А & B), суммы (A | B) и продолжения (-A), но не содержит обычных функций (A -> B). А дальше они описывают простенький чистый функциональный язык с привычными конструкциями (определение функции, применение ее, создание туплов, их матчинг для получения составляющих, создание суммарных типов (Left a, Right a) и их матчинг), а затем описывают два способа компиляции его в IL: в одном случае получается семантика строгая, а во втором ленивая. Т.е. исходный язык один и тот же, целевой язык тоже один, а разница между строгой и ленивой семантикой только в манере компиляции. И суть ее именно в том, что ленивые значения компилируются в санки типа --А.

В процессе осмысления статьи я реализовал на Окамле интепретатор IL (вместо компиляции в абстрактную машину) и оба способа компиляции функционального языка (FL) в этот IL - строгий и ленивый. IL и FL я расширил, добавив туда числовые константы и функции для вывода значений. Вся программа (2 сотни строк) представлена здесь, зависимостей у нее нет, компилируется тривиально. Там в конце составляется AST программы на FL, компилируется в IL и запускается интерпретация. В зависимости от того, каким из способов шла компиляция, результат работы разный: в одном случае вычисляются все компоненты тупла и выводятся соответствующие значения (с другой парой - выбрасывается ошибка), а в другом случае вычисляется только один из компонентов и ошибки не происходит.