[Haskell-cafe] Finite but not fixed length...

Daniel Peebles pumpkingod at gmail.com
Wed Oct 13 14:47:00 EDT 2010


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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20101013/d884059a/attachment.html


More information about the Haskell-Cafe mailing list