Gosh! I suspected I hit a non-trivial problem... cool!
C.
On Tue, Sep 9, 2014 at 3:56 PM, Carter Schonwald 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 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@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