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

[migmit.livejournal.com]

Не понял, в чём проблема с конструированием. Конструктор-то есть.

[nponeccop.livejournal.com]

Он без параметров

[migmit.livejournal.com]

Э-э-э... и? Мы конструкторов без параметров не видали, что ли? data Bool = False | True, например.

[nponeccop.livejournal.com]

Так у Bool паттерн-матчинг позволяет извлекать полезную информацию. А здесь из полезной информации - голый словарь.

Как его использовать для соблюдения DRY в примере?

[migmit.livejournal.com]

> А здесь из полезной информации - голый словарь.

Ничего себе "голый словарь". Это ж дофига информации!

> Как его использовать для соблюдения DRY в примере?

В примере — не слишком интересно. data Wrapper' c where Wrapper' :: Record c a -> a -> Wrapper' c, те же яйца, вид в профиль.

Куда интереснее использовать его для других целей. Например — как подсказать компилятору, что один класс есть подкласс другого? (Ну да, теоретически, компилятор и сам должен это выводить, но увы, не умеет)

А вот как:

data Void (c :: * -> Constraint) = Void -- это чисто для удобства
class c1 :<= c2 where
  isSubClass :: c1 a => Void c1 -> Record c2 a

Можно даже упростить создание инстансов, добавив в этот класс такое:

  default isSubClass :: c2 a => Void c1 -> Record c2 a
  isSubClass _ = Record

После этого, если есть какой-то

class Show a => Shit a where -- ну, там, какие-то методы

достаточно будет объявить

instance Shit :<= Show

и компилятор удовлетворится. А вот instance Show :<= Shit, или instance Num :<= Show не скомпилируются.

Зачем это нужно? Ну, например, можно будет писать такое:

instance (c :<= Show) => Show (Wrapper c) where
  show (Wrapper (x :: a)) = case isSubClass (Void :: Void c) :: Record Show a of Record -> show x

Без этого фокуса придётся отдельно делать

instance Show (Wrapper Show) where show (Wrapper x) = show x
instance Show (Wrapper Shit) where show (Wrapper x) = show x

и те де.