haskell - 使用 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 标准中，有两种非常相似的结构——块和语句。块基本上只是也可以包含变量声明的语句列表。在这段代码中，我试图将语句声明为块项构造函数的子集（asSideEff和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)])

您可以在此处运行代码。

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

标签： haskell

Answer 1

（Haskell 专业提示：如果您发现自己不得不使用ImpredicativeTypes扩展程序，请将您的手从键盘上移开并远离计算机。）

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

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

这是一个产品类型String和一个列表。列表的元素具有 type forall a. BlockItem a，这是可以BlockItem a为任何事物的类型a（由值的调用者/用户选择）。正如@luqui 指出的那样，Var "a" (Lit 2)有这种类型——它可以是BlockItem a任何可能的a，但你的其他块项目不能。例如，Return (Lit 0)只能是BlockItem awhen ais a StmtType，所以不能放在[forall a. BlockItem a]列表中——类型太笼统了。

它类似于以下类型，它允许存储可以是任何类型的东西Num：

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

因为3and18 - 1可以是任何一种Num，我们可以将它们放在列表中：

mylist = NL [3, 18-1]

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

NL [_,x] = mylist

并将其视为Num我们想要的任何类型：

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

但是我们不能将特定Num类型（例如 an Int）放入列表中：

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

如果可以，那么我们可以这样写：

> let NL [x] = badlist in sqrt x

取sqrta Int，所有“类型地狱”都会崩溃。

所以，这就是你做错了。很难说你应该如何做正确。如果没有 GADT 和 DataKinds，为什么以下内容对您不起作用？

data Defn = Func String [BlockItem]

data BlockItem
  = Var String Expr
  | Stmt Statement

data Statement
  = SideEff Expr
  | Return Expr

data Expr
  = Lit Int