有没有办法分开无限列表和有限列表？

Question

例如，我正在为列表编写一些函数，我想使用长度函数

foo :: [a] -> Bool
foo xs = length xs == 100

有人怎么能理解这个函数是否可以与无限列表一起使用？

或者我应该总是考虑无限列表并使用类似的东西

foo :: [a] -> Bool
foo xs = length (take 101 xs) == 100

而不是直接使用长度？

如果 haskell 有 FiniteList 类型，那么 length 和 foo 会怎样

length :: FiniteList a -> Int
foo :: FiniteList a -> Bool

Answer 1

length 遍历整个列表，但要确定列表是否具有特定长度 n，您只需查看第一个 n 元素。

您使用take 的想法会奏效。或者 您可以像这样编写lengthIs 函数：

-- assume n >= 0
lengthIs 0 [] = True
lengthIs 0 _  = False
lengthIs n [] = False
lengthIs n (x:xs) = lengthIs (n-1) xs

您可以使用相同的想法编写lengthIsAtLeast 和lengthIsAtMost 变体。

Answer 2

编辑时：我主要回答您标题中的问题，而不是您的特定示例的细节（ErikR 的回答非常好）。

列表上的许多函数（例如length 本身）仅对有限列表有意义。如果您编写的函数仅对有限列表有意义，请在文档中明确说明（如果不明显）。由于停止问题无法解决，因此没有任何方法可以强制执行该限制。根本没有算法可以提前确定是否理解

takeWhile f [1..]

（其中f 是整数谓词）生成有限或无限列表。

Answer 3

Nats 和懒惰再次来袭：

import Data.List

data Nat = S Nat | Z deriving (Eq)

instance Num Nat where
    fromInteger 0 = Z
    fromInteger n = S (fromInteger (n - 1))

    Z   + m = m
    S n + m = S (n + m)

lazyLength :: [a] -> Nat
lazyLength = genericLength

main = do
    print $ lazyLength [1..]    == 100 -- False
    print $ lazyLength [1..100] == 100 -- True

Answer 4

ErikR 和 John Coleman 已经回答了您问题的主要部分，但我想补充一点：

最好以不依赖于输入的有限性或无限性的方式编写函数 - 有时这是不可能的，但很多时候只是重新设计的问题。例如，您可以计算一个运行平均值，而不是计算整个列表的平均值，它本身就是一个列表；如果输入列表是无限的，那么这个列表本身就是无限的，否则就是有限的。

avg :: [Double] -> [Double]
avg = drop 1 . scanl f 0.0 . zip [0..]
  where f avg (n, i) = avg * (dbl n / dbl n') +
                       i            / dbl n'      where n'  = n+1
                                                        dbl = fromInteger

在这种情况下，您可以平均一个无限列表，而不必取其length：

*Main> take 10 $ avg [1..]
[1.0,1.5,2.0,2.5,3.0,3.5,4.0,4.5,5.0]

---

换句话说，一种选择是将尽可能多的函数设计为根本不关心无穷大方面，并将列表的（完整）评估和其他（可能是无限的）数据结构延迟到最后一个阶段尽可能在你的程序中。

通过这种方式，它们也将更具可重用性和可组合性——任何对其输入的一般假设更少或更多的东西往往更具可组合性；相反，任何具有更多或更多特定假设的东西往往不太可组合，因此可重用性较差。

Answer 5

有几种不同的方法可以创建有限列表类型。第一个是简单地使列表在其脊椎骨中变得严格：

data FList a = Nil | Cons a !(FList a)

不幸的是，这抛弃了懒惰带来的所有效率优势。其中一些可以通过使用长度索引列表来恢复：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

data Nat = Z | S Nat deriving (Show, Read, Eq, Ord)

data Vec :: Nat -> * -> * where
  Nil :: Vec 'Z a
  Cons :: a -> Vec n a -> Vec ('S n) a

instance Functor (Vec n) where
  fmap _f Nil = Nil
  fmap f (Cons x xs) = Cons (f x) (fmap f xs)

data FList :: * -> * where
  FList :: Vec n a -> FList a

instance Functor FList where
  fmap f (FList xs) = FList (fmap f xs)

fcons :: a -> FList a -> FList a
fcons x (FList xs) = FList (Cons x xs)

funcons :: FList a -> Maybe (a, FList a)
funcons (FList Nil) = Nothing
funcons (FList (Cons x xs)) = Just (x, FList xs)

-- Foldable and Traversable instances are straightforward
-- as well, and in recent GHC versions, Foldable brings
-- along a definition of length.

GHC 不允许无限类型，因此无法构建无限 Vec，因此无法构建无限 FList (1)。但是，FList 可以稍微懒惰地转换和使用，从而带来缓存和垃圾收集的好处。

(1) 请注意，类型系统强制 fcons 在其 FList 参数中为 strict，因此任何与 FList 打结的尝试都会触底。