在Haskell中，两个函数看似相等但有所不同

Question

我正在尝试在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

这是不平等的。

这里是问题。

1. 我认为它具有相同的类型签名，因为在折叠和替换时beq，beq'看起来似乎具有相同的结果。就像有很多方法可以实现一个功能。但事实并非如此。Haskell中有一些秘密规则和语法吗？

2. 如果我想beq使用该函数编写代码not，该如何使其工作？

Answer 1

如何修正编码

教会编码在无类型演算中非常有效。

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

例如，您的代码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上一次String。如果Bool不是多态的，这将失败。

为什么β减少会改变推断的类型

此外，您似乎确信可以在减少之前和之后都可以beta减少Haskell表达式和推断的类型。通常，这是不对的，正如您在实验中发现的那样。要查看原因，这是一个简单的示例：

id1 x = x

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

id2 x = (\ _ -> x) e

请注意，id2beta会降低到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。