3

我一直在尝试了解 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只返回一个 type 的值Int。然而，从逻辑的角度来看，契约f2是“一个来自()某个未知实例的函数Integral”并且f1完美地满足了它。

GHC 应该做一些隐含的魔法来让它工作还是我错过了什么？

4

2 回答 2

6

a您拥有的类型f2是普遍量化的，而不是存在量化的。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 ()除了它的类型是Integral. 你不再知道它是一个Int. 也可以跟踪此信息，但这可能有用也可能没有用，具体取决于您在做什么。

更多关于您正在做的事情和您希望看到的内容的背景信息将使我应该添加关于这些事情的哪些类型的信息变得更容易。

作为旁注：没有必要将它们变成带参数的函数。你可以只拥有f1 :: Intand f2 :: Constrained Integral。

另外，如果我没有提到这一点，我会感到有点失职，尽管在这个答案的早些时候淡化了这些类型在 Haskell 中的效用，但我写了一个答案，描述了 受约束的存在类型的一些潜在实际用途。虽然我们对这个主题有所了解，但可能还值得指出的是，这ConstraintKinds是一个强大的扩展，它的用途不仅仅是受约束的存在。

于 2017-08-17T19:20:34.263 回答
5

您正在阅读f2错误方式的类型。

的类型f2说“如果你给我一个()，我会给你一个(forall a. Integral a => a)。也就是说，f2承诺给你一个可以使用的值，就好像它是任何类型的成员一样Integral。

然而，实现f2说它将通过简单地调用来实现这一点f1。但f1只有回报Int！这确实是 的成员Integral，但它不能用作任何属于 的成员的类型Integral。

实际上，类型f1实际上是f2's 类型的子类型，而不是相反！这实际上有效：

{-# LANGUAGE RankNTypes #-}

f1 :: () -> Int
f1 = f2

f2 :: () -> (forall a. Integral a => a)
f2 _ = 5

它之所以有效，是因为数字文字是多态的，所以 a5可以是任何Num类型（并且Num是 的超类Integral，所以如果它可以是 anyNum它也可以是 any Integral）。f1然后调用f2请求Int作为a.

您注意到 GHC 似乎正在将您写入的类型转换为f2 :: forall a. Integral a => () -> a，您是对的；它实际上确实使您写入该类型的内容正常化。原因是这两种类型实际上与 GHC 类型系统的工作方式相同。调用者实例化在整个类型上量化的任何类型变量f2，调用者也将是接收返回值的人，因此实例化仅在返回值上量化的任何类型变量。forall如果在整个类型或函数的返回类型上作用域，则引入类型变量是相同的；只有当它的范围在箭头的左侧（这是更高级别的类型出现的地方）时，它才会有所不同。

于 2017-08-18T08:16:58.330 回答