5

我正在解析表格的一些陈述

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 来解决它，但是没有更简洁的方法吗？

4

1 回答 1

9

问题是没有可能的类型evalVar可以有：

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

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

data SomeExpr where
  SomeExpr :: Expr a -> SomeExpr

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

data SomeExpr = forall a. SomeExpr (Expr a)

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

data PPair = PPair String SomeExpr

并evalVar解决：

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

（当然，您可以只使用 a[(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包；您可以从and构造Keys ，并将其用作异构容器。它基本上就像键保存相应值的类型的地方。具体来说，我建议定义为并使用 a而不是你的. （完全披露：我已经研究过 Vault 包。）STIOVaultMapVar aKey (Expr a)Vault[PPair]

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

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

于 2012-01-20T17:36:01.510 回答