OCaml 4 и GADские Типы

[thedeemon]

Раз все молчат, напишу я. На днях вышел Окамл 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'ам знаете вы?

Comments

[dmzlj.livejournal.com]

Сейчас попробую сформулировать, давненько было.

Суть такова: есть у нас некие команды. У команды есть опкод, и есть операнды.

Опкод --- ну просто некие значения, идущие последовательно, без дырок.

Операнды --- ну, операнды разной разрядности, Word32 допустим. Или Word16. Или Word64. Или Label (которая потом заменяется на Word-соответствующей-разрядности-после-линковки)

С одной стороны, команды обрабатываются унифицировано. Ну, что там с ними делается --- допустим, asm pretty printing или генерация бинарных кодов.

С другой стороны, типы Команда Опкод Операнды надо бы задавать жёстко, что бы если уж определено, что инструкция имеет такой-то формат --- ни в каком другом формате ее нельзя бы было определить.


Что-то эта задача решалась только через
GADT + экзистенциальные типы + макро для генерации типов, причем GADT в таком случае особенно-то и не нужен оказался. Я так и не осилил это нормально типизировать как-то.