生存型

Question

我已经得到了他们的工作是计算型a WRT类型的某些价值函数的一些最佳值的函数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应该计算最优值WRT val，并在容器的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。

我误解了这种情况下的存在类型？ optimize声明中的forall v是否意味着optimize可能期望从a -> v什么v它想要什么？或者这是否意味着optimize可能对a -> v期待什么，除了Ord v？

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

我设法实现了与一个额外的typeclass，它提供optimize函数与OptiF a v类似的签名，但看起来比使用高阶函数更丑陋。

Answer 1

这是很容易出错的东西。

你在optimize的签名是而不是存在，但一个普遍的。

...因为existentials都有些过时了，无论如何，让您的数据改写为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)，它实际上需要Num实例，并非所有Ord■找。实际上，optimize不应该需要rank2类型：它应该适用于调用者可能给它的任何Ord-v。

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

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

你想要的解决方案是这样的：Container不应该是存在的，要么是！ opti函数应该适用于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)