3 ms·
Thanks for the informative post. Could you please clarify a couple of things for me? > Named instances are incompatible with coherence. We could > just put one
by oggy 11y ago
Thanks for the informative post. Could you please clarify a couple of things for me?
> Named instances are incompatible with coherence. We could
> just put one named instance into a runtime object
Could you give an example of what you mean in, e.g., Haskell (assuming some fictional facility for named instances existed)?
> With dependent types, checking whether two instance heads
> are different
What are instance heads?
- Kutta 11y ago> instance heads Instance heads are the types in the instance declaration that the compiler dispatches on, for example in `instance Show Int` the head is `Int`. > named instances You can see an example for named instances in Idris (very Haskell-like syntax) here (http://idris.readthedocs.org/en/latest/tutorial/classes.html#named-instances http://idris.readthedocs.org/en/latest/tutorial/classes.html...). We could put named instances into runtime objects (example in Haskell: `data ShowInstance a = Show a => Instance` which does exactly this), thereby forgetting the name, which could cause ambiguities down the line. But even without instances in runtime boxes, different instances for the same type necessitate that there are some rules for instance resolution that a programmer has to consider. For example, if we have two monoid instances for `Int`, one with addition and one with multiplication, we somehow need to make sure that the monoid operations mean what we want them to mean, so that we don't get unexpectedly addition instead of multiplication.