[Haskell-cafe] Reversing a fixed-length vector

[Cristiano Paris]

Hi,

I'm playing around with Type Families so I decided to implement a simple
fixed-length Vect of Integers.

Here is my straightforward implementation (ghc 7.8.3):

https://gist.github.com/anonymous/d838e68ce6a02412859f

As you can see, I'm trying to implement a reverse function for my vectors
which guarantees that the output vector is the same size as the input one.
I tried to express this constraint at the type level.

The problem is that I can't have ghc to type check the reverse function in
the non-trivial case:

_________________
    Could not deduce (Plus n1 (S m) ~ S (Plus n1 m))
    from the context (n ~ S n1)
      bound by a pattern with constructor
                 CV :: forall n. Int -> Vect n -> Vect (S n),
               in an equation for ‘vecReverse’
      at vect3.hs:30:13-18
    Expected type: Vect (Plus n m)
      Actual type: Vect (Plus n1 (S m))
_________________

Iit has to do with the fact that the type checker can't deduce that:

Plus n1 (S m) ~ S (Plus n1 m) ~ Plus (S n1) m ~Plus n m

I tried to insert the following instance to the family:

Plus n (S m) = S (Plus n m)

but to no avail.

Any clue?

Thanks.

C.

-- 
GPG Key: 4096R/C17E53C6 2010-02-22
Fingerprint = 4575 4FB5 DC8E 7641 D3D8  8EBE DF59 B4E9 C17E 53C6
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140909/ab1d0800/attachment.html>