[Haskell-cafe] Reversing a fixed-length vector
Erik Hesselink
hesselink at gmail.com
Tue Sep 9 14:21:58 UTC 2014
The problem with a class based approach is that the class context will
show up everywhere, even though all instances have already been
defined.
Erik
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
>>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list