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

On Tue, Dec 16, 2008 at 11:50 PM, Apfelmus, Heinrich wrote:

Put differently, always using elementAt would be pointless, i.e. you could dispense with type level integers entirely and use a normal list instead.

I am finding I need this less than I thought I would. I have been continuing on looking for alternatives and been fine so far.

Satisfying the i :<: s constraint means supplying a proof that the integer i is indeed smaller than s . Of course, if the index i is not known statically, you don't have such a proof and you won't be able to obtain one. But what you can do is to construct a different index j that is guaranteed to be smaller than s :

j = i `max` pred s

No matter what i is, j is always going to fulfill j :<: s. Hence, your function can be written as

elementAt :: FSVec s a -> Int -> Maybe a elementAt v i | 0 <= i && i < length v = reifyIntegral i at | otherwise = Nothing where at i = Just $ v ! max i (pred $ lengthT v)

(Note that it may be that this code still doesn't compile, for example because the type-level library maybe doesn't automatically deduce j :<: s or because the type checker doesn't accept our proof for some other reason.)

I couldn't get something along these lines to type check, but as mentioned above I'm doing ok without it so far. Thanks, Levi