On Tue, Dec 16, 2008 at 11:50 PM, Apfelmus, Heinrich
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