【问题标题】：Two functions seem equal but different in Haskell在 Haskell 中，两个函数看起来相等但不同
【发布时间】：2019-05-12 12:28:30
【问题描述】：

我正在尝试在 Haskell 中实现没有 Prelude 的布尔值。

当表达式，beq true true "TRUE" "FALSE" 被评估时，没关系。但是当我尝试评估 beq' true true "TRUE" "FALSE" 时，它会因预期类型和实际类型之间的一些差异而失败。

这是代码。

import qualified Prelude as P

i = \x -> x
k = \x y -> x
ki = k i

true = k
false = ki

not = \p -> p false true
beq = \p q -> p (q true false) (q false true)
beq' = \p q -> p q (not q)

所以我检查了论文的推断类型。

*Main> :type beq
beq
  :: (t1 -> t1 -> t2)
     -> ((p1 -> p1 -> p1) -> (p2 -> p2 -> p2) -> t1) -> t2

*Main> :type beq'
beq'
  :: (((p1 -> p2 -> p2) -> (p3 -> p4 -> p3) -> t1) -> t1 -> t2)
     -> ((p1 -> p2 -> p2) -> (p3 -> p4 -> p3) -> t1) -> t2

而且不相等。

这里有问题。

我认为它具有相同的类型签名，因为 beq 和 beq' 在折叠和替换时似乎产生相同的结果。就像有很多方法可以实现一个功能一样。但事实并非如此。 Haskell 中是否有一些秘密规则和语法？
如果我想用函数not写beq，我怎样才能让它工作？

【问题讨论】：

我不清楚为什么您认为它们应该具有相同的类型，因为它们具有完全不同的实现。也许您应该分享您认为 GHCi 报告错误的类型，以及您认为该类型应该是什么 - 连同您的推理 - 然后我们可以帮助您解释您的错误所在。

标签： haskell type-inference lambda-calculus

【解决方案1】：

如何修复编码

Church 编码在无类型演算中效果很好。

添加类型后，事情变得更加复杂。例如，对于简单类型，编码会丢失。如果支持更高的等级，则可以使用多态性来恢复它们。请注意，类型推断不适用于高级类型，因此需要一些显式类型注释。

例如，您的not 应写为：

{-# LANGUAGE RankNTypes #-}
type ChBool = forall a. a -> a -> a

not :: ChBool -> ChBool
not f x y = f y x

将布尔值建模为多态函数很重要，否则它们只能用于单一类型，导致许多示例失败。例如，考虑

foo :: Bool -> (Int, String)
foo b = (b 3 2, b "aa" "bb")

这里b需要使用两次，一次在Ints上，一次在Strings上。如果Bool 不是多态的，这将失败。

为什么 beta-reduction 会改变推断类型

此外，您似乎确信您可以对 Haskell 表达式进行 beta 归约，并且归约前后的推断类型必须相同。一般来说，正如您在实验中发现的那样，这不是真的。要了解原因，这里有一个简单的例子：

id1 x = x

这里推断的类型显然是id1 :: forall a. a -> a。请考虑这个变体：

id2 x = (\ _ -> x) e

请注意，id2 beta-reduce 为 id1，无论e 可能是什么。但是，通过仔细选择e，我们可以限制x 的类型。例如。让我们选择e = x "hello"

id2 x = (\ _ -> x) (x "hello")

现在，推断类型是id2 :: forall b. (String -> b) -> String -> b，因为x 只能是String-accepting 函数。 e 不会被评估无关紧要，类型推断算法无论如何都会使其类型良好。这使得id2 的推断类型与id1 的类型不同。

【讨论】：