Strange error with type classes + associated types

newer
Continual delivery status...

older
US Patent for the idea of using...

Brent Yorgey

13 Apr 2010 13 Apr '10

10:48 p.m.

Hi all, Consider the following declarations.

...

-- from vector-space package: (*.*) :: (HasBasis u, HasTrie (Basis u), HasBasis v, HasTrie (Basis v), VectorSpace w, Scalar v ~ Scalar w) => (v :-* w) -> (u :-* v) -> u :-* w

-- my code: data Affine v = Affine (v :-* v) v

instance (HasBasis v, HasTrie (Basis v), VectorSpace v) => Monoid (Affine v) where mempty = Affine idL zeroV mappend (Affine a2 b2) (Affine a1 b1) = Affine (a2 *.* a1) (lapply a2 b1 ^+^ b2)

When I try to compile this, I get the following error: No instance for (HasTrie (Basis u)) arising from a use of `*.*' at Diagrams.hs:107:50-58 Possible fix: add an instance declaration for (HasTrie (Basis u)) In the first argument of `Affine', namely `(a2 *.* a1)' In the expression: Affine (a2 *.* a1) (lapply a2 b1 ^+^ b2) In the definition of `mappend': mappend (Affine a2 b2) (Affine a1 b1) = Affine (a2 *.* a1) (lapply a2 b1 ^+^ b2) This seems bizarre to me; it seems like GHC ought to be able to infer that in my use of (*.*), u,v, and w are all instantiated to the v in the instance declaration, and hence all the required constraints are satisfied. I have no idea why it would be complaining about u --- there's nothing called u in my instance declaration. Can someone more well-versed in the intricacies of type checking with associated types explain this? Or is this a bug in GHC? -Brent

Show replies by date

Stephen Tetley

14 Apr 14 Apr

4:51 a.m.

On 14 April 2010 03:48, Brent Yorgey wrote:

...

Can someone more well-versed in the intricacies of type checking with associated types explain this? Or is this a bug in GHC?

Hi Brent Maybe you can't compose linear maps of the same type, and thus can't build a valid monoid instance? If you take the definition of append out out the class - GHCi will give it a type:

...

append (Affine a2 b2) (Affine a1 b1) = Affine (a2 *.* a1) (lapply a2 b1 ^+^ b2)

*VectorSpace> :t append append :: (Scalar v ~ Scalar v1, Basis v ~ Basis u, Basis v1 ~ Basis v, VectorSpace v1, HasTrie (Basis v), HasBasis v, HasBasis u) => Affine v1 -> Affine v -> Affine v1 If you add that type back to the file containing append it no longer type checks... VectorSpaceTest.hs:44:54: Couldn't match expected type `Basis u' against inferred type `Basis u1' NB: `Basis' is a type function, and may not be injective Expected type: u :-* v Inferred type: v :-* v In the second argument of `(*.*)', namely `a1' In the first argument of `Affine', namely `(a2 *.* a1)' Failed, modules loaded: none. [ It also has the problem that its type isn't compatible with monoidal mappend anyway ] You can get empty to type check with this signature: empty :: (HasTrie u, u ~ Basis v, HasBasis v) => Affine v But trying to get append to type check with the same class constraints... append :: (HasTrie u, u ~ Basis v, HasBasis v) => Affine v -> Affine v -> Affine v ... gets another error where the inferred type of 'LinearMap' is from one type to the same type: VectorSpaceTest.hs:33:54: Couldn't match expected type `Basis u' against inferred type `u1' `u1' is a rigid type variable bound by the type signature for `append' at VectorSpace.hs:31:19 NB: `Basis' is a type function, and may not be injective Expected type: u :-* v Inferred type: v :-* v In the second argument of `(*.*)', namely `a1' In the first argument of `Affine', namely `(a2 *.* a1)' Failed, modules loaded: none.

Brent Yorgey

10:30 a.m.

On Wed, Apr 14, 2010 at 09:51:52AM +0100, Stephen Tetley wrote:

...

On 14 April 2010 03:48, Brent Yorgey wrote:

