haskell - 如何创建一个引入新类型的 Haskell 函数？

Question

我目前正在编写一个表达式解析器。我已经完成了词法和句法分析，现在正在检查类型。我在数据结构中有这样的表达式(简化版本):

data Expr = EBinaryOp String Expr Expr
          | EInt Int
          | EFloat Float

现在我需要一个函数将其转换为新类型，例如 TypedExpr，它也包含类型信息。现在我的主要问题是，这种类型应该是什么样子。我有两个想法 - 使用类型参数:

data TypedExpr t = TEBinaryOp (TBinaryOp a b t) (TExpr a) (TExpr b)
                 | TEConstant t
addTypes :: (ExprType t) => Expr -> TypedExpr t

或没有:

data TypedExpr = TEBinaryOp Type BinaryOp TypedExpr TypedExpr
               | TEConstant Type Dynamic
addTypes :: Expr -> TypedExpr

我从第一个选项开始，但遇到了问题，因为这种方法假设您在解析表达式之前知道表达式的类型(对我来说，在大多数情况下都是如此，但并非总是如此)。不过，我喜欢它，因为它让我可以使用 Haskell 的类型系统并在编译时检查大多数错误。

可以使用第一个选项吗？
你会选哪一个？为什么？
每个选项都会出现什么问题？

Answer 1

函数的类型

addTypes :: Expr -> TypedExpr t

是错误的，因为这意味着您将获得您喜欢的任何 t 的 TypedExpr t 。相反，您真正想要的是一个特定的 t，它由 Expr 类型的参数确定。

这个推理已经表明您超出了 Hindley-Milner 类型系统的能力。毕竟，addTypes 的返回类型应该取决于参数的值，但在普通的 Haskell 2010 中，类型可能不依赖于值。因此，您需要类型系统的扩展，使您更接近依赖类型。在 Haskell 中，广义代数数据类型 (GADT) 可以做到这一点。

有关 GADT 的初步介绍，另请参阅 my video on GADTs .

但是，熟悉 GADT 后，您仍然面临将非类型化表达式解析为类型化表达式的问题，即编写函数

addTypes :: Expr -> (exists t. TypedExpr t)

当然，你必须自己执行一些类型检查，但即便如此，要让 Haskell 编译器相信你的类型检查(发生在值级别)可以提升到类型级别也不容易。幸运的是，其他人已经考虑过这个问题，例如，请参阅 haskell-cafe 邮件列表中的以下消息:

Edward Kmett.
Re: Manual Type-Checking to provide Read instances for GADTs. (was Re: [Haskell-cafe] Read instance for GATD)
http://article.gmane.org/gmane.comp.lang.haskell.cafe/76466

(有人知道正式发布/写得很好的引用文献吗？)