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 11:57 am (UTC)http://hackage.haskell.org/packages/archive/hoopl/3.8.7.4/doc/html/src/Compiler-Hoopl-Graph.html#O
For example,
• A shift-left instruction is open on entry (because control can
fall into it from the preceding instruction), and open on exit
(because control falls through to the next instruction).
• An unconditional branch is open on entry, but closed on exit
(because control cannot fall through to the next instruction).
• A label is closed on entry (because in Hoopl we do not allow
control to fall through into a branch target), but open on exit.
http://research.microsoft.com/en-us/um/people/simonpj/papers/c--/dfopt.pdf
http://blog.ezyang.com/2011/04/hoopl-guided-tour-base-system/
no subject
Date: 2012-07-30 12:43 pm (UTC)> Раз все молчат
а что о них говорить? Они были доступны в окамле ещё очень давно, ценой "значения-свидетеля равенства типов". Вполне юзабельно. Я там даже как-то налепил расширение на случай подтипизации, правда на практике не пригодилось.
А у окамловских GADT'ов, судя по рассылке, всё непросто с выводом подтипизации на полиморфных вариантах. Тогда как в явном случае (со значением-свидетелем) можно оформить любую правильную схему подтипизации. По крайней мере, проблемы будут видны явно, при реализации, а не раскапыванием кода компилятора.
2. вот я как-то вбросил на тему того, что GADT'ы нужны только для "typed evaluator of dsl", до сих пор никто не опроверг. Кроме того, смесь интуиции и олеговских примеров показывает, что для dsl (и его typed evaluator) не обязательно GADT'ы, достаточно простых функций (код будет в стиле, слегка напоминающем cps, но его можно сделать максимально-"шитым", т.е. чтобы всё вычисление выражения, находящегося в dsl-типах, было оптимальным -- вызывался бы только нужный код -- только closures, ответственные за логику выполнения, а не за логику интерпретации).
3. в lwt в исходниках видел камент про то, что типы input/output channel "будут представлены GADT'ами, когда они будут в языке". Впрочем, деталей не помню, но этот камент, как подсказывает интуиция, всё ещё есть в исходниках lwt.
no subject
Date: 2012-07-30 12:49 pm (UTC)no subject
Date: 2012-07-30 12:51 pm (UTC)no subject
Date: 2012-07-30 12:58 pm (UTC)Суть такова: есть у нас некие команды. У команды есть опкод, и есть операнды.
Опкод --- ну просто некие значения, идущие последовательно, без дырок.
Операнды --- ну, операнды разной разрядности, Word32 допустим. Или Word16. Или Word64. Или Label (которая потом заменяется на Word-соответствующей-разрядности-после-линковки)
С одной стороны, команды обрабатываются унифицировано. Ну, что там с ними делается --- допустим, asm pretty printing или генерация бинарных кодов.
С другой стороны, типы Команда Опкод Операнды надо бы задавать жёстко, что бы если уж определено, что инструкция имеет такой-то формат --- ни в каком другом формате ее нельзя бы было определить.
Что-то эта задача решалась только через
GADT + экзистенциальные типы + макро для генерации типов, причем GADT в таком случае особенно-то и не нужен оказался. Я так и не осилил это нормально типизировать как-то.
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)no subject
Date: 2012-07-30 01:39 pm (UTC)Ну, GADTs are poor man's dependent types - на них произвольные статические гарантии можно записывать, вроде тотальности head и сбалансированности деревьев (cтр. 87)
Тот же HOOPL уже упоминался - я использую его в HNC, удобно.
См. тж.
http://lambda-the-ultimate.org/node/1293
http://www.cs.st-andrews.ac.uk/~eb/drafts/tfp08.pdf
no subject
Date: 2012-07-30 04:11 pm (UTC)А в overbld 4.0 стоит ожидать? А то я какой-то виндовый инсталлятор по ссылке из рассылки нашел, он в байткод нормально компилит, а с ocamlopt опять все непросто.
no subject
Date: 2012-07-30 04:20 pm (UTC)no subject
Date: 2012-07-30 07:02 pm (UTC)no subject
Date: 2012-07-30 07:47 pm (UTC)Замечательно двумя вещами: ясностью и полной неожиданностью для многих хаскелистов.
no subject
Date: 2012-07-30 07:49 pm (UTC)no subject
Date: 2012-07-30 07:56 pm (UTC)no subject
Date: 2012-07-31 02:27 am (UTC)