Hm. This is not actually an answer to your question, just a "discussion starter", but still.
The code below typechecks, though actually it shouldn't: there's no type "n" such that "ones" is formed by the FL from some value of type List Int n. Or should it? {-# LANGUAGE ExistentialQuantification, GADTs, EmptyDataDecls #-} module Finite where data Zero data Succ a class Finite a where instance Finite Zero instance (Finite a) => Finite (Succ a) data List a n where Nil :: List a Zero Cons :: (Finite n) => a -> List a n -> List a (Succ n) data FiniteList a where FL :: (Finite n) => List a n -> FiniteList a nil :: FiniteList a nil = FL Nil cons :: a -> FiniteList a -> FiniteList a cons a (FL x) = FL (Cons a x) list123 = cons 1 (cons 2 (cons 3 nil)) ones = cons 1 ones -- typechecks ok 2010/10/13 Jason Dusek <jason.du...@gmail.com>: > 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? > > -- > Jason Dusek > Linux User #510144 | http://counter.li.org/ > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Eugene Kirpichov Senior Software Engineer, Grid Dynamics http://www.griddynamics.com/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe