haskell - DSL的GADT : swings and roundabouts?

Question

GADT好处的典型示例代表DSL的语法；说here on the wiki或the PLDI 2005 paper。

我可以看到，如果您的AST在构造上是正确的，则编写eval函数很容易。

如何将GADT处理程序构建为REPL？或更具体地说，是进入Read-Parse-Typecheck-Eval-Print-Loop？我看到您只是将eval步骤的复杂性推到了较早的步骤。

GHCi是否在内部使用GADT表示要评估的表达式？ (这些表达式比典型的DSL更加笨拙。)

一方面，您不能为GADT设置derive Show，因此对于“打印”步骤，您可以手动滚动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。

在最后一个项目符号上，我似乎还支持“智能构造函数”，那就是GADT应该改进(？)。此外，我还在某处加倍了工作。

我没有“更好的方法”来解决它。我想知道如何在实践中处理DSL应用程序。 (对于上下文:我正在考虑一个数据库查询环境，其中类型推断必须查看数据库中字段的类型以验证对其执行的操作。)

附加:经过@Alec的回答后，

我看到 glambda中用于 pretty-print 的代码涉及几层类和实例。与AST的GADT所声称的优势相反，这里有些不对劲。 (类型正确的)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使用相同的构造函数(用户不在乎它们来自不同的数据类型)；并且他们应用了“草率”的类型检查。 pretty-print /错误报告也不需要严格的类型检查。 Eval会这样做，并坚持将IsTerm实例全部排成一行。

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

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

Answer 1

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

DSL

为了使您的Term类型更加充实，请考虑使用 glambda 。它的 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类实现)。

evaluation code itself很漂亮，但是我怀疑是否需要以此为卖点。 :)

EDSL

据我了解，GADT对于EDSL(嵌入式DSL)非常出色，因为它们只是大型Haskell程序中代码的一部分。是的，类型错误可能很复杂(并且将直接来自GHC)，但这是您能够在代码中维护类型级不变式所要付出的代价。例如，考虑一下CFG中基本块的 hoopl表示:

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更酷，更实用。