`foldr` 或其他高阶函数的通用性

Question

这是一个简单的函数，它接受一个列表和一个数字，并计算列表的长度是否大于该数字。

例如

compareLengthTo [1,2,3] 3 == EQ
compareLengthTo [1,2] 3 == LT
compareLengthTo [1,2,3,4] 3 == GT
compareLengthTo [1..] 3 == GT

注意它有两个属性：

它适用于无限列表。
它是尾递归的，使用常量space。

import Data.Ord

compareLengthTo :: [a] -> Int -> Ordering
compareLengthTo l n = f 0 l
  where
    f c [] = c `compare` n
    f c (l:ls) | c > n = GT
               | otherwise = f (c + 1) ls

有没有办法只使用 foldr 来写 compareLengthTo？

请注意，这是使用 drop 的 compareLengthTo 版本：

compareLengthToDrop :: [a] -> Int -> Ordering
compareLengthToDrop l n = f (drop n (undefined:l))
  where
    f [] = LT
    f [_] = EQ
    f _ = GT

我想另一个问题是，你能用 foldr 来实现 drop 吗？

Answer 1

根据定义，foldr 不是尾递归的：

-- slightly simplified
foldr :: (a -> r -> r) -> r -> ([a] -> r)
foldr cons nil []     = nil
foldr cons nil (a:as) = cons a (foldr cons nil as)

所以你无法达到那个目的。也就是说，foldr 的语义有一些吸引人的组成部分。特别是 "productive" 允许用 foldr 编写的折叠在懒惰时表现得很好。

我们可以看到 foldr 说明如何一次分解（催化）一个列表 "layer"。如果 cons 参数可以 return 而不关心列表的任何其他层，那么它可以提前终止并且我们避免检查列表的更多尾部---这就是 foldr 有时可以不严格地行动。

你的函数，处理无限列表，做一些类似于数字参数的事情。我们想对该参数进行操作 "layer by layer"。为了更清楚地说明这一点，让我们将自然数定义如下

data Nat = Zero | Succ Nat

现在 "layer by layer" 更清楚地表示 "counting down to zero"。我们可以像这样将这个概念形式化：

foldNat :: (r -> r) -> r -> (Nat -> r)
foldNat succ zero Zero = zero
foldNat succ zero (Succ n) = succ (foldNat succ zero n)

现在我们可以定义一些类似于我们正在寻找的东西

compareLengthTo :: Nat -> [a] -> Ordering
compareLengthTo = foldNat succ zero where
  zero :: [a] -> Ordering
  zero [] = EQ  -- we emptied the list and the nat at the same time
  zero _  = GT  -- we're done with the nat, but more list remains

  succ :: ([a] -> Ordering) -> ([a] -> Ordering)
  succ continue []     = LT  -- we ran out of list, but had more nat
  succ continue (_:as) = continue as -- keep going, both nat and list remain

可能需要一些时间来研究以上内容以了解其工作原理。特别要注意的是，我将 r 实例化为函数、[a] -> Ordering。上面函数的形式是 "recursion on the natural numbers" 并且它允许它接受无限列表只要 Nat 参数不是...

 infinity :: Nat
 infinity = Succ infinity

现在，上面的函数适用于这个奇怪的类型，Nat，它对非负整数进行建模。我们可以通过将 foldNat 替换为 foldInt 将相同的概念翻译成 Int，类似地写成：

foldInt :: (r -> r) -> r -> (Int -> r)
foldInt succ zero 0 = zero
foldInt succ zero n = succ (foldInt succ zero (n - 1))

你可以验证它体现了与 foldNat 完全相同的模式，但避免使用笨拙的 Succ 和 Zero 构造函数。如果我们给它负整数，您还可以验证 foldInt 是否表现得不正常……这正是我们所期望的。

Answer 2

开始吧（注意：我只是更改了一个比较，这让它变得更懒惰）：

compareLengthTo :: [a] -> Int -> Ordering
compareLengthTo l n = foldr f (`compare` n) l 0
  where
    f l cont c | c >= n = GT
               | otherwise = cont $! c + 1

这使用了与 foldl 中 foldr 完全相同的技术。有一篇关于通用技术的经典文章叫做A tutorial on the universality and expressiveness of fold. You can also see a step-by-step explanation I wrote on the Haskell Wiki。

