[Haskell-beginners] A type level programming question

[Levi Stephen]

On Tue, Dec 16, 2008 at 6:33 AM, Justin Bailey <jgbailey at gmail.com> wrote:
> 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.

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