不断发展的数据结构

Question

我正在尝试在Haskell中为类C语言编写编译器.编译器通过转换AST来进行.第一个传递解析输入以创建AST,使用符号表绑定结点,以允许在定义符号之前定位符号,而无需前向引用.

AST包含有关类型和表达式的信息,它们之间可以有连接; 例如,sizeof(T)是一个依赖于类型的表达式T,并且T[e]是一个依赖于常量表达式的数组类型e.

类型和表达式由Haskell数据类型表示,如下所示:

data Type = TypeInt Id
          | TypePointer Id Type -- target type
          | TypeArray Id Type Expr -- elt type, elt count
          | TypeStruct Id [(String, Type)] -- [(field name, field type)]
          | TypeOf Id Expr
          | TypeDef Id Type

data Expr = ExprInt Int -- literal int
          | ExprVar Var -- variable
          | ExprSizeof Type
          | ExprUnop Unop Expr
          | ExprBinop Binop Expr Expr
          | ExprField Bool Expr String -- Bool gives true=>s.field, false=>p->field

其中Unop包括address-of(&)和dereference(*)等Binop运算符,并包含plus(+)和times(*)等运算符......

请注意,每种类型都分配了唯一的Id.这用于构造类型依赖图,以便检测导致无限类型的循环.一旦我们确定类型图中没有循环,就可以安全地对它们应用递归函数而不会进入无限循环.

下一步是确定每种类型的大小,为结构字段分配偏移量,并ExprField用指针算法替换s.在这样做时,我们可以确定表达式的类型,并从类型图中消除ExprSizeofs,ExprFields,TypeDefs和TypeOfs,因此我们的类型和表达式已经发展,现在看起来更像是这样:

