如何创建一个引入新类型的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

这是错误的,因为这意味着你得到TypedExpr t 任何t你喜欢的.相反,你真正想要的是一种 t由类型的论证决定的特殊情况Expr.

这种推理已经表明你超越了Hindley-Milner型系统的功能.毕竟,返回类型的addTypes应取决于价值的说法,但在普通的Haskell 2010,类型可能不依赖于价值.因此,您需要类型系统的扩展,使您更接近依赖类型.在Haskell中,广义代数数据类型(GADT)可以做到这一点.

有关GADT的第一次介绍,另请参阅我关于GADT的视频.

但是,在熟悉GADT之后,您仍然会遇到将无类型表达式解析为类型化表达式的问题,即编写函数

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

当然,你必须自己进行一些类型检查,但即使这样,也不容易说服Haskell编译器你的类型检查(发生在值级别上)可以提升到类型级别.幸运的是,其他人已经考虑过它,例如在haskell-cafe邮件列表中查看以下消息:

爱德华Kmett.
Re:手动类型检查以提供GADT的读取实例.(是Re:[Haskell-cafe]阅读GATD实例)
http://article.gmane.org/gmane.comp.lang.haskell.cafe/76466

(有没有人知道正式出版/精心编写的参考文献？)