[Haskell-cafe] Reversing a fixed-length vector

[Cristiano Paris]

In the meantime I factored out the "Plus" type family.

https://gist.github.com/anonymous/77fe0d1a6525c9e78d42

I wonder whether it'd be possible to move the Type Equality at a more
general level in order to hold in any context where Plus appears.

C.

On Tue, Sep 9, 2014 at 4:45 PM, Cristiano Paris <frodo at theshire.org> wrote:

> I almost got there with Type Equalities, but I can't really understand the
> "VecReverse n (S m)" constraint in the instance bit of "VecReverse (S n) m".
>
> C.
>
> On Tue, Sep 9, 2014 at 4:12 PM, adam vogt <vogt.adam at gmail.com> wrote:
>
>> 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
>> >
>>
>
>
>
> --
> GPG Key: 4096R/C17E53C6 2010-02-22
> Fingerprint = 4575 4FB5 DC8E 7641 D3D8  8EBE DF59 B4E9 C17E 53C6
>
>



-- 
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/1859e38f/attachment.html>