Also I'm guessing 1, 2 and 17 are just examples, he really wants arbitrary length finite lists.

/J

On 13 October 2010 20:47, Daniel Peebles <pumpkingod@gmail.com> wrote:

One option could be something like:

data Z
data S n

data Vec n a where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

data Length n where
  One :: Length (S Z)
  Two :: Length (S (S Z))
  Seventeen :: Length (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))

data FixedVec a where

  FixedVec :: Legnth n -> Vec n a -> FixedVec a

But it's obviously rather cumbersome :)

On Wed, Oct 13, 2010 at 7:57 AM, Jason Dusek <jason.dusek@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?

--
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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe