告诉 Haskell 编译器两种类型是兼容的

Question

我有以下 Haskell 函数：

apply_to_f :: (a -> a) -> ((a -> a) -> b) -> ((b -> c) -> c)
apply_to_f f = \ g -> \ h -> h (g f)

（这来自教堂数字的“pred”函数）。

我想告诉编译器一个约束：可以将

(apply_to_f f)

与自身组合。

换句话说，

(apply_to_f f)

采用

(a -> a) -> a

类型的函数，并且还返回

(a -> a) -> a

类型的函数。

那么是否可以告诉编译器需要将

(a -> a) -> b

和

(b -> c) -> c

统一为

apply_to_f

的类型，或者如果我想写出精确的类型，我是否必须自己弄清楚这一点功能？

我最初的猜测是，我也许可以为

apply_to_f

编写一个模糊类型，使用类型变量来指示此约束。但这似乎不起作用。

Answer 1

有几种可能性。首先，您可以将额外的约束表示为类型相等：

apply_to_f :: ((a -> a) -> b) ~ ((b -> c) -> c)
  => (a -> a) -> ((a -> a) -> b) -> ((b -> c) -> c)

请注意，生成的类型签名不完全等同于：

apply_to_f :: (a -> a) -> ((a -> a) -> a) -> ((a -> a) -> a)

特别是，GHCi 会为这两种类型签名报告不同的类型，如果在“错误类型”处使用

apply_to_f

，则报告的错误将会不同。例如，以下代码类型检查：

apply_to_f :: (a -> a) -> ((a -> a) -> b) -> ((b -> c) -> c)
apply_to_f f = \ g -> \ h -> h (g f)

foo = apply_to_f id id

如果您使用直接类型签名限制

apply_to_f

的类型：

apply_to_f :: (a -> a) -> ((a -> a) -> a) -> ((a -> a) -> a)

产生的类型错误将与

id

定义中的第二个

foo

相关联，并附有对该第二个

id

的预期版本实际类型的清晰解释：

Unify.hs:13:21-22: error:
    • Couldn't match type ‘a’ with ‘a -> a’
      Expected: (a -> a) -> a
        Actual: (a -> a) -> a -> a
      ‘a’ is a rigid type variable bound by
        the inferred type of foo :: (a -> a) -> a
        at Unify.hs:13:1-22
    • In the second argument of ‘apply_to_f’, namely ‘id’
      In the expression: apply_to_f id id
      In an equation for ‘foo’: foo = apply_to_f id id
    • Relevant bindings include
        foo :: (a -> a) -> a (bound at Unify.hs:13:1)
   |
13 | foo = apply_to_f id id
   |                     ^^

如果你使用约束来代替：

apply_to_f :: ((a -> a) -> b) ~ ((b -> c) -> c)
  => (a -> a) -> ((a -> a) -> b) -> ((b -> c) -> c)

那么类型错误将与

apply_to_f

定义中

foo

的使用相关联，并将更模糊地与“foo 推断类型中的某些问题”相关联：

Unify.hs:12:7-16: error:
    • Couldn't match type ‘a’ with ‘a -> a’
        arising from a use of ‘apply_to_f’
      ‘a’ is a rigid type variable bound by
        the inferred type of foo :: ((a -> a) -> a -> a) -> a -> a
        at Unify.hs:12:1-22
    • In the expression: apply_to_f id id
      In an equation for ‘foo’: foo = apply_to_f id id
    • Relevant bindings include
        foo :: ((a -> a) -> a -> a) -> a -> a (bound at Unify.hs:12:1)
   |
12 | foo = apply_to_f id id
   |       ^^^^^^^^^^

尽管如此，我认为这两个签名之间的差异在大多数情况下可能只是表面上的，并且出于实际目的，它们的行为应该大致相同。

其次，您可以通过强制类型检查器键入需要约束的检查表达式，利用类型检查器来计算

apply_to_f

所需的类型。例如，定义：

apply_to_f = general_apply_to_f
  where general_apply_to_f :: (a -> a) -> ((a -> a) -> b) -> ((b -> c) -> c)
        general_apply_to_f f = \ g -> \ h -> h (g f)

        _ = apply_to_f undefined . apply_to_f undefined

将导致

apply_to_f

的类型被正确推断为：

λ> :t apply_to_f
apply_to_f :: (a -> a) -> ((a -> a) -> a) -> (a -> a) -> a