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

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