[Haskell-cafe] Reversing a fixed-length vector

[adam vogt]

Hi Cristiano,

You can also convince ghc about (Plus n1 (S m) ~ S (Plus n1 m)) by
writing VecReverse as a class:
https://gist.github.com/aavogt/15399cbdd5e74d0e9cd8

Regards,
Adam

On Tue, Sep 9, 2014 at 10:07 AM, Cristiano Paris <frodo at theshire.org> wrote:
> Gosh! I suspected I hit a non-trivial problem... cool!
>
> C.
>
> On Tue, Sep 9, 2014 at 3:56 PM, Carter Schonwald
> <carter.schonwald at gmail.com> wrote:
>>
>> heres a version richard eisenburg helped me write
>> https://gist.github.com/cartazio/9340008
>> see the linked gist for the full code but heres the meat of it
>>
>>
>> data Shape (rank :: Nat) a where
>>     Nil  :: Shape Z a
>>     (:*) ::  !(a) -> !(Shape r a ) -> Shape  (S r) a
>>
>>     {-# INLINE reverseShape #-}
>> reverseShape :: Shape n a -> Shape n a
>> reverseShape Nil = Nil
>> reverseShape list = go SZero Nil list
>>   where
>>     go :: SNat n1 -> Shape n1  a-> Shape n2 a -> Shape (n1 + n2) a
>>     go snat acc Nil = gcastWith (plus_id_r snat) acc
>>     go snat acc (h :* (t :: Shape n3 a)) =
>>       gcastWith (plus_succ_r snat (Proxy :: Proxy n3))
>>               (go (SSucc snat) (h :* acc) t)
>>
>>
>> On Tue, Sep 9, 2014 at 8:55 AM, Cristiano Paris <frodo at theshire.org>
>> wrote:
>>>
>>> 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
>>>
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>
>
>
> --
> GPG Key: 4096R/C17E53C6 2010-02-22
> Fingerprint = 4575 4FB5 DC8E 7641 D3D8  8EBE DF59 B4E9 C17E 53C6
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>