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.dusek@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/