data Type' = TypeInt Id
           | TypePointer Id Type'
           | TypeArray Id Type' Int -- constant expression has been eval'd
           | TypeStruct Id [(String, Int, Type')] -- field offset has been determined

data Expr' = ExprInt Type' Int
           | ExprVar Type' Var
           | ExprUnop Type' Unop Expr'
           | ExprBinop Type' Binop Expr' Expr'

请注意,我们已经删除了一些数据构造函数,并稍微改变了其他一些数据构造函数.特别是,Type'不再包含任何Expr',并且每个人Expr'都确定了它Type'.

最后,问题是:创建两个几乎相同的数据类型集,或尝试将它们统一为单个数据类型是否更好？

保留两个单独的数据类型可以明确表示某些构造函数不再出现.但是,执行常量折叠以评估常量表达式的函数将具有以下类型:

foldConstants :: Expr -> Either String Expr'

但是这意味着我们以后不能用Expr's 执行常量折叠(想象一下操纵一个传递Expr',并想要折叠任何出现的常量表达式).我们需要另一个实现:

foldConstants' :: Expr' -> Either String Expr'

另一方面,保持单一类型可以解决常量折叠问题,但会阻止类型检查器强制执行静态不变量.

此外,在第一次传递期间,我们将什么放入未知字段(如字段偏移,数组大小和表达式类型)？我们可以插上这些洞undefined,或者error "*hole*",但这感觉就像是等待发生的灾难(就像NULL你甚至无法检查的指针).我们可以将未知字段更改为Maybes,然后插入漏洞Nothing(就像NULL我们可以检查的指针一样),但是在后续的传递中,如果必须继续从Maybes总是将s中拉出值,那将会很烦人Just.

Answer 1

希望有更多经验的人会有一个更加优雅,经过实战考验并且准备好的答案,但这是我的目标.

您可以用GADT以相对较低的成本获得馅饼并吃掉其中的一部分:

{-# LANGUAGE GADTs #-}

data P0 -- phase zero
data P1 -- phase one

data Type p where
     TypeInt     :: Id -> Type p
     TypePointer :: Id -> Type p -> Type p             -- target type
     TypeArray   :: Id -> Type p -> Expr p -> Type p   -- elt type, elt count
     TypeStruct  :: Id -> [(String, Type p)] -> Type p -- [(field name, field type)]
     TypeOf      :: Id -> Expr P0 -> Type P0
     TypeDef     :: Id -> Type P0 -> Type P0

data Expr p where
     ExprInt     :: Int -> Expr p                        -- literal int
     ExprVar     :: Var -> Expr p                        -- variable
     ExprSizeof  :: Type P0 -> Expr P0
     ExprUnop    :: Unop -> Expr p -> Expr p
     ExprBinop   :: Binop -> Expr p -> Expr p -> Expr p
     ExprField   :: Bool -> Expr P0 -> String -> Expr P0 -- Bool gives true=>s.field, false=>p->field

这里我们改变的是:

• 数据类型现在使用GADT语法.这意味着构造函数使用其类型签名进行声明.data Foo = Bar Int Char变得data Foo where Bar :: Int -> Char -> Foo(除了语法之外,两者完全等价).

• 我们在两个Type和都添加了一个类型变量Expr.这是一个所谓的幻像类型变量:没有存储类型的实际数据p,它仅用于强制类型系统中的不变量.

• 我们已经声明了虚拟类型来表示转换之前和之后的阶段:阶段0和阶段1.(在具有多个阶段的更复杂的系统中,我们可能使用类型级别的数字来表示它们.)

• GADT让我们在数据结构中存储类型级不变量.这里我们有两个.第一个是递归位置必须与包含它们的结构具有相同的相位.例如,在查看时TypePointer :: Id -> Type p -> Type p,您将a传递Type p给TypePointer构造函数并获得Type p结果,并且这些p必须是相同的类型.(如果我们想允许不同的类型,我们可以使用p和q.)

• 第二个是我们强制执行一些构造函数只能在第一阶段使用的事实.大多数构造函数在幻像类型变量中都是多态的p,但是其中一些构造函数需要它P0.这意味着那些构造只能用来构造类型的值Type P0或Expr P0,而不是任何其他相.

GADT在两个方向上工作.第一个是如果你有一个返回a的函数Type P1,并尝试使用其中一个返回a Type P0来构造它的构造函数,你将得到一个类型错误.这就是所谓的"构造正确":构建无效结构是绝对不可能的(前提是您可以对类型系统中的所有相关不变量进行编码).另一方面,如果你有一个值Type P1,你可以确定它是正确构造的:TypeOf和TypeDef构造函数不能被使用(实际上,如果你尝试对它们进行模式匹配,编译器会抱怨) ,任何递归位置也必须是相位的P1.本质上,当您构建GADT时,您存储了满足类型约束的证据,并且当您对其进行模式匹配时,您将检索该证据并可以利用它.

这很容易.不幸的是,除了允许哪些构造函数之外,我们在两种类型之间存在一些差异:一些构造函数参数在各阶段之间是不同的,而一些仅在转换后阶段存在.我们可以再次使用GADT对其进行编码,但这并不是低成本和优雅的.一种解决方案是复制所有不同的构造函数,并且每个构造函数都有一个P0和P1.但重复并不好.我们可以尝试做得更精细:

-- a couple of helper types
-- here I take advantage of the fact that of the things only present in one phase,
-- they're always present in P1 and not P0, and not vice versa
data MaybeP p a where
     NothingP :: MaybeP P0 a
     JustP    :: a -> MaybeP P1 a

data EitherP p a b where
     LeftP  :: a -> EitherP P0 a b
     RightP :: b -> EitherP P1 a b

data Type p where
     TypeInt     :: Id -> Type p
     TypePointer :: Id -> Type p -> Type p
     TypeArray   :: Id -> Type p -> EitherP p (Expr p) Int -> Type p
     TypeStruct  :: Id -> [(String, MaybeP p Int, Type p)] -> Type p
     TypeOf      :: Id -> Expr P0 -> Type P0
     TypeDef     :: Id -> Type P0 -> Type P0

-- for brevity
type MaybeType p = MaybeP p (Type p)

data Expr p where
     ExprInt     :: MaybeType p -> Int -> Expr p
     ExprVar     :: MaybeType p -> Var -> Expr p
     ExprSizeof  :: Type P0 -> Expr P0
     ExprUnop    :: MaybeType p -> Unop -> Expr p -> Expr p
     ExprBinop   :: MaybeType p -> Binop -> Expr p -> Expr p -> Expr p
     ExprField   :: Bool -> Expr P0 -> String -> Expr P0

这里有一些帮助器类型,我们强制执行一些构造函数参数只能出现在第一阶段(MaybeP)中,而有些在两个阶段(EitherP)之间有所不同.虽然这使我们完全类型安全,但它感觉有点特别,我们仍然需要一直包装和退出MaybePs和EitherPs.我不知道在这方面是否有更好的解决方案.完整的类型安全是一件事:我们可以写,fromJustP :: MaybeP P1 a -> a并确保它是完全和完全安全的.

更新:另一种方法是使用TypeFamilies:

data Proxy a = Proxy

class Phase p where
    type MaybeP  p a
    type EitherP p a b
    maybeP  :: Proxy p -> MaybeP p a -> Maybe a
    eitherP :: Proxy p -> EitherP p a b -> Either a b
    phase   :: Proxy p
    phase = Proxy

instance Phase P0 where
    type MaybeP  P0 a   = ()
    type EitherP P0 a b = a
    maybeP  _ _ = Nothing
    eitherP _ a = Left a

instance Phase P1 where
    type MaybeP  P1 a   = a
    type EitherP P1 a b = b
    maybeP  _ a = Just  a
    eitherP _ a = Right a

以唯一的变化Expr和Type相对以前的版本是,构造函数需要有一个额外的Phase p约束,例如ExprInt :: Phase p => MaybeType p -> Int -> Expr p.

这里,如果类型p的Type或者Expr是已知的,可以静态地知道是否MaybeP旨意是()或类型的给定类型和EitherPs为,可以直接使用它们作为该类型没有明确的解缠.什么时候p不知道你可以使用maybeP和eitherP从Phase课堂上找出它们是什么.(Proxy参数是必要的,因为否则编译器就没有办法告诉你意味着哪个阶段.)这类似于GADT版本,如果p已知,你可以确定什么MaybeP和EitherP包含,否则你有模式匹配两种可能性.这个解决方案并不完美,因为"缺失"的论点变得()而不是完全消失.

构造Exprs和Types似乎在两个版本之间大致相似:如果你正在构造的值具有关于它的任何阶段特定的,那么它必须在其类型中指定该阶段.当你想编写一个多态函数p但仍在处理特定于阶段的部分时,似乎就会遇到麻烦.使用GADT,这很简单:

asdf :: MaybeP p a -> MaybeP p a
asdf NothingP  = NothingP
asdf (JustP a) = JustP a

请注意,如果我只是编写asdf _ = NothingP了编译器就会抱怨,因为输出的类型不能保证与输入相同.通过模式匹配,我们可以确定输入的类型并返回相同类型的结果.

TypeFamilies但是,对于这个版本,这要困难得多.只是使用maybeP和结果Maybe你无法向编译器证明任何类型的东西.您可以通过那里得到一部分的方式,而不必maybeP与eitherP返回Maybe和Either,使他们拆解功能,如maybe和either这也使一种平等可供选择:

maybeP  :: Proxy p -> (p ~ P0 => r) -> (p ~ P1 => a -> r) -> MaybeP p a -> r
eitherP :: Proxy p -> (p ~ P0 => a -> r) -> (p ~ P1 => b -> r) -> EitherP p a b -> r

(请注意,我们需要Rank2Types这个,并注意这些本质上是MaybeP和GADT版本的CPS转换版本EitherP.)

然后我们可以写:

asdf :: Phase p => MaybeP p a -> MaybeP p a
asdf a = maybeP phase () id a

但这仍然不够,因为GHC说:

data.hs:116:29:
 Could not deduce (MaybeP p a ~ MaybeP p0 a0)
 from the context (Phase p)
   bound by the type signature for
              asdf :: Phase p => MaybeP p a -> MaybeP p a
   at data.hs:116:1-29
 NB: `MaybeP' is a type function, and may not be injective
 In the fourth argument of `maybeP', namely `a'
 In the expression: maybeP phase () id a
 In an equation for `asdf': asdf a = maybeP phase () id a

也许你可以用某种类型的签名来解决这个问题,但是在这一点上它似乎比它的价值更麻烦.所以等待来自其他人的进一步信息我将推荐使用GADT版本,更简单,更强大,以一点点语法噪音为代价.

再次更新:这里的问题是因为MaybeP p a是一个类型函数,没有其他信息可以通过,GHC无法知道什么p和a应该是什么.如果我传入Proxy p并使用它而不是phase解决p,但a仍然是未知的.