...
Can someone more well-versed in the intricacies of type checking with associated types explain this? Or is this a bug in GHC?

If you take the definition of append out out the class - GHCi will give it a type:

...
append (Affine a2 b2) (Affine a1 b1) = Affine (a2 *.* a1) (lapply a2 b1 ^+^ b2)

*VectorSpace> :t append append :: (Scalar v ~ Scalar v1, Basis v ~ Basis u, Basis v1 ~ Basis v, VectorSpace v1, HasTrie (Basis v), HasBasis v, HasBasis u) => Affine v1 -> Affine v -> Affine v1

Right, this seems weird to me. Why is there still a 'u' mentioned in the constraints? Actually, I don't even see why there ought to be both v and v1. The type of (*.*) mentions three type variables, u, v, and w: (*.*) :: (HasBasis u, HasTrie (Basis u), HasBasis v, HasTrie (Basis v), VectorSpace w, Scalar v ~ Scalar w) => (v :-* w) -> (u :-* v) -> u :-* w The type of a2 is unified with (v :-* w) and the type of a1 is unified with (u :-* v). Since both a1 and a2 are obtained from pattern-matching on an Affine constructor (which contains something of type (z :-* z)), u, v, and w ought to all unify to the same thing. Instead we get a bunch of strange type equalities which don't help because Scalar and Basis may not be injective.

...

If you add that type back to the file containing append it no longer type checks...

VectorSpaceTest.hs:44:54: Couldn't match expected type `Basis u' against inferred type `Basis u1' NB: `Basis' is a type function, and may not be injective Expected type: u :-* v Inferred type: v :-* v In the second argument of `(*.*)', namely `a1' In the first argument of `Affine', namely `(a2 *.* a1)' Failed, modules loaded: none.

[ It also has the problem that its type isn't compatible with monoidal mappend anyway ]

Its type WOULD be compatible with mappend (just unify v and v1) if it weren't for that pesky u. Thanks for looking at this. I think I'll file a bug. I hope very much that it IS a bug, because otherwise I don't understand what's going on at all. -Brent

Roman Leshchinskiy

10:48 a.m.

On 15/04/2010, at 00:30, Brent Yorgey wrote:

...

On Wed, Apr 14, 2010 at 09:51:52AM +0100, Stephen Tetley wrote:

...
On 14 April 2010 03:48, Brent Yorgey wrote:

...
Can someone more well-versed in the intricacies of type checking with associated types explain this? Or is this a bug in GHC?

If you take the definition of append out out the class - GHCi will give it a type:

...
append (Affine a2 b2) (Affine a1 b1) = Affine (a2 *.* a1) (lapply a2 b1 ^+^ b2)

*VectorSpace> :t append append :: (Scalar v ~ Scalar v1, Basis v ~ Basis u, Basis v1 ~ Basis v, VectorSpace v1, HasTrie (Basis v), HasBasis v, HasBasis u) => Affine v1 -> Affine v -> Affine v1

Right, this seems weird to me. Why is there still a 'u' mentioned in the constraints? Actually, I don't even see why there ought to be both v and v1. The type of (*.*) mentions three type variables, u, v, and w:

(*.*) :: (HasBasis u, HasTrie (Basis u), HasBasis v, HasTrie (Basis v), VectorSpace w, Scalar v ~ Scalar w) => (v :-* w) -> (u :-* v) -> u :-* w

Note that (:-*) is a type synonym: type :-* u v = MSum (Basis u :->: v) Substituting this into the type of (*.*), we get: (*.*) :: ... => MSum (Basis v :-* w) -> MSum (Basis u :-* v) -> MSum (Basis u :-* w) Now, Basis is an associated type: class VectorSpace v => HasBasis v where type Basis v ... This means that there is no way to obtain u from Basis u. Since u only ever occurs as an argument to Basis, a type family, it can never be unified with anything. This, in turn, means that there is no way to call (*.*) at all (unless I'm severely mistaken). Roman

Brent Yorgey

11:01 a.m.

On Thu, Apr 15, 2010 at 12:48:20AM +1000, Roman Leshchinskiy wrote:

...

...
Right, this seems weird to me. Why is there still a 'u' mentioned in the constraints? Actually, I don't even see why there ought to be both v and v1. The type of (*.*) mentions three type variables, u, v, and w:

(*.*) :: (HasBasis u, HasTrie (Basis u), HasBasis v, HasTrie (Basis v), VectorSpace w, Scalar v ~ Scalar w) => (v :-* w) -> (u :-* v) -> u :-* w

Note that (:-*) is a type synonym:

type :-* u v = MSum (Basis u :->: v)

Aha! That's what I was missing. Thanks for the insight, Roman. I guess it's time to go bug Conal... =) -Brent

Conal Elliott

16 Apr 16 Apr

9 p.m.

Hi Brent, I'm sorry to hear that the non-injectivity issue bit you. It's bitten me also at times, leading me to choose associated data types (injective) instead of associated synonyms (potentially non-injective). And sometimes, the data types route is problematic, as the new types aren't instances (and I don't know how to declare them to be) of other classes when I need them to be. MemoTrie & vector-space seem to trip over these issues, and I thought I'd lucked into a combo that worked, but from your note I guess I just hadn't pushed far enough to uncover difficulties. I'm unsure now, but I think I tried making Basis a data type (not syn) and ran into the problem I mentioned above. The Basis *synonyms* also have HasTrie instances, which is crucially important. If we switch to (injective) data types, then we lose the HasTrie instances. I'd be okay with defining HasTrie instances (preferably via "deriving") for the associated Basis data types, but I couldn't figure out how to. Maybe it's not possible currently, or maybe I just didn't know how. I'd love to have help exploring these issues more widely & deeply, as they do seem to fatally wound the usefulness of associated data types. - Conal On Wed, Apr 14, 2010 at 8:01 AM, Brent Yorgey wrote:

