Levi Stephen wrote:
Justin Bailey wrote:
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
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?
Yes and no. Actually, the type for elementAt should be elementAT :: FSVec s a -> Int -> Maybe a So, you can try to fetch an element at a particular index, but it's not guaranteed to work. In contrast, (!) :: (Pos s, Nat i, i :<: s) => FSVec s a -> i -> a is guaranteed to return an element because the index is guaranteed to be in range. The point is that i is usually not obtained from a value level integer, but instead constructed from other type level integers such that the construction vouches that it's in range. Put differently, always using elementAt would be pointless, i.e. you could dispense with type level integers entirely and use a normal list instead.
The type-level library provides the function reifyIntegral for this purpose, but the continuation is only allowed to rely on the Nat class constraint.
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.
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.) Regards, H. Apfelmus