[Haskell-cafe] Finite but not fixed length...

[Max Bolingbroke]

On 13 October 2010 08:57, Jason Dusek <jason.dusek at gmail.com> wrote:
>  Is there a way to write a Haskell data structure that is
>  necessarily only one or two or seventeen items long; but
>  that is nonetheless statically guaranteed to be of finite
>  length?

Maybe you want a list whose denotation is formed by a least (rather
than a greatest) fixed point? i.e. the type of spine-strict lists:

"""
data FinList a = Nil
               | Cons a !(FinList a)
               deriving (Show)


ones_fin = 1 `Cons` ones_fin

take_fin n Nil = Nil
take_fin n (Cons x rest)
  | n <= 0    = Nil
  | otherwise = Cons x (take_fin (n - 1) rest)

ones = 1 : ones

main = do
    print $ take 5 ones
    print $ take_fin 5 ones_fin
"""

If you have e :: FinList a then if e /= _|_ it is necessarily of finite length.

Max