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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On 14 April 2010 03:48, Brent Yorgey <[hidden email]> 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Wed, Apr 14, 2010 at 09:51:52AM +0100, Stephen Tetley wrote:
> On 14 April 2010 03:48, Brent Yorgey <[hidden email]> 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 <[hidden email]> 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 <[hidden email]> wrote:
_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 <[hidden email]> wrote:
_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 <[hidden email]>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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Sun, Apr 18, 2010 at 9:02 PM, Brent Yorgey <[hidden email]> wrote:
Conal, 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 The dependency on the Boolean package now specifies >= 0.0.1. -Brent _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Mon, Apr 19, 2010 at 09:40:25AM -0700, Conal Elliott wrote:
> On Sun, Apr 18, 2010 at 9:02 PM, Brent Yorgey <[hidden email]>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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |