10

我有一个函数，它的工作是计算一些类型的最佳值awrt 一些类型的值函数a -> v

type OptiF a v = (a -> v) -> a

然后我有一个容器想要将这样的函数与另一个使用值的函数一起存储：

data Container a = forall v. (Ord v) => Cons (OptiF a v) (a -> Int)

这个想法是，任何实现类型函数的人OptiF a v都不应该被它的细节所困扰，v除非它是Ord.

所以我写了一个函数，它接受这样一个值函数和一个容器。使用OptiF a v它应该计算出最佳值 wrtval并将其插入容器的result函数中：

optimize :: (forall v. (Ord v) => a -> v) -> Container a -> Int
optimize val (Cons opti result) = result (opti val)

到目前为止一切顺利，但我不能打电话optimize，因为

callOptimize :: Int
callOptimize = optimize val cont
   where val = (*3)
         opti val' = if val' 1 > val' 0 then 100 else -100
         cont = Cons opti (*2)

不编译：

Could not deduce (v ~ Int)
from the context (Ord v)
  bound by a type expected by the context: Ord v => Int -> v
  at bla.hs:12:16-32
  `v' is a rigid type variable bound by
      a type expected by the context: Ord v => Int -> v at bla.hs:12:16
Expected type: Int
  Actual type: Int
Expected type: Int -> v
  Actual type: Int -> Int
In the first argument of `optimize', namely `val'
In the expression: optimize val cont

第 12:16-32 行在哪里optimize val cont。

在这种情况下，我是否误解了存在类型？forall v声明中的optimize意思是否可以optimize期望得到它想要的a -> v任何东西？v或者这是否意味着除此之外optimize可能没有任何期望？a -> vOrd v

我想要的是OptiF a vany 不是固定的v，因为我想a -> v稍后插入一些。我想施加的唯一约束是Ord v. 甚至可以使用存在类型（或其他）来表达类似的东西吗？

我设法通过一个额外的类型类来实现这一点，它提供了optimize一个与OptiF a v.

4

1 回答 1

12

这是很容易出错的事情。

你所拥有的optimize不是存在主义的，而是普遍的。

...因为存在主义无论如何都有些过时了，让我们将您的数据重写为 GADT 形式，这样可以更清楚地说明这一点，因为语法与多态函数基本相同：

data Container a where
  (:/->) :: Ord v =>                       -- come on, you can't call this `Cons`!
     OptiF a v -> (a->Int) -> Container a

观察Ord约束（这意味着这里是forall v...）位于类型变量参数化函数签名之外，即v当我们想要构造一个Container值时，我们可以从外部指定一个参数。换句话说，

对于所有v存在的构造Ord 函数(:/->) :: OptiF a v -> (a->Int) -> Container a

这就是“存在类型”这个名字的由来。同样，这类似于普通的多态函数。

另一方面，在签名

optimize :: (forall v. (Ord v) => a -> v) -> Container a -> Int

您有一个forall内部签名术语本身，这意味着v可能采用的具体类型将由被调用者,optimize内部决定——我们从外部控制的只是它在Ord. 没有什么是“存在的”，这就是为什么这个签名实际上不会单独编译XExistentialQuantification或XGADTs单独编译：

<interactive>:37:26:
    Illegal symbol '.' in type
    Perhaps you intended -XRankNTypes or similar flag
    to enable explicit-forall syntax: forall <tvs>. <type>

val = (*3)显然不满足(forall v. (Ord v) => a -> v)，它实际上需要一个并非所有s 都有的Num实例。Ord事实上，optimize不应该需要 rank2 类型：它应该适用于调用者可能给它的任何Ord类型。v

optimize :: Ord v => (a -> v) -> Container a -> Int

但是，在这种情况下，您的实现不再起作用：因为(:/->)它实际上是一个存在构造函数，它只需要包含任何 OptiF函数，对于某些未知类型v1。因此，optimize 的调用者可以自由选择针对任何特定类型的 opti 函数，以及针对任何其他可能的固定类型优化的函数——这是行不通的！

您想要的解决方案是：Container也不应该是存在的！opti-function 应该适用于 in 中的任何类型Ord，而不仅仅是一种特定类型。好吧，作为 GADT，这看起来与您最初拥有的通用量化签名大致相同optimize：

data Container a where
  (:/->) :: (forall v. Ord v => OptiF a v) -> (a->Int) -> Container a

现在，优化工作

optimize :: Ord v => (a -> v) -> Container a -> Int
optimize val (opti :/-> result) = result (opti val)

并且可以随心所欲地使用

callOptimize :: Int
callOptimize = optimize val cont
   where val = (*3)
         opti val' = if val' 1 > val' 0 then 100 else -100
         cont = opti :/-> (*2)
于 2013-02-28T02:22:26.233 回答