[Haskell-cafe] Reversing a fixed-length vector
Cristiano Paris
frodo at theshire.org
Tue Sep 9 14:07:43 UTC 2014
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140909/2b7b0370/attachment.html>
More information about the Haskell-Cafe
mailing list