Типичные примеры преимуществ GADT представляют синтаксис для DSL;скажем здесь, на вики или бумаге PLDI 2005 .
Я могу видеть, что если у вас есть AST, который по типу корректен по конструкции, пишите evalФункция проста.
Как встроить обработку GADT в REPL?Или, более конкретно, в цикл чтения-разбора-проверки типа-проверки-печати?Я вижу, что вы просто подталкиваете сложность от шага eval к более ранним шагам.
Использует ли GHCi внутренний GADT для представления выражений, которые он оценивает?(Выражения намного короче, чем типичные DSL.)
С одной стороны, вы не можете derive Show для GADT, поэтому для шага печати вы либо катитесь вручнуюShow экземпляров или что-то вроде этого:
{-# LANGUAGE GADTs, StandaloneDeriving #-}
data Term a where
Lit :: Int -> Term Int
Inc :: Term Int -> Term Int
IsZ :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
Pair :: (Show a, Show b) => Term a -> Term b -> Term (a,b)
Fst :: (Show b) => Term (a,b) -> Term a
Snd :: (Show a) => Term (a,b) -> Term b
deriving instance (Show a) => Show (Term a)
(Мне кажется, что эти Show ограничения, запутанные в конструкторах, уже не в состоянии разделить проблемы.)
Я больше думаю о пользовательском опыте, когда кто-то вводит выражения DSL, а не об удобстве программиста функцией eval.Либо:
- Пользователь вводит выражения непосредственно с помощью конструкторов GADT.Легко сделать синтаксически правильную, но неправильно напечатанную ошибку (скажем, неправильно поставленные парены).Тогда GHCi дает довольно недружелюбные сообщения об отказе.Или
- REPL принимает ввод как текст и анализирует его.Но для GADT, подобного этому, получение экземпляра
Read - это действительно тяжелая работа.Так что, возможно, - Приложение имеет две структуры данных: одна допускает ошибки типа;другой - ГАДТ;и шаг проверки создает GADT AST, если он может сделать это безошибочно с типом.
В этой последней статье я, кажется, вернулся с «умными конструкторами», которые GADT должны улучшить(?) Более того, я где-то удвоил работу.
У меня нет «лучшего способа» подойти к ней.Мне интересно, как на практике подходить к приложениям DSL.(Для контекста: я имею в виду среду запросов к базе данных, где вывод типов должен смотреть на типы полей в базе данных, чтобы проверить, какие операции над ними.)
Addit: после проработки ответа от @ Alec
Я вижу, что код для красивой печати в glambda включает несколько слоев классов и экземпляров.Здесь что-то не так, в отличие от заявленных преимуществ GADT для AST.Идея (хорошо типизированного) AST заключается в том, что вы можете одинаково легко: оценить его;или просто распечатай;или оптимизировать его;или генерировать код из него;и т. д.
glambda, кажется, нацелены на повышение квалификации (что достаточно справедливо с учетом цели упражнения).Мне интересно ...
Зачем нужно выражать весь синтаксис для (E) DSL в одном типе данных?(Пример из викибук начинает, когда соломенный человек делает это data Expr = ...; и быстро сталкивается с проблемами типа. Ну, конечно, это так; это никогда не сработает; почти все будет работать лучше этого; я чувствую себя обманутым.)
Если мы все равно в конечном итоге пишем классы и экземпляры, почему бы не сделать каждый синтаксис производящим отдельный тип данных: data Lit = Lit Int ... data If b a1 a2 = If b a1 a2 ... Тогда a class IsTerm a c | a -> c where ... (то есть a FunDep или, возможно, семейство типов, экземпляры которого сообщают нам тип результата термина.)
Теперь в EDSL используются одни и те же конструкторы (пользователю не важно, что они имеют разные типы данных);и они применяют «небрежную» проверку типов.Хорошая печать / отчеты об ошибках также не требуют строгой проверки типов.Эвал делает это и настаивает на том, чтобы все экземпляры IsTerm были выстроены в ряд.
Я не предлагал такой подход раньше, потому что он, казалось, содержал слишком много грубого кода.Но на самом деле это не хуже, чем glambda - то есть, когда вы рассматриваете всю функциональность, а не только шаг eval.
Мне кажется большим преимуществом выражать синтаксис только один раз.Более того, это кажется более расширяемым: добавьте новый тип данных для каждого синтаксического производства, а не взламывайте существующий тип данных.Да, и, поскольку они являются типами данных H98 (без экзистенциалов), deriving отлично работает.