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

[Levi Stephen]

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