DSL 的 GADT：摇摆和迂回？

Question

GADT 优势的典型示例是表示 DSL 的语法；说 here on the wiki or the PLDI 2005 paper.

我可以看出，如果你有一个通过构造类型正确的 AST，编写一个 eval 函数很容易。

如何将 GADT 处理构建到 REPL 中？或者更具体地说，进入 Read-Parse-Typecheck-Eval-Print-Loop？我发现您只是将 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；并且验证步骤构造 GADT AST，如果它可以类型安全地这样做的话。

在最后一个项目符号中，我似乎回到了 'smart constructors'，GADT 应该改进（？）更重要的是我在某处加倍了工作。

我没有 'better way' 来接近它。我想知道如何在实践中处理 DSL 应用程序。（对于上下文：我正在考虑一个数据库查询环境，其中类型推断必须查看数据库中字段的类型以验证对它们的操作。）

添加： 在完成@Alec

的回答后

我看到 glambda 中的漂亮打印代码涉及多个层类和实例。与 GADT 对 AST 的声称优势相反，这里感觉有些不对劲。（类型良好的）AST 的想法是您同样可以轻松地：评估它；或漂亮地打印出来；或优化它；或从中生成代码；等等

glambda 似乎旨在评估（考虑到练习的目的，这很公平）。我想知道...

为什么需要用一种数据类型表达 (E)DSL 的整个语法？（wikibook 示例开始它的稻草人这样做 data Expr = ...；并很快遇到类型问题。当然是这样；那永远行不通；几乎任何东西都比那更好；我觉得被骗了。）
如果我们最终写成类和实例，为什么不让每个语法产生一个单独的数据类型：data Lit = Lit Int ... data If b a1 a2 = If b a1 a2 ...然后是一个 class IsTerm a c | a -> c where ...（即 FunDep 或者一个类型族，其实例告诉我们术语的结果类型。）
现在 EDSL 使用相同的构造函数（用户不关心它们来自不同的数据类型）；他们应用 'sloppy' 类型检查。漂亮的 printing/error 报告也不需要严格的类型检查。 Eval 确实如此，并坚持 IsTerm 个实例都排成一行。

我以前没有建议过这种方法，因为它似乎涉及太多笨拙的代码。但实际上它并不比 glambda 差——也就是说，当您考虑整个功能时，而不仅仅是评估步骤。

在我看来，只表达一次语法是一个很大的优势。此外，它似乎更具可扩展性：为每个语法生成添加一个新的数据类型，而不是打破现有的数据类型。哦，因为它们是 H98 数据类型（没有存在性），deriving 工作正常。

Answer 1

请注意，GHCi 不使用 GADT 来表示表达式。甚至 GHC 的内部核心表达式类型 Expr 也不是 GADT。

DSL

为了获得更大更充实的 Term 类型示例，请考虑 glambda. Its Exp 类型甚至在类型级别跟踪变量。

还有第二种 UExp 数据类型，正如您自己观察到的那样，它实际上是从 REPL 中解析出来的。这个类型然后被类型检查到 Exp 并传递给一个延续：
```
check :: (MonadError Doc m, MonadReader Globals m)
      => UExp -> (forall t. STy t -> Exp '[] t -> m r)
      -> m r
```
UExp 和 Exp 的漂亮打印是手写的，但至少 uses the same code（它通过 PrettyExp class).
evaluation code itself 很漂亮，但我怀疑我是否需要就此向您推销。 :)

EDSL

据我所知，GADT 非常适合 EDSL（嵌入式 DSL），因为它们只是大型 Haskell 程序中的部分代码。是的，类型错误可能很复杂（并且将直接来自 GHC），但这是您为能够在代码中维护类型级不变量而付出的代价。例如，考虑 hoopl 对 CFG 中基本块的表示：

data Block n e x where
  BlockCO  :: n C O -> Block n O O          -> Block n C O
  BlockCC  :: n C O -> Block n O O -> n O C -> Block n C C
  BlockOC  ::          Block n O O -> n O C -> Block n O C

  BNil    :: Block n O O
  BMiddle :: n O O                      -> Block n O O
  BCat    :: Block n O O -> Block n O O -> Block n O O
  BSnoc   :: Block n O O -> n O O       -> Block n O O
  BCons   :: n O O       -> Block n O O -> Block n O O

当然，您可能会遇到严重的类型错误，但您也有能力在类型级别跟踪失败信息。这使得考虑数据流问题变得容易得多。

那又怎样...?

我想表达的观点是：如果您的 GADT 是从 String（或自定义 REPL）构建的，您将很难执行翻译.这是不可避免的，因为您所做的实际上是重新实现一个简单的类型检查器。 您最好的办法是直面这个问题（就像 glambda 所做的那样）并将解析与类型检查区分开来.

但是，如果您能够负担得起 Haskell 代码的限制，您可以将解析和类型检查交给 GHC。恕我直言，EDSL 比非嵌入式 DSL 更酷、更实用。

DSL 的 GADT：摇摆和迂回？

GADTs for a DSL: swings and roundabouts?

haskell

gadt

DSL

EDSL

那又怎样...?