Re: [Haskell-cafe] Strange error with type classes + associated types
On Sun, Apr 18, 2010 at 9:02 PM, Brent Yorgey byor...@seas.upenn.eduwrote: 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 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 r...@cse.unsw.edu.au 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange error with type classes + associated types
On Mon, Apr 19, 2010 at 09:40:25AM -0700, Conal Elliott wrote: On Sun, Apr 18, 2010 at 9:02 PM, Brent Yorgey byor...@seas.upenn.eduwrote: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange error with type classes + associated types
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 r...@cse.unsw.edu.auwrote: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange error with type classes + associated types
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
Re: [Haskell-cafe] Strange error with type classes + associated types
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 r...@cse.unsw.edu.auwrote: 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
Re: [Haskell-cafe] Strange error with type classes + associated types
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 byor...@seas.upenn.eduwrote: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange error with type classes + associated types
On 14 April 2010 03:48, Brent Yorgey byor...@seas.upenn.edu 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange error with type classes + associated types
On Wed, Apr 14, 2010 at 09:51:52AM +0100, Stephen Tetley wrote: On 14 April 2010 03:48, Brent Yorgey byor...@seas.upenn.edu 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange error with type classes + associated types
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 byor...@seas.upenn.edu 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange error with type classes + associated types
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
[Haskell-cafe] Strange error with type classes + associated types
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
