Alternatives to type classes.
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? -- Jason Dusek
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
On Tue, Dec 29, 2009 at 6:22 PM, Jason Dusek
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 / _)
Ignoring 0 for sake of discussion.
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?
I consider typeclasses a happy notational medium. They are not perfect, they miss some cases, but they are pretty good. For full generality at the expense of some verbosity, I like Agda's solution pretty well. Agda allows you to "open" a record into a scope. record Group (a : Set) where field _+_ : a -> a -> a -_ : a -> a 0 : a conj : {a : Set} -> Group a -> a -> a -> a conj g x y = x + y + (-x) where open g Maybe I even got the syntax right :-P The cool thing is that you can use this for the invariant-keeping property of typeclasses, too. Eg. Data.Map relies on the fact that there is at most one Ord instance per type. By parameterizing the module over the Ord record, we can do the same: record Ord (a : Set) where ... module MapMod (a : Set) (ord : Ord a) where Map : b -> Set Map = ... insert : {b : Set} -> a -> b -> Map b -> Map b insert = ... ... So we have the liberty of being able to use different Ord instances, but different Ord instances give rise to different Map types, so we can not violate any invariants. You can do something similar in Haskell using an existential type, although it is very inconvenient: data Ord a = ... data MapMod map a b = MapMod { empty :: map a b, insert :: a -> b -> map a b -> map a b, ... } withMap :: Ord a -> (forall map. MapMod map a b -> z) -> z withMap ord f = f ( {- implement MapMod here, using ord for ordering }- ) Then you could use maps on different Ords for the same type, but they could not talk to each other. Some syntax sugar could help the Haskell situation quite a lot. Luke
participants (3)
-
Dan Doel -
Jason Dusek -
Luke Palmer