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

[thedeemon]

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

Comments

[gds]

1.
> Раз все молчат

а что о них говорить? Они были доступны в окамле ещё очень давно, ценой "значения-свидетеля равенства типов". Вполне юзабельно. Я там даже как-то налепил расширение на случай подтипизации, правда на практике не пригодилось.

А у окамловских GADT'ов, судя по рассылке, всё непросто с выводом подтипизации на полиморфных вариантах. Тогда как в явном случае (со значением-свидетелем) можно оформить любую правильную схему подтипизации. По крайней мере, проблемы будут видны явно, при реализации, а не раскапыванием кода компилятора.

2. вот я как-то вбросил на тему того, что GADT'ы нужны только для "typed evaluator of dsl", до сих пор никто не опроверг. Кроме того, смесь интуиции и олеговских примеров показывает, что для dsl (и его typed evaluator) не обязательно GADT'ы, достаточно простых функций (код будет в стиле, слегка напоминающем cps, но его можно сделать максимально-"шитым", т.е. чтобы всё вычисление выражения, находящегося в dsl-типах, было оптимальным -- вызывался бы только нужный код -- только closures, ответственные за логику выполнения, а не за логику интерпретации).

3. в lwt в исходниках видел камент про то, что типы input/output channel "будут представлены GADT'ами, когда они будут в языке". Впрочем, деталей не помню, но этот камент, как подсказывает интуиция, всё ещё есть в исходниках lwt.

[dmzlj]

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

[gds]

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

[dmzlj]

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

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

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

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

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

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

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

[migmit]

> вот я как-то вбросил на тему того, что GADT'ы нужны только для "typed evaluator of dsl", до сих пор никто не опроверг.

Ну, это зависит от понимания, что есть "typed evaluator of dsl", потому что при желании сюда можно притянуть за уши любой пример.

Вот, допустим, пишем мы библиотеку для работы со списками, но списками не конкретных типов - это Data.List, - а произвольных типов, поддерживающий заданный интерфейс. Такая библиотека будет содержать тип-обёртку:

data Wrapper c where Wrapper :: c a => a -> Wrapper c
type HeteroList c = [Wrapper c]

Без GADT-ов будет тяжело.

[gds]

а почему бы не сделать тупо? Выделить этот интерфейс в запись (или можно в объект, или в модульб если про окамл говорить), и складировать эти интерфейсы в список. Понятно, что решение тупое, но интересны его недостатки по сравнению с GADT'ами.

[migmit]

> Выделить этот интерфейс в запись (или можно в объект, или в модульб если про окамл говорить), и складировать эти интерфейсы в список.

Придётся для каждого класса делать отдельный тип записей, по сути дублируя существующий код. Соблюсти принцип DRY вполне можно, но... при помощи GADT-ов:

data Record c a where Record :: c a => Record c a

[nponeccop]

{-# LANGUAGE ExistentialQuantification #-}

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

[gds]

да, так. Только не обязательно функторы, в простом случае даже тупых лямбд хватает. Классический трюк с упаковыванием "2 forall 1 exists" остаётся в силе, но и без этого existential types есть. Остальное -- удобства, не обязательные, но желательные. И каждый дрочит как ему приятнее.

[migmit]

http://thedeemon.livejournal.com/51630.html?thread=657070#t657070

[gds]

вот, я тоже в сторону http://thedeemon.livejournal.com/51630.html?thread=655790#t655790 смотрел. Ну, в окамле будет чуть более явно: http://paste.in.ua/4565/

[migmit]

Ага, значит, экзистеншиалы за часть гадтов не считаем? Ладно, как насчёт типа Record выше? Это не просто экзистеншиал.

[gds]

> Ага, значит, экзистеншиалы за часть гадтов не считаем?

не считаем, так как для гадтов нужно только протягивание равенства между типами.

> Ладно, как насчёт типа Record выше? Это не просто экзистеншиал.

а вот тут, честно признаюсь, я не копенгаген. Начиная с того, что не совсем понимаю (хотя и есть догадки), что именно "data Record c a" постановляет. Наверное, Вам будет лень "возиться со мной", поэтому можем проехать этот вопрос.

[migmit]

Давайте вы не будете говорить за меня, ладно?

Постановляет только одно: наличие, собственно говоря, этого самого instance c a. То есть, если у вас есть какая-то функция вроде, скажем

f :: C a => Int -> (a -> String) -> Char -- от балды, по большей части

то вы можете соорудить функцию

f' :: Record C a -> Int -> (a -> String) -> Char
f' Record n h = f n h

при этом паттерн-матчинг по первому аргументу в левой части обеспечит вам право использовать instance C a в правой. Вариант

f' _ n h = f n h

не прокатит.

[migmit]

Собственно, можно и попроще. Общеизвестно, что список - монада, а вот Set - не монада, так как там на каждый чих нужен instance Ord для того, что в этом Set находится. С GADT-ами получается легко и приятно:

data Set' a where Set' :: Ord a => Set a -> Set' a
instance Monad Set' where
return = Set' . singleton
Set' sa >>= h = Set' $ fold (\a sb -> case h a of Set' sb' -> sb `union` sb') empty sa

если я не напутал нигде.

[nponeccop]

> Это не просто экзистеншиал.

Это и не GADT. Он требует ConstraintKinds, т.е. большинство реализаций GADT этого не позволяют.