OCaml 4 и GADские Типы
Jul. 30th, 2012 06:10 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonРаз все молчат, напишу я. На днях вышел Окамл 4.0, в котором появились GADT. Рассказать о них можно на классическом примере: AST. Пусть у нас есть язычок с целыми числами, которые можно складывать и сравнивать. Результат сложения - целое число, результат сравнения - булев. Есть выражение if, в котором должно быть булево условие и пара выражений одинакового типа. Раньше, если мы все выражения этого язычка описали бы одним типом, то булевы и численные выражения оказались бы взаимозаменяемы, и проверку типов пришлось бы встраивать в интерпретатор, делать ее в рантайме. Если разнести численные и булевы выражения по разным типам, то можно было бы статически гарантировать, что условие в if'e точно будет булевым выражением, но пришлось бы делать разные функции для интерпретации и других операций над AST - как минимум одну для булевых выражений и одну для численных. С GADT можно все описать одним типом и одной функцией, не потеряв статических гарантий:
Тип expr устроен таким образом, что в условии у if'a может оказаться только булево выражение, а складываться и сравниваться могут только численные. При этом функция eval для целочисленных выражений возвращает int, а для булевых - bool:
Результат вычисления выражения if имеет тот же тип, что оба подвыражения-ветки, причем их тип должен быть одинаковым, иначе компилятор не даст построить такое if-выражение.
А какие полезные применения 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'ам знаете вы?
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2012-07-30 01:05 pm (UTC)Ну, это зависит от понимания, что есть "typed evaluator of dsl", потому что при желании сюда можно притянуть за уши любой пример.
Вот, допустим, пишем мы библиотеку для работы со списками, но списками не конкретных типов - это Data.List, - а произвольных типов, поддерживающий заданный интерфейс. Такая библиотека будет содержать тип-обёртку:
Без GADT-ов будет тяжело.
no subject
Date: 2012-07-30 01:12 pm (UTC)no subject
Date: 2012-07-30 01:24 pm (UTC)Придётся для каждого класса делать отдельный тип записей, по сути дублируя существующий код. Соблюсти принцип DRY вполне можно, но... при помощи GADT-ов:
no subject
Date: 2012-07-30 01:52 pm (UTC)data Obj = forall a. (Show a) => Obj a
xs :: [Obj]
xs = [Obj 1, Obj "foo", Obj 'c']
doShow :: [Obj] -> String
doShow [] = ""
doShow ((Obj x):xs) = show x ++ doShow xs
main = putStrLn $ doShow xs
В Окамле экзистеншиалы на функторах вроде как есть http://caml.inria.fr/pub/ml-archives/caml-list/2004/01/be82a912316130893f08204cbd86e0b5.en.html
no subject
Date: 2012-07-30 04:48 pm (UTC)no subject
Date: 2012-07-30 05:59 pm (UTC)no subject
Date: 2012-07-30 04:45 pm (UTC)no subject
Date: 2012-07-30 05:59 pm (UTC)no subject
Date: 2012-07-30 06:27 pm (UTC)не считаем, так как для гадтов нужно только протягивание равенства между типами.
> Ладно, как насчёт типа Record выше? Это не просто экзистеншиал.
а вот тут, честно признаюсь, я не копенгаген. Начиная с того, что не совсем понимаю (хотя и есть догадки), что именно "data Record c a" постановляет. Наверное, Вам будет лень "возиться со мной", поэтому можем проехать этот вопрос.
no subject
Date: 2012-07-30 06:47 pm (UTC)Постановляет только одно: наличие, собственно говоря, этого самого instance c a. То есть, если у вас есть какая-то функция вроде, скажем
то вы можете соорудить функцию
при этом паттерн-матчинг по первому аргументу в левой части обеспечит вам право использовать instance C a в правой. Вариант
не прокатит.
no subject
Date: 2012-07-30 09:43 pm (UTC)если я не напутал нигде.
no subject
Date: 2012-07-30 06:33 pm (UTC)Это и не GADT. Он требует ConstraintKinds, т.е. большинство реализаций GADT этого не позволяют.
no subject
Date: 2012-07-30 06:34 pm (UTC)no subject
Date: 2012-07-30 06:39 pm (UTC)data Record c a where Record :: c a => a -> Record c a
no subject
Date: 2012-07-30 06:48 pm (UTC)no subject
Date: 2012-07-30 07:12 pm (UTC)no subject
Date: 2012-07-30 07:15 pm (UTC)data Bool = False | True, например.no subject
Date: 2012-07-30 07:25 pm (UTC)Как его использовать для соблюдения DRY в примере?
no subject
Date: 2012-07-30 07:41 pm (UTC)Ничего себе "голый словарь". Это ж дофига информации!
> Как его использовать для соблюдения DRY в примере?
В примере — не слишком интересно.
data Wrapper' c where Wrapper' :: Record c a -> a -> Wrapper' c, те же яйца, вид в профиль.Куда интереснее использовать его для других целей. Например — как подсказать компилятору, что один класс есть подкласс другого? (Ну да, теоретически, компилятор и сам должен это выводить, но увы, не умеет)
А вот как:
Можно даже упростить создание инстансов, добавив в этот класс такое:
После этого, если есть какой-то
достаточно будет объявить
и компилятор удовлетворится. А вот
instance Show :<= Shit, илиinstance Num :<= Showне скомпилируются.Зачем это нужно? Ну, например, можно будет писать такое:
Без этого фокуса придётся отдельно делать
и те де.
no subject
Date: 2012-07-30 01:30 pm (UTC)