Dmitry Popov

(сам внезапно набирающий популярность ответ здесь)

Раз все молчат, напишу я. На днях вышел Окамл 4.0, в котором появились GADT. Рассказать о них можно на классическом примере: AST. Пусть у нас есть язычок с целыми числами, которые можно складывать и сравнивать. Результат сложения - целое число, результат сравнения - булев. Есть выражение if, в котором должно быть булево условие и пара выражений одинакового типа. Раньше, если мы все выражения этого язычка описали бы одним типом, то булевы и численные выражения оказались бы взаимозаменяемы, и проверку типов пришлось бы встраивать в интерпретатор, делать ее в рантайме. Если разнести численные и булевы выражения по разным типам, то можно было бы статически гарантировать, что условие в if'e точно будет булевым выражением, но пришлось бы делать разные функции для интерпретации и других операций над AST - как минимум одну для булевых выражений и одну для численных. С GADT можно все описать одним типом и одной функцией, не потеряв статических гарантий:

type 'a expr =  
  | I   : int -> int expr 
  | Add : int expr * int expr -> int expr 
  | Gt  : int expr * int expr -> bool expr 
  | If  : bool expr * 'a expr * 'a expr -> 'a expr;; 
 
let rec eval : type a . a expr -> a = function 
  | I n -> n 
  | Add(e1, e2) -> eval e1 + eval e2 
  | Gt(e1, e2)  -> eval e1 > eval e2 
  | If(cond, thn, els) -> if eval cond then eval thn else eval els;; 

Тип expr устроен таким образом, что в условии у if'a может оказаться только булево выражение, а складываться и сравниваться могут только численные. При этом функция eval для целочисленных выражений возвращает int, а для булевых - bool:

 
let e1 = If( Gt( Add(I 5, I 2), I 6 ),  I 1, I 0) in 
let b = Gt(I 1, I 2) in 
let e2 = If(b, b, b) in 
print_int (eval e1); 
Printf.printf " %b" (eval e2);; 

Результат вычисления выражения if имеет тот же тип, что оба подвыражения-ветки, причем их тип должен быть одинаковым, иначе компилятор не даст построить такое if-выражение.

А какие полезные применения GADT'ам знаете вы?

Лемму Йонеды называют самой сложной тривиальной вещью в математике. Сегодня мы попробуем закодировать ее на Окамле и понять ее связь с продолжениями (continuations). Лемма эта из теории категорий, я буду объяснять на пальцах, не слишком строго. В категории у нас есть коллекция объектов (порой очень большая, настолько, что это даже не обязательно множество) и коллекция стрелок между ними, также называемых морфизмами. Знакомый нам пример категории - где объекты это типы данных, а стрелки - функции между ними. Функтором называется отображение одной категории в другую (или в ту же, тогда это эндофунктор), сохраняющее структуру - "рисунок" стрелок. Он всякому объекту из первой категории сопоставляет некоторый объект из второй, и стрелки переносит соответственно. Конструкторы типов, вроде списка или дерева, - примеры (эндо)функторов в знакомой нам категории. Функтор "список" ('a list) отображает типы вроде int и string в типы вроде int list и string list, а функции вроде int -> string превращает в функции вроде int list -> string list. Такие вещи очень просто записываются на хаскеле, но сегодня я хочу использовать окамл, все-таки он наследник categorical abstract machine language. На окамле функтор в общем виде можно так, например, описать:

module type Functor = sig 
  type 'a t 
  val fmap : ('a -> 'b) -> 'a t -> 'b t 
end 

Это сигнатура модуля, "интерфейс". Реализуя его для конкретных конструкторов типов, вроде списка или дерева, мы получим конкретные функторы.

Если мы в некоторой категории С возьмем произвольный объект А, то ( Read more... )

Некоторое время назад меня пытались убедить, что Окамл недостаточно хорош для парсер-комбинаторов, потому что стоит попытаться добавить в парсеры состояние, как тут же возникают трудности, связанные с нехваткой полиморфизма. Проблема там вот в чем. Мой вариант простых парсеров не содержал состояния, и парсером там была функция типа char list -> 'a parse_result, где тип результата выглядел так:

type 'a parse_result = Parsed of 'a * char list | Failed

В определенном смысле какое-то состояние в таких парсерах есть - это текущая позиция в разбираемом тексте, определяемая неразобранным остатком текста, возвращаемым в случае успеха. Для разбора контекстно-зависимых грамматик иногда хочется, чтобы парсер имел какое-то дополнительное состояние. Например, при разборе текста на С++ хорошо бы помнить имена описанных ранее классов, чтобы понимать, что означает some_name(42). Расширим наше определение парсера и добавим передачу произвольного состояния:

type ('res, 'state) parse_result =  
  Parsed of 'res * ('state * char list) | Failed

( Read more... )

Итак, получив работающую виртуальную машину, я принялся за написание компилятора снизу-вверх. Первым делом система команд ВМ была описана в виде набора типов:

