Re: [Haskell-beginners] A type level programming question

On Tue, Dec 16, 2008 at 6:33 AM, Justin Bailey wrote:

On Sun, Dec 14, 2008 at 3:11 PM, Levi Stephen 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.

I may not have to write this function, but I'm guessing at some stage it's going to be necessary to convert from value level integers to type level. Is this a bad guess? The type-level library provides the function reifyIntegral for this purpose, but the continuation is only allowed to rely on the Nat class constraint.

That said, I'd try removing the type signature from elementAt and see what your compiler infers for you.

I don't know how to implement elementAt yet. FSVec provides the (!) function for accessing elements, but I need to satisfy the i :<: s class constraint before calling it.

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.

length has type forall s a. Nat s => FSVec s a -> Int

Justin

Thanks, Levi