...and you can always do hack :: Vec n a -> FixedVec a hack x :: FixedVec undefined 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