...

On Thu, Apr 15, 2010 at 12:48:20AM +1000, Roman Leshchinskiy wrote:

...
...
Right, this seems weird to me. Why is there still a 'u' mentioned in the constraints? Actually, I don't even see why there ought to be both v and v1. The type of (*.*) mentions three type variables, u, v,

and w:

...
...
(*.*) :: (HasBasis u, HasTrie (Basis u), HasBasis v, HasTrie (Basis v), VectorSpace w, Scalar v ~ Scalar w) => (v :-* w) -> (u :-* v) -> u :-* w

Note that (:-*) is a type synonym:

type :-* u v = MSum (Basis u :->: v)

Aha! That's what I was missing. Thanks for the insight, Roman. I guess it's time to go bug Conal... =)

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

Roman Leshchinskiy

17 Apr 17 Apr

6:46 a.m.

On 17/04/2010, at 11:00, Conal Elliott wrote:

...

I'm unsure now, but I think I tried making Basis a data type (not syn) and ran into the problem I mentioned above. The Basis *synonyms* also have HasTrie instances, which is crucially important. If we switch to (injective) data types, then we lose the HasTrie instances. I'd be okay with defining HasTrie instances (preferably via "deriving") for the associated Basis data types, but I couldn't figure out how to. Maybe it's not possible currently, or maybe I just didn't know how.

Could you perhaps make (:-*) a proper type rather than a synonym? That would help with the ambiguity. Roman

Conal Elliott

1:28 p.m.

Oh! I'd completely forgotten about this idea. Looking at Data.LinearMap in vector-space, I see a comment about exactly this ambiguity, as well as the start of a new module that wraps a data type around the linear map representation. I don't recall whether I got stuck or just distracted. On Sat, Apr 17, 2010 at 3:46 AM, Roman Leshchinskiy wrote:

...

On 17/04/2010, at 11:00, Conal Elliott wrote:

...
I'm unsure now, but I think I tried making Basis a data type (not syn) and ran into the problem I mentioned above. The Basis *synonyms* also have HasTrie instances, which is crucially important. If we switch to (injective) data types, then we lose the HasTrie instances. I'd be okay with defining HasTrie instances (preferably via "deriving") for the associated Basis data types, but I couldn't figure out how to. Maybe it's not possible currently, or maybe I just didn't know how.

