高阶函数中的存在类型

Question

我有一个函数,它的工作是计算类型的a某些值函数的类型的最佳值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.

在这种情况下,我是否误解了存在主义类型？是否forall v在声明optimize是否意味着optimize可以期望从a -> v任何v就是了？或者它是否意味着除了那之外optimize可能没什么可期待的？a -> vOrd v

我想要的OptiF a v是没有任何固定v,因为我想a -> v稍后插入一些.我想要强加的唯一限制是Ord v.是否有可能使用存在类型(或其他)表达类似的东西？

我设法通过一个额外的类型类来实现它,它提供了一个optimize具有类似签名的函数OptiF a v,但这对我来说比使用高阶函数更加丑陋.

Answer 1

这很容易出错.

你在签名中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),它实际上需要一个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)