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

[Apfelmus, Heinrich]

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