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

问：

我有以下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) -> capply_to_f

我最初的猜测是，我也许能够为，使用类型变量来指示此约束。但这似乎行不通。apply_to_f

Haskell 类型推断

为什么需要不太通用（更受限制）的类型？就像现在一样，编译并具有类型。有一些方法可以限制类型，例如自己统一变量，或添加类似的东西，但我想知道理由是什么。apply_to_f f . apply_to_f fapply_to_f id . apply_to_f id :: ((a -> a) -> b) -> (b -> c) -> c(T ~ U) => ...

0赞 Theo H 11/11/2023

似乎应该有一种方法来表达所述的约束（并且有！），而不是自己编写受限制的类型。在教会数字的上下文中，受限制的类型是（理解）函数工作方式的关键——请参阅此处的各种解释：stackoverflow.com/questions/8790249/...pred

1赞 Daniel Wagner 11/12/2023

您可能还喜欢Unifying c -> a -> b 和（a -> b） -> c。

答：

2赞 K. A. Buhr 11/11/2023 #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)

由此产生的类型错误将与定义中的第二个相关联，并将伴随着对第二个定义中预期版本实际类型的明确解释：idfooid

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)

那么类型错误将与定义中的使用相关联，并且会更模糊地与“Foo 推断类型中的某个问题”相关联：apply_to_ffoo

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

上一个：了解 Web.Scotty 流

下一个：如何使用定点来覆盖 nixpkgs 包？

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

Telling Haskell compiler that two types are compatible

评论