Is there any way to separate infinite and finite lists?

Question

For example, I am writing some function for lists and I want to use length function

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

How can someone understand could this function be used with infinite lists or not?

Or should I always think about infinite lists and use something like this

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

instead of using length directly?

What if haskell would have FiniteList type, so length and foo would be

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

Answer 1

length traverses the entire list, but to determine if a list has a particular length n you only need to look at the first n elements.

Your idea of using take will work. Alternatively you can write a lengthIs function like this:

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

You can use the same idea to write the lengthIsAtLeast and lengthIsAtMost variants.

Answer 2

On edit: I am primaily responding to the question in your title rather than the specifics of your particular example, (for which ErikR's answer is excellent).

A great many functions (such as length itself) on lists only make sense for finite lists. If the function that you are writing only makes sense for finite lists, make that clear in the documentation (if it isn't obvious). There isn't any way to enforce the restriction since the Halting problem is unsolvable. There simply is no algorithm to determine ahead of time whether or not the comprehension

takeWhile f [1..]

(where f is a predicate on integers) produces a finite or an infinite list.

Answer 3

Nats and laziness strike again:

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