haskell - 为什么通过存在和约束进行子类型不起作用？

Question

我一直在尝试了解 Haskell 如何处理子类型，因此我想出了以下代码片段:

{-# LANGUAGE RankNTypes #-}

f1 :: () -> Int
f1 _ = 5

f2 :: () -> (forall a. Integral a => a)
f2 = f1

行 f2 = f1 失败并出现意外错误消息:

Couldn't match type ‘a’ with ‘Int’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      f2 :: forall a. Integral a => () -> a

似乎存在主义已被提升为普遍性，这当然是无意的。

我的猜测是，在实现方面f2需要返回一个值和相应的字典，而f1只返回一个Int类型的值>。然而，从逻辑角度来看，f2 的契约是“从 () 到 Integral 的某个未知实例的函数”，而 f1 完美满足。

GHC 应该做一些隐含的魔法来使其发挥作用还是我错过了一些东西？

Answer 1

f2 中的 a 类型是通用量化的，而不是存在量化的。 GHC 不直接支持您正在寻找的存在类型。

但是，您可以通过将其包装在新的数据类型中来获得类似的结果:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ConstraintKinds           #-}

data Constrained c = forall a. c a => Constrained a

f1 :: () -> Int
f1 _ = 5

f2 :: () -> Constrained Integral
f2 unit = Constrained (f1 unit)

现在，这通常不是很有用，因为我们已经完成了所有关于 f2 () 的(类型)信息，除了它的类型是 积分。您不再知道它是一个Int。也可以跟踪这些信息，但这可能有用也可能没用，具体取决于您正在做什么。

了解您正在做的事情以及您想要查看的内容的更多背景信息将使我更容易确定应该添加有关此类事物的信息。

附带说明:没有必要将它们放入带有参数的函数中。您可以只使用 f1::Int 和 f2::Constrained Integral。

另外，如果我没有提到这一点，我会觉得有点疏忽，尽管在这个答案的前面，I wrote an answer that describes some potentially practical uses for constrained existential types 淡化了 Haskell 中这些类型的实用性。 。虽然我们对这个主题有所了解，但可能还值得指出 ConstraintKinds 是一个强大的扩展，它的用途不仅仅是受约束的存在。