GADT用于多态列表

Question

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

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

这是非常期待的.我该如何解决这个问题？我知道我可以通过打破所有候选类型的类型来解决它,但是没有更简洁的方法吗？

Answer 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)

这称为存在量化.然后您可以PPair使用SomeExpr以下方法重写:

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包; 你可以Key从ST和构造s IO,并Vault用作异构容器.它基本上就像一个Map键包含相应值的类型.具体来说,我建议定义Var a为Key (Expr a)和使用Vault而不是你的[PPair].(完全披露:我已经参与了金库包.)

当然,您仍然需要将变量名称映射到Key值,但是您可以Key在解析后立即创建所有s,并携带它们而不是字符串.(但是,Var使用此策略从a 到相应的变量名称会有一些工作;您可以使用存在列表来执行此操作,但解决方案太长而无法提供此答案.)

(顺便说一句,你可以使用GADT为数据构造函数提供多个参数,就像常规类型一样:data PPair where PPair :: String -> Expr a -> PPair.)