On Tuesday 29 December 2009 8:22:15 pm Jason Dusek wrote:
Consider the real numbers. They "are" a group. We have an identity element `0', inverses and closure under the associative operation `+'.
Group+ = (+, 0, -1 * _)
They are another group, too -- the group with `*':
Group* = (*, 1, 1 / _)
This seems like a real problem with the whole notion of typeclasses -- we can't really say a set/type "is" its extension with some new operations.
One road to go on this is to make every extension of the set with new ops a different type; but that seems really horribly inconvenient. I wonder what approaches have been tried here?
The solution to this used in the standard library tends to be to define a newtype wrapper to select the right group structure. But that isn't ideal. What this is really indicating is that we want a parameterized module or (dependent) record of some sort. For instance: data GroupStructure a = Group { (*) :: a -> a -> a ; e :: a ; inv :: a -> a } which works fine in this case, because there are no associated types (and we can't encode equational laws in the type system anyway). But if there were, we'd probably want something more like ML modules (or dependent records). And of course, that's essentially what type classes are. They're records/modules that are uniquely determined by the type(s) in question, so they can be filled in automatically. But that obviously doesn't work very well when there isn't a single correct instance for any type. Sometimes there are many valid instances but one 'best' one, and I've wondered if something like: class Group a where structure :: GroupStructure a might not be a decent way to go. One can then write things like: foo :: GroupStructure a -> ... foo gs = ... foo' :: Group a => ... foo' = foo structure where foo is for people who want to use the non-standard instances, while foo' retains the ease of use. But that's quite a bit of boilerplate, so ideally I suppose this sort of duality would be recognized and supported by the language---there would be a default GroupStructure for various types you could use like with type classes, but you could supply a custom GroupStructure to the very same function if you wished. I think this may be the way type classes work in Coq, but I don't really have any experience using them there. -- Dan