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

[thedeemon]

Раз все молчат, напишу я. На днях вышел Окамл 4.0, в котором появились GADT. Рассказать о них можно на классическом примере: AST. Пусть у нас есть язычок с целыми числами, которые можно складывать и сравнивать. Результат сложения - целое число, результат сравнения - булев. Есть выражение if, в котором должно быть булево условие и пара выражений

Comments

[isorecursive]

В Hoopl их изящно используют - для описания открыто-закрытости форм потока управления:
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.pdfhttp://blog

[gds]

1

[dmzlj]

я как-то пытался на GADT типизировать опкоды, но не сумел. Пришлось в рантайме проверять.

[gds]

интересненько, а что требовалось от этой типизации?

[dmzlj]

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

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

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

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

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

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

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

[stdray]

А разве не через них реализуются всякие option[T] и either[T,U]? Если, конечно, я правильно все понял.

[triampurum]

вот замечательное определение: http://cstheory.stackexchange.com/questions/10594/whats-the-difference-between-adts-gadts-and-inductive-types/10596#10596
Замечательно двумя вещами: ясностью и полной неожиданностью для многих хаскелистов.

[triampurum]

(и считаем комментарии "это определение неверно")

[migmit]

Можно, я буду первым? Это определение - хуйня. jbapple там правильно сказал.