为了让您开始，请注意 foldr 被应用于此处的四个个参数，而不是通常的三个。这是可行的，因为被折叠的函数需要三个参数，而“基本情况”是一个函数，(`compare` n).

编辑

如果你想像 J. Abrahamson 一样使用惰性 Peano 数字，你可以倒数而不是倒数。

compareLengthTo :: [a] -> Nat -> Ordering
compareLengthTo l n = foldr f final l n
  where
    f _ _ Zero = GT
    f _ cont (Succ p) = cont p

    final Zero = EQ
    final _ = LT

Answer 3

必须参加本次编程比赛：

"Prelude":

import Test.QuickCheck
import Control.Applicative

compareLengthTo :: [a] -> Int -> Ordering
compareLengthTo l n = f 0 l
  where
    f c [] = c `compare` n
    f c (l:ls) | c > n = GT
               | otherwise = f (c + 1) ls

我第一次尝试写这个

compareLengthTo1 :: [a] -> Int -> Ordering
compareLengthTo1 l n = g $ foldr f (Just n) l
  where
    -- we go below zero
    f _ (Just 0) = Nothing
    f _ (Just n) = Just (n - 1)
    f _ Nothing  = Nothing
    g (Just 0) = EQ
    g (Just _) = LT
    g Nothing  = GT

它适用于有限参数：

prop1 :: [()] -> NonNegative Int -> Property
prop1 l (NonNegative n) = compareLengthTo l n === compareLengthTo1 l n

-- >>> quickCheck prop1
-- +++ OK, passed 100 tests.

但它对无限列表无效。为什么？

让我们使用 peano naturals 定义一个变体：

data Nat = Zero | Succ Nat

foldNat :: (r -> r) -> r -> (Nat -> r)
foldNat succ zero Zero = zero
foldNat succ zero (Succ n) = succ (foldNat succ zero n)

natFromInteger :: Integer -> Nat
natFromInteger 0 = Zero
natFromInteger n = Succ (natFromInteger (n - 1))

natToIntegral :: Integral a => Nat -> a
natToIntegral = foldNat (1+) 0

instance Arbitrary Nat where
  arbitrary = natFromInteger . getNonNegative <$> arbitrary

instance Show Nat where
  show = show . (natToIntegral :: Nat -> Integer)

infinity :: Nat
infinity = Succ infinity

compareLengthTo2 :: [a] -> Nat -> Ordering
compareLengthTo2 l n = g $ foldr f (Just n) l
  where
    f _ (Just Zero) = Nothing
    f _ (Just (Succ n)) = Just n
    f _ Nothing  = Nothing
    g (Just Zero) = EQ
    g (Just _) = LT
    g Nothing  = GT

prop2 :: [()] -> Nat -> Property
prop2 l n = compareLengthTo l (natToIntegral n) === compareLengthTo2 l n

-- >>> compareLengthTo2 [] infinity
-- LT

观察足够长的时间后，我们发现它适用于无限数字，而不适用于无限列表。这就是在他的定义中使用 foldNat 的原因。因此，如果我们折叠数字参数，我们将得到适用于无限列表但有限数字的函数：

compareLengthTo3 :: [a] -> Nat -> Ordering
compareLengthTo3 l n = g $ foldNat f (Just l) n
  where
    f (Just [])     = Nothing
    f (Just (x:xs)) = Just xs
    f Nothing       = Nothing
    g (Just [])     = EQ
    g (Just _)      = GT
    g Nothing       = LT

prop3 :: [()] -> Nat -> Property
prop3 l n = compareLengthTo l (natToIntegral n) === compareLengthTo3 l n

nats :: [Nat]
nats = iterate Succ Zero

-- >>> compareLengthTo3 nats (natFromInteger 10)
-- GT

foldr 和 foldNat 是一种在参数上概括结构递归的函数 (catamorphisms)。他们有很好的属性给定 finite 输入和总函数作为参数，它们也是总的，即总是终止。

这就是我们在最后一个例子中 foldNat 的原因。我们假设 Nat 参数是有限的，因此 compareLengthTo3 适用于所有 [a] - 甚至是无限的。

`foldr` 或其他高阶函数的通用性

Generality of `foldr` or other higher order function

algorithm

haskell

编辑