使用GADT和构造函数子集的C语言AST

Question

我想定义类型级别安全的C语言AST。到目前为止，我想出了这样的东西：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}

data Defn
  = Func String [Block]

type Block = forall a. BlockItem a
type Stmt = BlockItem StmtType

data BlockItemKind = StmtType

data BlockItem :: BlockItemKind -> * where
  Var :: String -> Expr -> BlockItem a
  SideEff :: Expr -> BlockItem StmtType
  Return :: Expr -> BlockItem StmtType

data Expr
  = Lit Int

关键是BlockItem数据类型。在C标准中，有两个非常相似的结构-块和语句。块基本上是可以包含变量声明的语句列表。在这段代码中，我试图将语句声明为块项构造函数(如SideEff和Return)的子集。

但是，此代码不像预期的那样工作。请考虑以下打印此AST的代码：

showDefn :: Defn -> String
showDefn (Func name block) = "func " ++ name ++ " . " ++ show (showBlock <$> block)

showBlock :: Block -> String
showBlock (Var name e) = name ++ " = " ++ showExpr e ++ ";"
showBlock e = showStmt e

showStmt :: Stmt -> String
showStmt (SideEff e) = showExpr e ++ ";"
showStmt (Return e) = "return " ++ showExpr e ++ ";"

showExpr :: Expr -> String
showExpr (Lit x) = show x

当我用showDefn评估[Block]时，一切都很好。但是，当我使用Stmt类型时，此代码无法工作：

main :: IO ()
main = do
  -- FOLLOWING WORK
  print $ showDefn (Func "foo" [Var "a" (Lit 2), Var "b" (Lit 3)])

  -- FOLLOWING DOES NOT WORK
  print $ showDefn (Func "foo" [Return (Lit 0)])
  print $ showDefn (Func "foo" [Var "a" (Lit 1), SideEff (Lit 2)])

您可以运行代码这里。

问题出在哪里？我甚至不确定，这是否是正确的设计。

Answer 1

(Haskell支持提示:如果你发现自己不得不使用ImpredicativeTypes扩展，把你的手从键盘上拿开，远离电脑。)

无论如何，要详细说明@luqui的评论，Defn类型相当于：

data Defn = Func String [forall a. BlockItem a]

这是String和list的产品类型。列表中的元素具有forall a. BlockItem a类型，它是任何a (由值的调用方/用户选择)的BlockItem a类型。正如@luqui所指出的，Var "a" (Lit 2)有这种类型--它可以是任何可能的a的BlockItem a，但您的其他块项不能。例如，当a是StmtType时，Return (Lit 0)只能是BlockItem a，所以不能放在[forall a. BlockItem a]列表中--这种类型对它来说太笼统了。

它类似于下面的类型，它允许存储任何类型的Num

data NumList = NL [forall a. Num a => a]

因为3和18 - 1可以是任何类型的Num，所以我们可以将它们放在列表中：

mylist = NL [3, 18-1]

稍后，我们可以提取此列表中的一个元素：

NL [_,x] = mylist

把它当作我们想要的任何一种Num：

> x :: Integer
17
> x :: Double
17.0

但是我们不能将特定的Num类型(例如，Int)放到列表中：

badlist = NL [length "hello"]  -- type error

如果可以的话，我们就可以写：

> let NL [x] = badlist in sqrt x

要想获得sqrt of a Int，所有的“类型地狱”都会崩溃。

所以，这就是你做错的地方。很难说你该怎么做才对。为什么在没有and和DataKinds的情况下，下面的内容对您不起作用呢？

data Defn = Func String [BlockItem]

data BlockItem
  = Var String Expr
  | Stmt Statement

data Statement
  = SideEff Expr
  | Return Expr

data Expr
  = Lit Int