Strange error with type classes + associated types

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
11 messages Options
Reply | Threaded
Open this post in threaded view
|

Strange error with type classes + associated types

Brent Yorgey-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with type classes + associated types

Stephen Tetley-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with type classes + associated types

Brent Yorgey-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with type classes + associated types

Roman Leshchinskiy

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
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with type classes + associated types

Brent Yorgey-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with type classes + associated types

Conal Elliott
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:
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


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with type classes + associated types

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with type classes + associated types

Conal Elliott
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
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with type classes + associated types

Brent Yorgey-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with type classes + associated types

Conal Elliott
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.
 
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 <[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
Reply | Threaded
Open this post in threaded view
|

Re: Strange error with type classes + associated types

Brent Yorgey-2
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