使用 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

当我用[Block]评估showDefn时，一切正常。但是，当我使用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和列表的产品类型。 列表的元素具有类型forall a. BlockItem a，这是可以为任何a(由值的调用方/用户选择)BlockItem a事物的类型。 正如@luqui指出的那样，Var "a" (Lit 2)有这种类型——它可以是任何可能的a的BlockItem a，但你的其他块项目不能。 例如，Return (Lit 0)只有在a是StmtType时才能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

拿一个Int的sqrt，所有的"类型地狱"都会崩溃。

所以，这就是你做错的地方。 很难说你应该如何做对。 为什么没有 GADT 和 DataKinds 的以下方法对您不起作用？

data Defn = Func String [BlockItem]
data BlockItem
= Var String Expr
| Stmt Statement
data Statement
= SideEff Expr
| Return Expr
data Expr
= Lit Int