希望有更多经验的人会有一个更完善、经过实战考验和准备好的答案，但这是我的看法。
使用 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，它仅用于强制类型系统中的不变量。
我们已经声明了虚拟类型来表示转换之前和之后的阶段：阶段零和阶段一。（在具有多个阶段的更复杂的系统中，我们可能会使用类型级别的数字来表示它们。）
GADT 让我们可以在数据结构中存储类型级别的不变量。这里我们有两个。首先是递归位置必须与包含它们的结构处于同一阶段。例如，查看TypePointer :: Id -> Type p -> Type p，您将 a 传递Type p给TypePointer构造函数并得到 aType p作为结果，并且这些ps 必须是相同的类型。（如果我们想允许不同的类型，我们可以使用pand q。）
第二个是我们强制执行某些构造函数只能在第一阶段使用的事实。大多数构造函数在幻像类型变量中是多态的p，但其中一些要求它是多态的P0。这意味着这些构造函数只能用于构造Type P0or类型的值Expr P0，而不能用于构造任何其他阶段。
GADT 有两个方向。第一个是如果你有一个返回 a 的函数Type P1，并尝试使用一个返回 a 的构造函数Type P0来构造它，你会得到一个类型错误。这就是所谓的“通过构造正确”：构造无效结构在静态上是不可能的（前提是您可以对类型系统中的所有相关不变量进行编码）。它的另一面是，如果你有一个值Type P1，你可以确定它是正确构造的：TypeOf和TypeDef构造函数不能被使用（事实上，如果你尝试对它们进行模式匹配，编译器会抱怨） ，并且任何递归位置也必须是相位的P1. 本质上，当您构建 GADT 时，您存储了满足类型约束的证据，并且当您对其进行模式匹配时，您检索该证据并可以利用它。
那是容易的部分。不幸的是，除了允许的构造函数之外，我们在这两种类型之间还有一些差异：一些构造函数参数在不同阶段之间是不同的，而一些只存在于转换后阶段。我们可以再次使用 GADT 对其进行编码，但它不是低成本和优雅的。一种解决方案是复制所有不同的构造函数，并且每个构造函数都有一个 forP0和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.
在这里，如果paType中的类型Expr已知，您可以静态地知道MaybePs 将是()还是给定类型以及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和eitherPreturn Maybeand ，使它们成为像and这样的Either解构函数，这也使类型相等可用：maybeeither
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要这样做，还要注意这些本质上是 和 的 GADT 版本的 CPS 转换版本MaybeP。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是什么。如果我传入 aProxy p并使用它而不是phase那个解决方案p，但a仍然未知。