Could you perhaps make (:-*) a proper type rather than a synonym? That would help with the ambiguity.

Roman

Brent Yorgey

19 Apr 19 Apr

12:02 a.m.

Conal, Thanks for looking into this! Making (:-*) into a proper type seems promising. I did try wrapping (:-*) in a newtype but that didn't help (although I didn't expect it to). I see you just uploaded a new version of vector-space; what's new in 0.6.2? -Brent On Sat, Apr 17, 2010 at 10:28:45AM -0700, Conal Elliott wrote:

...

Oh! I'd completely forgotten about this idea. Looking at Data.LinearMap in vector-space, I see a comment about exactly this ambiguity, as well as the start of a new module that wraps a data type around the linear map representation. I don't recall whether I got stuck or just distracted.

On Sat, Apr 17, 2010 at 3:46 AM, Roman Leshchinskiy wrote:

...
On 17/04/2010, at 11:00, Conal Elliott wrote:

...
I'm unsure now, but I think I tried making Basis a data type (not syn) and ran into the problem I mentioned above. The Basis *synonyms* also have HasTrie instances, which is crucially important. If we switch to (injective) data types, then we lose the HasTrie instances. I'd be okay with defining HasTrie instances (preferably via "deriving") for the associated Basis data types, but I couldn't figure out how to. Maybe it's not possible currently, or maybe I just didn't know how.

Could you perhaps make (:-*) a proper type rather than a synonym? That would help with the ambiguity.

Roman

...

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

Conal Elliott

12:40 p.m.

On Sun, Apr 18, 2010 at 9:02 PM, Brent Yorgey wrote:

...

Conal,

Thanks for looking into this! Making (:-*) into a proper type seems promising. I did try wrapping (:-*) in a newtype but that didn't help (although I didn't expect it to).

What do you mean by a "proper type"? I didn't know what Roman meant either, though I guessed he meant a newtype or data type.

...

I see you just uploaded a new version of vector-space; what's new in 0.6.2?

The dependency on the Boolean package now specifies >= 0.0.1.

...

-Brent

...
Oh! I'd completely forgotten about this idea. Looking at Data.LinearMap in vector-space, I see a comment about exactly this ambiguity, as well as

On Sat, Apr 17, 2010 at 10:28:45AM -0700, Conal Elliott wrote: the

...
start of a new module that wraps a data type around the linear map representation. I don't recall whether I got stuck or just distracted.

On Sat, Apr 17, 2010 at 3:46 AM, Roman Leshchinskiy
...
On 17/04/2010, at 11:00, Conal Elliott wrote:

...
I'm unsure now, but I think I tried making Basis a data type (not syn) and ran into the problem I mentioned above. The Basis *synonyms* also have HasTrie instances, which is crucially important. If we switch to (injective) data types, then we lose the HasTrie instances. I'd be okay with defining HasTrie instances (preferably via "deriving") for the associated Basis data types, but I couldn't figure out how to. Maybe it's not possible currently, or maybe I just didn't know how.

Could you perhaps make (:-*) a proper type rather than a synonym? That would help with the ambiguity.

Roman

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

Brent Yorgey

6:22 p.m.

On Mon, Apr 19, 2010 at 09:40:25AM -0700, Conal Elliott wrote:

...

On Sun, Apr 18, 2010 at 9:02 PM, Brent Yorgey wrote:

...
Conal,

Thanks for looking into this! Making (:-*) into a proper type seems promising. I did try wrapping (:-*) in a newtype but that didn't help (although I didn't expect it to).

What do you mean by a "proper type"? I didn't know what Roman meant either, though I guessed he meant a newtype or data type.

Yes, that's what I meant too, sorry for the imprecise terminology.

...

...
I see you just uploaded a new version of vector-space; what's new in 0.6.2?

The dependency on the Boolean package now specifies >= 0.0.1.

Ah, OK. -Brent

5512

Age (days ago)

5517

Last active (days ago)

List overview

Download

10 comments

4 participants

participants (4)

Brent Yorgey
Conal Elliott
Roman Leshchinskiy
Stephen Tetley