DSL的GADT:波动和环形交叉口？

Question

GADT的优点的典型示例代表DSL的语法; 说这里的维基或在PLDI 2005年纸.

我可以看到,如果你通过构造得到一个类型正确的AST,那么编写一个eval函数很容易.

如何将GADT处理构建到REPL中？或者更具体地说是Read-Parse-Typecheck-Eval-Print-Loop？我看到你只是将eval步骤的复杂性推到了前面的步骤中.

GHCi是否在内部使用GADT来表示它正在评估的表达式？(表达式比典型的DSL要厚很多.)

• 首先,您不能derive Show使用GADT,因此对于Print步骤,您可以手动滚动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构造函数直接输入表达式.很容易做出语法上正确但错误的错误(比如错误的parens).然后GHCi给出了相当不友好的拒绝消息.要么
• REPL将输入作为文本并解析它.但对于这样的GADT来说,获得一个Read实例真的很辛苦.也许吧
• 该应用程序有两种数据结构:一种是类型错误容忍的; 另一个是GADT; 并且验证步骤构造GADT AST,如果它可以安全地类型化.

在最后一个子弹,我似乎回到了'聪明的构造者',GADT应该改进(？)我的工作在某个地方翻了一倍.

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

Addit:在完成@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使用相同的构造函数(用户并不关心它们来自不同的数据类型); 他们应用'马虎'式检查.漂亮的打印/错误报告也不需要严格的类型检查.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是手写的，但至少使用相同的代码（它通过PrettyExp类来实现）。

• 该评估代码本身是美丽的，但我怀疑我需要向你推销上。:)

EDSL

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

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