[Haskell-beginners] A type level programming question

[Justin Bailey]

On Sun, Dec 14, 2008 at 3:11 PM, Levi Stephen <levi.stephen at gmail.com> wrote:
> (!) :: (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