Next priority for OCaml?

Mmmm … in Rust you don’t have that property either. The most common example being the “collect” trait that converts an iterator into a collection type. You often have to write:

e1.collect()

in order to get a collection of type T [IIRC]. So for instance, you light want a vec, but you might want something else (list ?) It’s been nearly a year since I hacked Rust, so I don’t remember the precise details, but this isn’t a rare thing.

It’s mentioned in the Book: Traits: Defining Shared Behavior - The Rust Programming Language

This restriction is part of a property called coherence, and more specifically the orphan rule, so named because the parent type is not present. This rule ensures that other people’s code can’t break your code and vice versa. Without the rule, two crates could implement the same trait for the same type, and Rust wouldn’t know which implementation to use.

Example:

$ cargo build
   Compiling rc v0.1.0 (/Users/yawarquadiramin/src/rc)
error[E0119]: conflicting implementations of trait `S` for type `T`
  --> src/main.rs:12:1
   |
7  | impl S for T {
   | ------------ first implementation here
...
12 | impl S for T {
   | ^^^^^^^^^^^^ conflicting implementation for `T`

For more information about this error, try `rustc --explain E0119`.
error: could not compile `rc` (bin "rc") due to previous error

The problem I was indicating with not having coherence, however, is the other problem: the logic type checks but different instances are visible at different points in the logic and their behaviors are different in ways that lead programmers to assume that the type checker has provided a guarantee that it does not actually provide.

And I think that’s not all that different from the problem that a subclass often type checks as a subtype while it’s easy to write a subclass that cannot actually be substituted for any other instance of the superclass.

Accordingly I don’t think the essay is really describing a problem with ad hoc polymorphism. It’s describing a problem with the Liskov substituton principle in general— one that comes with the territory and you just have to live with it, in any language that allows substitution.

Yes, this means you don’t have coherence. Any sane implementation will fail the compile with a coherence error (‘multiple instances found’ etc.). The modular implicits paper also emphasizes this.

1 Like

The way I read the modular implicits paper is that it also emphasizes how canonical coherence is a property that cannot be achieved with the OCaml module language, and that what it proposes instead is non-ambiguous coherence, where there is unambiguously one implementation of an instance in scope at any given reference, which still allows for different implementations of the same instance to be in use in the same program.

As it happens, I think that’s a desirable language feature rather than a defect, but I’m probably in a very marginal minority on that point. I’m frequently clashing with colleagues on points related to this when similar conversations arise in the C++ community around function overloading and template specialization.

6 Likes