4 ms·
That's not good. We can put an instance into a runtime box, pass it to another module, and now there are potentially two different instances to choose from in t
by Kutta 11y ago
That's not good. We can put an instance into a runtime box, pass it to another module, and now there are potentially two different instances to choose from in the other module. We'd have to ban moving around instances in runtime data if we are to preserve class coherence, which is unsatisfactory.
- jules 11y ago> and now there are potentially two different instances to choose from in the other module [...] to preserve class coherence I know the standard arguments for class coherence (Set etc.), but I haven't found any of them convincing. Relying on two values coming from two different places to be the same indicates that the design of the code is wrong. It's like writing a function f x y but you must only ever call it with identical arguments x=y. The right thing to do then is to give f only one argument to begin with.
- Kutta 11y agoI consider coherence seriously mainly because Edward Kmett supports it, and he has immense experience regarding the relative merits of coherent vs. incoherent classes in practical development. One core Kmett argument that I subscribe to is that 95% percent of the time there is no newtype noise needed, and in that case coherence is very nice, since one doesn't have to think about class hierarchies (which can get very complex, with many alternate instance derivations) as far as the code typechecks. But aside of that, I'm not all that convinced of the importance of coherence in a dependent setting either! My intuition is that types should encode all the properties that we'd like to be able to use in instances. In other words, even if we don't get coherence, we can use types to constrain the implementation of instances as much as we like. Highly ambiguous instance resolution (like a bunch of Monoid Int instances lying around) is a bit of a pain though, and there could be some "using instance" feature/syntax that locally throws out all instances except one. Additionally, as of now there are no large production code bases that use Coq style type classes in a proper dependent language. There are very few sizable applications in dependent languages to begin with. So we don't know a lot about the practical caveats of that design, while there is a lot of experience and know-how about Haskell-style classes, which is one reason why we should at least consider salvaging coherence in future languages. Generally, I think that type classes are a rather ugly and haphazard construction compared to the succinct elegance of the type theories of core languages; still, eventually type classes worm their way into languages (Agda, Coq) because people really like them and like to use them, so a language designer should consider them. I wish there was an elegant/general formal treatment that captures the essential features, in any case.
- TuringTest 11y agoWhat if you'd have a way to disambiguate in such cases, just like you do with method overriding? Tie the type definition to the point where the data is created. Default to the local definition, but have a way to select the other one if you need some particular interaction between modules. Wouldn't that solve the conflict?
- merijnv 11y agoBut then my ability to insert elements into a Set depends on the location where those elements were created...that sounds awful.
- marcosdumay 11y agoThat's exactly the same problem you have with every other Haskell name. Have you got much trouble with those on function names?
- merijnv 11y agoThe origin of a name is statically known in the location (i.e. file, expression, whatever). The origin of data is dynamic and can vary at runtime based on arbitrary previous evaluations. Unless you're going to propose making types unique (i.e., not compatible) depending on their origin and enforce never mixing them in the compiler. At which point you have basically reinvented "newtype"
- justthistime_ 11y agoIf you care about coherence, you should be very dissatisfied with GHC anyway.
- Kutta 11y agoCurrent GHC by default either prevents me from getting incoherence or at least throws warnings on orphan instances. What matters is whether a) someone not caring about incoherence writes coherent classes by default, just by not trying to actively screw up the system b) if you're actively trying to write coherent classes, you have a very easy job. On both accounts GHC does well enough.
- justthistime_ 11y agoYes, as long as you never use any third-party library and place all your code into a single module, GHC doesn't completely fail on its promises. My concern is that this PhD-style development suffices for most Haskell users, but is not practical for any non-small project in the real world with more than one developer.