[Haskell-beginners] Re: A type level programming question
Levi Stephen
levi.stephen at gmail.com
Sun Dec 21 17:17:29 EST 2008
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
More information about the Beginners
mailing list