haskell - 反转对的棘手类型签名

Question

假设我有以下数据类型:

data D a b = D (a,b) (b,a)

我想在上面定义以下函数:

apply f (D x y) = D (f x) (f y)

apply 的类型签名是什么？

以下是一些 f 的示例，这些示例都可以:

f :: a -> a -- OK
f :: (a, b) -> (b, a) -- OK
f :: (a, b) -> ((a, c), (b, c)) -- OK

在上述所有情况下，我们最终得到一个有效的类型 D。

但这不行:

f :: (a, b) -> (a, a)

因为当我们通过 apply 发送这样的函数时，我们最终不得不尝试构造 D (a,a) (b,b) ，除非它是无效的a = b。

我似乎无法找出一个类型签名来表达这一切？另外，一般来说，有没有办法让 GHC 告诉我这些签名应该是什么？

键入的孔编辑:

为了尝试使用键入的孔查找类型，我尝试了以下操作:

x = apply _ (D (1::Int,'a') ('b',2::Int))

得到:

Found hole ‘_’ with type: (Int, Int) -> (b, b)
Where: ‘b’ is a rigid type variable bound by
           the inferred type of x :: D b b

在我看来这是无稽之谈，因为 f::(Int, Int) -> (b, b) 显然在这里不起作用。

Answer 1

多种类型适合apply，但推断出的((t, t) -> (b, b)) -> D t t -> D b b是最多的明智且可用的一款。替代方案的级别将更高，因此让我们启用该语言扩展:

{-# LANGUAGE RankNTypes #-}

首先，我们可以让apply id工作:

apply :: (forall a. a -> a) -> D a b -> D a b
apply f (D x y) = D (f x) (f y)

但是，现在 id 是 apply 可以使用的唯一函数(forall a. a - 类型的所有总函数) > a 等于id)。

这是另一种类型:

apply :: (forall a. a -> (c, c)) -> D a b -> D c c
apply f (D x y) = D (f x) (f y)

但这也是有代价的。现在，f-s 只能是忽略 D 之前字段的常量函数。所以 apply (const (0, 0)) 可以工作，但我们无法检查 f 的参数。

相比之下，推断类型非常有用。我们可以用它来表达转换，查看 D 中包含的实际数据。

此时，我们可能会问:为什么 GHC 会推断出它所推断的内容？毕竟，某些函数适用于替代类型，但不适用于默认类型。有时推断更高级别的类型会更好吗？嗯，这样的类型通常非常有用，但推断它们是不可行的。

Rank-2 类型的类型推断相当复杂，而且也不是很实用，因为不可能推断出最通用的类型。通过 Rank-1 推断，我们可以推断出比同一表达式的所有其他有效类型更通用的类型。 2 级类型没有这样的保证。而对于 3 级及以上类型的推理只是 undecidable 。

由于这些原因，GHC 坚持 1 级推理，因此它永远不会在函数参数内使用 forall-s 来推断类型。