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

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

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

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

takeWhile f [1..]

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

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

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

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.