One option could be something like:<div><br></div><div>data Z</div><div>data S n</div><div><br></div><div>data Vec n a where</div><div>  Nil :: Vec Z a</div><div>  Cons :: a -&gt; Vec n a -&gt; Vec (S n) a</div><div><br></div>
<div>data Length n where</div><div>  One :: Length (S Z)</div><div>  Two :: Length (S (S Z))</div><div>  Seventeen :: Length (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))</div><div><br></div><div>data FixedVec a where</div>
<div>  FixedVec :: Legnth n -&gt; Vec n a -&gt; FixedVec a</div><div><br></div><div>But it&#39;s obviously rather cumbersome :)<br><br><div class="gmail_quote">On Wed, Oct 13, 2010 at 7:57 AM, Jason Dusek <span dir="ltr">&lt;<a href="mailto:jason.dusek@gmail.com">jason.dusek@gmail.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">  Is there a way to write a Haskell data structure that is<br>
  necessarily only one or two or seventeen items long; but<br>
  that is nonetheless statically guaranteed to be of finite<br>
  length?<br>
<font color="#888888"><br>
--<br>
Jason Dusek<br>
Linux User #510144 | <a href="http://counter.li.org/" target="_blank">http://counter.li.org/</a><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</font></blockquote></div><br></div>