多态列表的 GADT答案

【问题标题】：GADT for polymorphic list多态列表的 GADT
【发布时间】：2012-01-20 17:31:25
【问题描述】：

我正在解析表单的一些语句

v1 = expression1
v2 = expression2
...

我正在使用 State Monad，我的状态应该是一对 (String, Expr a)，我真的坚持要输入表达式。我尝试将状态实现为 [PPair]，在其中我通过 GADT 定义 PPair：

data PPair where
    PPair :: (String, Expr a) -> PPair

当这行代码通过编译器时，我觉得我做的事情真的很不对劲。我抑制住了这个想法，继续编码。当我开始编写从 State 中提取变量值的代码时，我意识到了问题：

evalVar k ((PPair (kk, v)):s) = if k == kk then v else evalVar k s

我明白了：

Inferred type is less polymorphic than expected

这是意料之中的。我该如何解决这个问题？我知道我可以通过将类型分解为所有候选类型 a 来解决它，但是没有更简洁的方法吗？

【问题讨论】：

标签： haskell gadt

【解决方案1】：

问题是evalVar 不可能有这样的类型：

evalVar :: String -> [PPair] -> Expr ?

你不能说? 是a，因为你声称你的返回值适用于a 的任何值。但是，您可以将“具有未知类型的Expr”包装到它自己的数据类型中：

data SomeExpr where
  SomeExpr :: Expr a -> SomeExpr

或者，等效地，使用RankNTypes 而不是GADTs：

data SomeExpr = forall a. SomeExpr (Expr a)

这称为存在量化。然后您可以使用SomeExpr 重写PPair：

data PPair = PPair String SomeExpr

evalVar 解决了：

evalVar k (PPair kk v : xs)
  | k == kk = v
  | otherwise = evalVar k xs

（当然，您可以只使用[(String,SomeExpr)] 和标准的lookup 函数。）

不过，一般来说，像这样在 Haskell 级别保持表达式完全键入可能是徒劳的；像Agda 这样的依赖类型语言不会有任何问题，但是您最终可能会遇到 Haskell 无法很快完成的事情，或者将事情削弱到您想要的编译时安全性的地步努力就白费了。

当然，这并不是说它永远不会起作用；类型语言是 GADT 的激励示例之一。但它可能不会像你想要的那样工作，如果你的语言有任何重要的类型系统特性，比如多态，你可能会遇到麻烦。

如果你真的想保持打字，那么我会使用比字符串更丰富的结构来命名变量；有一个 Var a 明确携带该类型的类型，如下所示：

data PPair where
  PPair :: Var a -> Expr a -> PPair

evalVar :: Var a -> [PPair] -> Maybe (Expr a)

实现与此类似的一个好方法是使用vault 包；您可以从ST 和IO 构造Keys，并将Vault 用作异构容器。它基本上就像一个Map，其中的键保存相应值的类型。具体来说，我建议将Var a 定义为Key (Expr a) 并使用Vault 而不是[PPair]。（完全披露：我已经研究过 Vault 包。）

当然，您仍然需要将变量名称映射到 Key 值，但您可以在解析后立即创建所有 Keys，并携带它们而不是字符串。（不过，使用这种策略从Var 到其对应的变量名需要做一些工作；您可以使用存在列表来完成，但解决方案太长，无法放入此答案。）

（顺便说一句，您可以使用 GADT 为数据构造函数提供多个参数，就像常规类型一样：data PPair where PPair :: String -> Expr a -> PPair。）

【讨论】：

很好的答案，像往常一样......谢谢！