On Sun, Dec 14, 2008 at 3:11 PM, Levi Stephen
(!) :: (Pos s, Nat i, i :<: s) => FSVec s a -> i -> a
I was wondering if it was possible to write a function of type:
elementAt :: FSVec s a -> Int -> a
that called the above function, throwing an error if the index was out of bounds. e.g.,
Why would you want to write that function? From the signature on (!), it looks like any out of bounds errors should occur at compile time. I'd say the library is trying to make it so you don't have to write that function. That said, I'd try removing the type signature from elementAt and see what your compiler infers for you. You'll also have to find a way to relate "idx" to "v". Unless "length v" returns a Nat, the comparison you have won't do it. Justin