When asked "When is a typeclass good", the common answer seems to be "When it has laws!"
This is a good start, but I think this is only the start of the story. The answer /ought/ to be "When it has laws, and a unique (lawful) instance". (1/4)
Conversation
This means most algebraic structures /do not/ make good typeclasses! For instance, consider Monoid. The thing that makes them cool is that there are a whole host of them! (2/4)
1
2
12
However, this is what makes programming with them /as a typeclass/ a huge pain. We need to constantly juggle newtypes just to convince instance selection to choose the right one, which is extremely clumsy. (3/4)
2
20
Not perfect but named implementations and using blocks seem like a sweet spot for me: idris2.readthedocs.io/en/latest/tuto ;
1
Unfortunately Idris seems to treat them as a bit of an afterthought. You get stuff like: github.com/idris-lang/Idr – this would behave in very confusing ways if named instances are actually being used. :(
1
1
Do you mean, as a result of an instance being overridden at some higher level, then propagating down into library code where you really want the default?
1
Named instances let you use different instances between calls to the `SortedMap` API. So you could accidentally compare two maps that use different orderings, or use different orderings over the lifetime of the map, leading to a map in a corrupted (non-sorted) state.
1
2
A more truthful and safe `SortedMap` type would be defined like:
record SortedMap k v (o : Ord k) where
...
1
2
Another approach would be:
record SortedMap k v where
constructor M
ord : Ord k
...
empty : Ord k => SortedMap k v
empty @{ord} = M empty ord
-- not sure if it's possible to bind instances like this
Tricky thing is:
(Eq k, Eq v) => Eq (SortedMap k v) where
(==) = (==) `on` toList
Where you need to constrain the two `ord` fields to be the same. Something like ML's `where type` could help here.
2