On 13 October 2010 08:57, Jason Dusek
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