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 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@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

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 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 wrote:

...

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 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@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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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 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 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 wrote:

...

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 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@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@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