type dst = RegDest of int | PntDest of int;; 
type src = Reg of int | Pnt of int | Val of int;; 
 
type 'loc command =  
  | Arith of oper * dst * src * src 
  | Mov of dst * src 
  | Movb of dst * src 
  | Jmple of 'loc * src * src 
  | Jmpeq of 'loc * src * src 
  | Jmp of 'loc 
  | Print of src 
...

Сделал вывод ее в текст в форме, которую можно вставить в текст на Си: int prg[] = { ... };
Тут оказался очень полезен окамловский паттерн-матчинг, особенно когда появились команды, являющиеся частными случаями других:( Read more... )

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



mr_aleph тогда написал: Но потом меня посетила интересная мысль, что (мета)задача написать программу, которая строит стратегию поиска фальшивой монеты из N монет за M взвешиваний, это хороший программисткий этюд.

С этим я полностью согласен, поэтому решил написать программу, и пусть японский компьютер мне придумывает аргоритм. Задачка получилась довольно интересная, ведь не сразу ясно как именно описать предметную область и как должен выглядеть ответ: программа должна не найти монету, а по заданному числу монет и взвешиваний найти алгоритм решения задачи. В итоге у меня получилось такое решение из сотни строк Окамла с активным применением функций сильно высокого порядка и ленивых вычислений. Для 4 монет и 2 взвешиваний результат работы выглядит так:

Weigh [1 and 2]:
 if left heavier then 
  last weighting [2 and 4]:
   if left lighter then fake is 2
   if equal then fake is 1
 if left lighter then 
  last weighting [2 and 4]:
   if left heavier then fake is 2
   if equal then fake is 1
 if equal then 
  last weighting [2 and 4]:
   if left heavier then fake is 4
   if left lighter then fake is 4
   if equal then fake is 3

А для 9 монет и 3 взвешиваний вот так. Решение исходной задачки с 12 монетами программа выдала вот такое, неоптимальное но вроде рабочее. При поиске решения у меня плохо учитывается симметрия ситуаций, поэтому с ростом числа монет время работы растет очень быстро: решение для 8 монет находится за 0,2 секунды, для 9 - за 1,6с, для 10 - за 38с, а про 12 монет железяка думала 5 часов. :)

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

Я тут PHP-шников набираю, задаю всем одинаковое тестовое задание, чтобы присылали его вместе с резюме. Вот оно:

===============================================
Требуется написать программу, которая делает из "мухи" - "слона". Например:

муха -> мука -> рука -> руна -> ... -> слон

Т.е., меняя за 1 шаг по 1 букве, нужно из слова "муха" вывести слово "слон" и распечатать все шаги. Решите,
пожалуйста, задачу в этой постановке так, как сочтете нужным.
===============================================

Ощущение такое, что практически никто не может это нормально решить. Чего только не присылают...

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

А на днях я увидел упоминание этой задачки и там же вариант решения на PHP. Сначала не стал смотреть на решение и сделал свое, потом все же заглянул. И тогда я понял, что имел в виду автор письма.
Когда на работу устраиваются новички, это можно понять - с учетом низкого порога вхождения в РНР уровень среднего новичка там может быть сколь угодно низким. Но когда такие решения приходят от опытных вроде бы разработчиков, возникает ощущение, что все же РНР ест мозг.

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

Я летом писал про классические парсер-комбинаторы на Окамле и жаловался, что у меня не получилось сделать рекурсивные, вроде такого:

let rec p_exp =  p_char 'a' ||| (p_char '(' >>> p_exp >>> p_char ')')

Такой парсер должен разбирать строки 'a', '(a)', '((a))' и т.д., но ругаться на '((a)'.

При попытке компиляции приведенной строчки выдавалось малоинформативное сообщение This kind of expression is not allowed as right-hand side of `let rec'. Оказывается, все очень просто. В правой части let rec может быть очень ограниченный набор конструкций, если они содержат одно из рекурсивно определяемых имен. Одна из поддерживаемых - fun. Все начинает компилироваться и правильно работать, если обернуть правую часть в нее:

let rec p_exp = fun s -> (p_char 'a' ||| (p_char '(' >>> p_exp >>> p_char ')')) s

В связи с возросшей в последнее время популярностью Окамла в ЖЖ, решил поделиться своим раскрашивателем кода.
Скармливаешь ему текст на Окамле и получаешь готовый HTML для вставки в текст поста ЖЖ. Никаких CSS отдельно настраивать не надо.

Краткий вариант:

Более полный вариант (с настройкой цветов):
http://ocolor.thedeemon.com/

На днях в качестве эксперимента реализовал на OCaml идею оптимизирующих парсер-комбинаторов.
На одном ядре 2.33 GHz и тестовой задачке с рсдн получилось 35 МБ в секунду, что существенно быстрее обычных парсер-комбинаторов на Окамле и даже вроде бы быстрее чем С++ / Boost.Spirit.